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

ABSTRACT

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.

REFERENCES

• 1: Alfred V. Aho , John E. Hopcroft, The Design and Analysis of Computer Algorithms, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1974
• 2: S.D. Brookes, "On the Relationship of CCS and CSP", technical report, Department of Computer Science, Carnegie-Mellon University, (1982).
• 3: A.K. Chandra, L.J. Stockmeyer, private communication (July 1982).
• 4: J. Hopcroft, "An n log n Algorithm for Minimizing States in a Finite Automaton", in Theory of Machines and Computations, pp. 189-196, Eds. Z. Kohavi and A. Paz, Academic Press, New York (1971).
• 5: C.A.R. Hoare, S.D. Brookes, A.W. Roscoe, "A Theory of Communicating Sequential Processes", Technical Monograph PRG-16, Oxford University Computing Laboratory, Programming Research Group, Oxford, England (May 1981).
• 6: John E. Hopcroft , Jeffrey D. Ullman, Introduction To Automata Theory, Languages, And Computation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• 7: R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
• 8: R. Milner, "A Complete Inference System for a Class of Regular Behaviors", Department of Computer Science, University of Edinburgh, Internal Report CSR-111-82 (April 1982).
• 9: Robin Milner, Four combinators for concurrency, Proceedings of the first ACM SIGACT-SIGOPS symposium on Principles of distributed computing, p.104-110, August 18-20, 1982, Ottawa, Canada [doi>10.1145/800220.806687]
• 10: Arto Salomaa, Two Complete Axiom Systems for the Algebra of Regular Events, Journal of the ACM (JACM), v.13 n.1, p.158-169, Jan. 1966 [doi>10.1145/321312.321326]
• 11: S.A. Smolka, Ph.D. Dissertation
• 12: M.T. Sanderson, "Proof Techniques for CCS", Department of Computer Science, University of Edinburgh, Internal Report CST 19-82 (Nov. 1982).
• 13: L. J. Stockmeyer , A. R. Meyer, Word problems requiring exponential time(Preliminary Report), Proceedings of the fifth annual ACM symposium on Theory of computing, p.1-9, April 30-May 02, 1973, Austin, Texas, United States [doi>10.1145/800125.804029]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Automata (e.g., finite, push-down, resource-bounded)

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Computability theory

General Terms:
Theory