×

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.

MSC:

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)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Aho, A. V.; Hopcroft, J. E.; Ullman, J. D., (The Design and Analysis of Computer Algorithms (1974), Addison-Wesley: Addison-Wesley Reading, MA) · Zbl 0326.68005
[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, (de Bakker, J. W.; Hazewinkel, M.; Lenstra, J. K., CWI Monographs I, Proceedings of the CWI Symposium on Mathematics and Computer Science (1986), North-Holland: North-Holland Amsterdam), 89-138 · Zbl 0605.68013
[4] Bergstra, J. A.; Klop, J. W., \((ACP_τ\): A Universal Axiom System for Process Specification (1987), Computer Science/Department of Software Technology, CWI: Computer Science/Department of Software Technology, CWI Amsterdam, The Netherlands), Report CS-R8725
[5] Brookes, S. D., On the relationship of CCS and CSP, (Proceedings, 10th International Conference on Automata, Languages, and Programming. Proceedings, 10th International Conference on Automata, Languages, and Programming, Barcelona, Spain. Proceedings, 10th International Conference on Automata, Languages, and Programming. Proceedings, 10th International Conference on Automata, Languages, and Programming, Barcelona, Spain, Lecture Notes in Computer Science, Vol. 154 (1983), Springer-Verlag: Springer-Verlag New York/Berlin), 83-96 · Zbl 0516.68024
[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, (Proceedings, 10th International Conference on Automata, Languages, and Programming. Proceedings, 10th International Conference on Automata, Languages, and Programming, Barcelona, Spain. Proceedings, 10th International Conference on Automata, Languages, and Programming. Proceedings, 10th International Conference on Automata, Languages, and Programming, Barcelona, Spain, Lecture Notes in Computer Science, Vol. 154 (1983), Springer-Verlag: Springer-Verlag New York/Berlin), 97-108
[8] Chandra, A. K., and Stockmeyer, L. J.; Chandra, A. K., and Stockmeyer, L. J.
[9] Coppersmith, D.; Winograd, S., Matrix multiplication via arithmetic progressions, (Proceedings, 19th ACM Symposium on Theory of Computing. Proceedings, 19th ACM Symposium on Theory of Computing, New York (1987)), 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 \(n\) log \(n\) algorithm for minimizing states in a finite automaton, (Kohavi, Z.; Paz, A., Theory of Machines and Computations (1971), Academic Press: Academic Press San Diego, CA/New York), 189-196
[13] Hopcroft, J. E.; Ullman, J. D., (Introduction to Automata Theory, Languages, and Computation (1979), Addison-Wesley: Addison-Wesley Reading, MA) · Zbl 0426.68001
[14] Kanellakis, P. C.; Smolka, S. A., CCS expressions, finite state processes, and three problems of equivalence, (Proceedings, 2nd Annual ACM Symposium on Principles of Distributed Computing. Proceedings, 2nd Annual ACM Symposium on Principles of Distributed Computing, Montreal, Canada (1983)), 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, (Lecture Notes in Computer Science, Vol. 92 (1980), Springer-Verlag: Springer-Verlag New York, Berlin) · 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., (Proof Techniques for CCS (1982), Department of Computer Science, University of Edinburgh), Internal Report CST-19-82
[23] Smolka, S. A., Analysis of Communicating Finite-State Processes, (Ph. D. dissertation (1984), Department of Computer Science, Brown University: Department of Computer Science, Brown University Providence, RI), Technical Report CS-84-05
[24] Stockmeyer, L. J.; Meyer, A. R., Word problems requiring exponential time, (Proceedings, 5th ACM Symposium on Theory of Computing. Proceedings, 5th ACM Symposium on Theory of Computing, Austin, Texas (1973)), 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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.