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.
2
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
In the classical shared-variable models, component processes reside on their processors and communicate by shared variables in memory shared by the processors. In this paper, we argue that shared memory is not necessary to share variables. Processes can share variables in local memories of processors if they travel among the processors. We present a formal distributed memory model in which a system can be decomposed into processes residing on processors and communicating by message passing or into processes travelling among processors and communicating by shared variables. We call this property communication dualism of distributed systems. We point out that the shared-memory monitor can be used in distributed memory and suggest that variable sharing is a convenient alternative to message passing. We also point out that a mobile agent is a kind of travelling process, but its prominent property, code mobility, is not related to shared-variable communication.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.