
Summary: The automated verification of concurrent systems by model checking is often confronted with the state space explosion problem. A widely adopted method to tackle this problem is to use Binary Decision Diagrams (BDDs) for representing systems and state spaces implicitly. However, it may be that even the system representation itself is prohibitively large. It is therefore interesting to study which factors influence the size of a BDD that represents the transition relation of a system. In this article, we consider the BDD representations of synchronous, asynchronous, and interleaved processes with communication via shared variables and present upper bounds for their sizes. To this end, we introduce a general representation strategy where catastrophic exponential growth of the BDD can only be due to the specifics of communication and/or write conflict resolution; it is neither due to the number of processes nor to the concurrency discipline. Moreover, conditions on communication and write conflict resolution are presented that are sufficient for polynomial sized BDD representations.
ddc:004, DATA processing & computer science, Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.), binary decision diagrams, info:eu-repo/classification/ddc/004, 004
ddc:004, DATA processing & computer science, Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.), binary decision diagrams, info:eu-repo/classification/ddc/004, 004
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 1 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
