A modular approach to observational equivalences.

Abstract

One of the fundamental notions in the study of concurrent systems is observational equivalence of processes, in its so-called weak or strong forms. It is mathematically natural, yet it captures the subtleties of process interaction and communication arising in real-life concurrent systems. Both forms of observational equivalence can be defined in terms of the behavior of processes in Milner's Calcullus of Communicating Systems (CCS). The practical importance of CCS is that the implementation and the specification of concurrent systems can be expressed in the same algebraic language reducing the verification problem for concurrent systems to the problem of equality of terms. Complementary to the behavioral representation is an axiomatic characterization of these equivalences. In this thesis, we bring these two characterizations together through a modular formulation of weak equivalence and its associated congruence. This modular formulation is based on simple bisimulations that have a nice characterization both in terms of transition systems and in terms of equational axioms. This effort produces both theoretical and practical results. From the theoretical point of view, we provide a simple proof of completeness for a group of bisimulation congruences--including weak equivalence--on processes using recursion. This proof is, in fact, a proof of completeness for strong congruence, with a slight variation to account for the silent action $\tau$. This way, we have simplified the analysis of observable behavior done in other completeness proofs by Bergstra and Klop, and Milner. This proof can be automatically reused to prove completeness results of equivalences other than weak equivalence. From the practical point of view, the laterial bisimulations have a nice characterization in terms of transition systems; hence an algorithm for the verification of concurrent systems is almost automatically suggested as a variation of the congruence closure algorithm. This algorithm is an alternative to the partition algorithm traditionally used in deciding these equivalences, where verification is carried out efficiently. Moreover, the congruence closure algorithm can be efficiently used to do partial verification in very large systems. We have implemented this algorithm to prove its efficiency, and have used it to verify some mutual exclusion algorithms.