CCS expressions, finite state processes, and three problems of equivalence

We examine the computational complexity of testing finite state processes for equivalence in Milner's Calculus of Communicating Systems (CCS). The equivalence problems in CCS are presented as refinements of the familiar problem of testing whether two nondeterministic finite automata (NFA) are equivalent, i.e., accept the same language. Three notions of equivalence proposed for CCS are investigated, namely, observational equivalence, strong observational equivalence, and failure equivalence. We show that observational equivalence can be tested in polynomial time. As defined in CCS, observational equivalence is the limit of a sequence of successively finer equivalence relations, ≈_k, where ≈₁ is nondeterministic finite automaton equivalence. We prove that, for each fixed k, deciding ≈_k is PSPACE-complete. We show that strong observational equivalence can be decided in polynomial time by reducing it to generalized partitioning, a new combinatorial problem of independent interest. Finally, we demonstrate that testing for failure equivalence is PSPACE-complete, even for a very restricted type of process.