CCS expressions, finite state processes, and three problems of equivalence. (English) Zbl 0705.68063

Summary: 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 defned in CCS, observational equivalence is the limit of a sequence of successively finer equivalence relations, \(\approx_ k\), where \(\approx_ 1\) is nondeterministic finite automaton equivalence. We prove that, for each fixed k, deciding \(\approx_ 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 in PSPACE-complete, even for a very restricted type of process.


68Q25 Analysis of algorithms and problem complexity
68Q05 Models of computation (Turing machines, etc.) (MSC2010)
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
03D15 Complexity of computation (including implicit computational complexity)
Full Text: DOI


[1] Aho, A.V.; Hopcroft, J.E.; Ullman, J.D., ()
[2] Benson, D.B.; Ben-Shachar, O., Bisimulation of automata, Inform. and comput., 79, No. 1, 60-83, (1988) · Zbl 0679.68111
[3] Bergstra, J.A.; Klop, J.W., Algebra of communicating processes, (), 89-138 · Zbl 0605.68013
[4] Bergstra, J.A.; Klop, J.W., (), Report CS-R8725
[5] Brookes, S.D., On the relationship of CCS and CSP, (), 83-96
[6] Brookes, S.D.; Hoare, C.A.R.; Roscoe, A.W., A theory of communicating sequential processes, J. assoc. comput. Mach., 31, No. 3, 560-599, (1984) · Zbl 0628.68025
[7] Brookes, S.D.; Rounds, W.C., Behavioural equivalence relationships induced by programming logics, (), 97-108
[8] {\scChandra, A. K., and Stockmeyer, L. J.} (1982), Private communication.
[9] Coppersmith, D.; Winograd, S., Matrix multiplication via arithmetic progressions, (), 1-6
[10] Hennessy, M.C.B., Acceptance trees, J. assoc. comput. Mach., 34, No. 4, 896-928, (1985) · Zbl 0633.68074
[11] Hennessy, M.C.B.; Milner, R., Algebraic laws for nondeterminism and concurrency, J. assoc. comput. Mach., 32, No. 1, 137-161, (1985) · Zbl 0629.68021
[12] Hopcroft, J.E., An nlogn algorithm for minimizing states in a finite automaton, (), 189-196
[13] Hopcroft, J.E.; Ullman, J.D., ()
[14] Kanellakis, P.C.; Smolka, S.A., CCS expressions, finite state processes, and three problems of equivalence, (), 228-240
[15] Kanellakis, P.C.; Smolka, S.A., On the analysis of cooperation and antagonism in networks of communicating processes, Algorithmica, 3, 421-450, (1988) · Zbl 0636.68023
[16] Milner, R., A calculus of communicating systems, () · Zbl 0452.68027
[17] Milner, R., Calculi for synchrony and asynchrony, Theoret. comput. sci., 25, 267-310, (1983) · Zbl 0512.68026
[18] Milner, R., A complete inference system for a class of regular behaviors, J. comput. system sci., 28, 439-466, (1984) · Zbl 0562.68065
[19] de Nicola, R.; Hennessy, M.C.B., Testing equivalences for processes, Theoret. comput. sci., 34, No. 1, 83-133, (1984) · Zbl 0985.68518
[20] Paige, R.; Tarjan, R.E., Three partition refinement algorithms, SIAM J. comput., 16, No. 6, 973-989, (1987) · Zbl 0654.68072
[21] Salomaa, A., Two complete axiom systems for the algebra of regular events, J. assoc. comput. Mach., 13, No. 1, 158-169, (1986) · Zbl 0149.24902
[22] Sanderson, M.T., (), Internal Report CST-19-82
[23] Smolka, S.A., Analysis of communicating finite-state processes, (), Technical Report CS-84-05
[24] Stockmeyer, L.J.; Meyer, A.R., Word problems requiring exponential time, (), 1-9 · Zbl 0359.68050
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.