CCS expressions, finite state processes, and three problems of equivalence
Paris Christos Kanellakis, Scott A. Smolka · 1983
We examine the computational complexity of testing finite state processes for equivalence, in the Calculus of Communicating Systems (CCS). This equivalence problem in CCS is presented as a refinement of the familiar problem of testing whether two nondeterministic finite state automata (n.f.s.a.) accept the same language. Three notions of equivalence, proposed for CCS, are investigated: (1) observation equivalence, (2) congruence, and (3) failure equivalence. We show that observation equivalence (@@@@) can be tested in cubic time and is the limit of a sequence of equivalence notions (@@@@k), where, @@@@1 is the familiar n.f.s.a. equivalence and, for each fixed k, @@@@k is PSPACE-complete. We provide an O(nlogn) test for congruence for n state processes of bounded fanout, by extending the algorithm that minimizes the states of d.f.s.a.'s. Finally, we show that, even for a very restricted type of process, testing for failure equivalence is PSPACE-complete.