Second International Conference on Application of Concurrency to System Design (ACSD'01)
The BDD Space Complexity of Different Forms of Concurrency
Newcastle upon Tyne, UK
June 25-June 29
ISBN: 0-7695-1071-X
Symbolic representations using binary decision diagrams (BDDs) are popular means to cope with extremely large state spaces. However, it may be the case that the BDD representation itself is prohibitively large. We consider the BDD representations of synchronous, asynchronous and interleaved processes with communication via shared variables and present upper bounds for their sizes. For this reason, we introduce a general representation strategy where a possible exponential growth of the BDD representation can only be due to the specifics of communication and/or write conflict resolution; it is never due to the number of processes or the concurrency discipline. Moreover, certain conditions on the communication and the write conflict resolution are postulated that lead to polynomial sized BDD representations.
Citation:
Michael Baldamus, Klaus Schneider, "The BDD Space Complexity of Different Forms of Concurrency," acsd, pp.231, Second International Conference on Application of Concurrency to System Design (ACSD'01), 2001