On deciding trace equivalences for processes. (English) Zbl 0783.68043

Summary: We investigate the complexity of deciding trace, maximal trace and \(\omega\)-equivalences for finite state processes and recursively defined processes specified by normed context-free grammars (CFGs) in Greibach normal form (GNF). The main results are as follows:
(1) Trace, maximal trace and \(\omega\)-trace equivalences for processes specified by normed GNF CFGs are all undecidable. For this class of processes, the regularity problem with respect to trace, maximal trace or \(\omega\)-trace equivalence is also undecidable. Moreover, all these undecidability results hold even for locally unary processes. For processes specified by unary GNF CFGs, the maximal trace equivalence is \(\prod^ p_ 2\)-complete while the \(\omega\)-trace equivalence is \(NL\)- complete and the trace equivalence is decidable in polynomial time by a dynamic programming algorithm.
(2) Trace, maximal trace and \(\omega\)-trace equivalences for finite state processes are PSPACE-complete. This holds even for locally unary finite state processes. For unary finite state processes, the maximal trace equivalence is co-\(NP\)-complete while trace and \(\omega\)-trace equivalences are \(NL\)-complete.


68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
68Q55 Semantics in the theory of computing
Full Text: DOI


[1] Baeten, J.C.M.; Bergstra, J.A.; Klop, J.W., Decidability of bisimulation equivalence for processes generating context-free languages, (), 82-95 · Zbl 0635.68014
[2] Bergstra, J.A.; Klop, J.W., Process algebra for synchronous communication, Inform. control, 60, 109-137, (1984) · Zbl 0597.68027
[3] Bergstra, J.A.; Klop, J.W.; Oldreog, E.R., Readies and failures in the algebra of communicating processes, SIAM J. comput., 17, 1134-1177, (1988) · Zbl 0677.68089
[4] Brookes, S.D.; Hoare, C.A.R.; Roscoe, W., A theory of communicating sequential processes, J. assoc. comput. math., 31, 560-599, (1984) · Zbl 0628.68025
[5] Clarke, E.M.; Browne, I.A.; Kurshan, R.P., A unified approach for showing language containment and equivalence between various types of ω-automata, (), 103-116 · Zbl 0759.68063
[6] Cook, S.A., A taxonomy of problems with fast parallel algorithms, Inform. control, 64, 2-22, (1985) · Zbl 0575.68045
[7] Garey, M.R.; Johnson, D.S., Computers and intractability: A guide to the theory of NP-completeness, (1979), Freeman New York · Zbl 0411.68039
[8] Harrison, M.A., Introduction to formal language theory, (1978), Addison-Wesley Reading, Mass · Zbl 0411.68058
[9] Hoare, C.A.R., Communicating sequential processes, (1985), Prentice-Hall Englewood Cliffs, N.J · Zbl 0637.68007
[10] Hoogeboom, H.J.; Rozenberg, G., Infinitary languages: basic theory and applications to concurrent systems, (), 266-342 · Zbl 0607.68059
[11] Hopcroft, J.E.; Ullman, J.D., Introduction to automata theory, languages and computation, (1979), Addison-Wesley Reading, Mass · Zbl 0196.01701
[12] Huynh, D.T., Deciding the inequivalence of context-free grammars with 1-letter terminal alphabet is σ2p-complete, Theoret. comput. sci., 33, 305-326, (1984) · Zbl 0556.68040
[13] Huynh, D.T.; Tian, L., On deciding readiness and failure equivalences for processes, (), 738-745
[14] Huynh, D.T.; Tian, L., On some equivalence relations for probabilistic processes, (), To appear in Fundamenta Informaticae. · Zbl 0766.68099
[15] Kanellakis, P.C.; Smolka, S.A., CCS expressions, finite state processes and three problems of equivalences, Inform. comput., 86, 43-68, (1990) · Zbl 0705.68063
[16] Milner, R., Communication and concurrency, (1989), Prentice-Hall Englewood Cliffs, N.J · Zbl 0683.68008
[17] de Nicola, R.; Hennessey, M.C.B., Testing equivalences for processes, Theoret. comput. sci., 34, 83-133, (1984) · Zbl 0985.68518
[18] Olderog, E.R.; Hoare, C.A.R., Specification-oriented semantics for communicating processes, Acta informatica, 23, 9-66, (1986) · Zbl 0569.68019
[19] Safra, S., On the complexity of ω-automata, (), 319-327
[20] Sistla, A.P.; Vardi, M.Y.; Wolper, P., The complementation problem for Büchi automata with applications to temporal logic, Theoret. comput. sci., 49, 217-237, (1987) · Zbl 0613.03015
[21] Stockmeyer, L.J., The polynomial-time hierarchy, Theoret. comput. sci., 3, 1-22, (1977) · Zbl 0353.02024
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.