Analysis of communicating finite-state processes
Scott A. Smolka · 1984
In this thesis we analyze a subclass of message-passing programs that can be modeled algebraically as networks of Finite-State Processes (FSPs). These networks form a subset of the systems describable in Milners CCS, and are used as a semantics for a regular subset of Hoare's CSP. We show that the Synchronization Analysis Problem, which subsumes the notion of deadlock, is NP-complete even for networks of constant-size tree processes, and identify a non-trivial subclass of networks for which the problem can be decided in polynomial time. We analyze the complexity of testing various notions of equivalence of FSPs, namely observation equivalence, congruence, and failure equivalence. Decision procedures for these equivalences, which can be used to verify that a finite-state message-passing program meets its specification, are developed. It is shown that observation equivalence, (DBLTURN), can be tested in cubic time. Moreover, observation equivalence is the limit of a sequence of successively finer equivalence relations, (DBLTURN)(,k), each of which is PSPACE-complete. We provide an O(n log n) test for congruence of n-state FSPs of bounded fanout by extending Hopcroft's algorithm for minimizing the number of states of a DFA. Finally, we show that testing for failure equivalence is PSPACE-complete, even for a very restricted type of FSP. We illustrate our procedures for synchronization analysis and verification by appliction to network protocols.