When reasoning about systems of parallel processes, verifying global properties requires construction of the global state space, whose size is typically exponential in the number of processes. Avoiding this state explosion is a central problem in the study of logics for distributed systems. A number of researchers have been studying this problem, and this paper makes a valuable contribution to this area.
If a model checker wishes to avoid constructing the global state space, it should check not that a component satisfies a property in a given system, but that the property holds for all systems containing that component. The authors provide a strategy for doing this as follows. They define a preorder ≤ on structures such that M ∥ M′ ≤ M , and whenever M 1 ≤ M 2 , ( M ∥ M 1 ) ≤ ( M ∥ M 2 ). They identify a sublogic of CTL* such that for a formula &fgr; in that logic, whenever M ≤ M′, if M′ ⊧ &fgr;, then we also have that M ⊧ &fgr;. Now, to check that ( M ∥ M′ ) ⊧ &fgr;, we proceed as follows: we show that M guarantees a property A 1, that M′ under the assumption of A 1 guarantees property A 2, and that M under the assumption of A 2 satisfies &fgr;. The assumption guarantee properties themselves could be specified as formulas of the logic or structures.
The sublogic of CTL* suggested by the authors is simply CTL* omitting the existential path quantifier. For this logic, standard model checking algorithms are available for answering the following question: is a formula true for all systems containing a specified component? In other words, the semantics of the logic respects the preorder above, and M ⊧ &fgr; if and only if M ≤ T ( &fgr; ), where T is the structure given by the tableau of &fgr;.
The use of Moore machines as temporal structures in the paper is noteworthy, because they are most suitable for modeling synchronous circuits, for which the authors suggest the proposed branching-time logic as a specification formalism.
The paper also discusses an implementation of the model checker using the controller of a simple CPU as an example.
