×

zbMATH — the first resource for mathematics

Hardness of equivalence checking for composed finite-state systems. (English) Zbl 1166.68018
Summary: Computational complexity of comparing behaviours of systems composed from interacting finite-state components is considered. The main result shows that the respective problems are EXPTIME-hard for all relations between bisimulation equivalence and trace preorder, as conjectured by A. Rabinovich [Inf. Comput. 139, No. 2, 111–129 (1997; Zbl 0892.68061)]. The result is proved for a specific model of parallel compositions where the components synchronize on shared actions but it can be easily extended to other similar models, to labelled 1-safe Petri nets. Further hardness results are shown for special cases of acyclic systems.

MSC:
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Balcázar J., Gabarró J., Sántha M.: Deciding bisimilarity is P-complete. Formal Aspects Comput. 4(6A), 638–648 (1992) · Zbl 0758.68033 · doi:10.1007/BF03180566
[2] Chandra A.K., Kozen D.C., Stockmeyer L.J.: Alternation. J. ACM. 28(1), 114–133 (1981) · Zbl 0473.68043 · doi:10.1145/322234.322243
[3] van Glabbeek R.: Handbook of process algebra. In: Bergstra, J., Ponse, A., Smolka, S. (eds.) Handbook of Process Algebra, chap. The Linear Time–Branching Time Spectrum, pp. 3–99. Elsevier, Amsterdam (2001) · Zbl 1035.68073
[4] Groote, J.F., Moller, F.: Verification of parallel systems via decomposition. In: Proceedings of Third International Conference on Concurrency Theory. Lecture Notes in Computer Science, vol. 630, pp. 62–76. Springer, Heidelberg (1992)
[5] Hoare C.A.R.: Communcating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985) · Zbl 0637.68007
[6] Immerman, N.: Descriptive Complexity, pp. 53–54. Springer, Heidelberg (1998) · Zbl 0945.03546
[7] Jančar, P., Srba, J.: Undecidability of bisimilarity by Defender’s forcing. J. ACM. 55(1) (2008) · Zbl 1326.68199
[8] Kanellakis P.C., Smolka S.A.: CCS expressions, finite state processes, and three problems of equivalence. Inf. Comput. 86(1), 43–68 (1990) · Zbl 0705.68063 · doi:10.1016/0890-5401(90)90025-D
[9] Laroussinie, F., Schnoebelen, P.: The state explosion problem from trace to bisimulation equivalence. In: Proceedings of the 3rd International Conference Foundations of Software Science and Computation Structures (FOSSACS’2000), Berlin, Germany, March–April 2000. Lecture Notes in Computer Science, vol. 1784, pp. 192–207. Springer, Heidelberg (2000) · Zbl 0961.68090
[10] Mansfield, A.: On the computational complexity of a merge recognition problem. DAMATH: Discrete Appl. Math. Combin. Oper. Res. Comput. Sci. 5, 119–122 (1983) · Zbl 0496.68028
[11] Meyer, A.R., Stockmeyer, L.J.: The equivalence problem for regular expressions with squaring requires exponential space. In: 13th Annual Symposium on Switching and Automata Theory, pp. 125–129. IEEE, New York (1972)
[12] Milner R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989) · Zbl 0683.68008
[13] Paige R., Tarjan R.E.: Three partition refinement algorithms. SIAM J. Comput. 16(6), 973–989 (1987) · Zbl 0654.68072 · doi:10.1137/0216062
[14] Rabinovich A.: Complexity of equivalence problems for concurrent systems of finite agents. Inf. Comput. 139(2), 111–129 (1997) · Zbl 0892.68061 · doi:10.1006/inco.1997.2661
[15] Sawa, Z.: Equivalence checking of non-flat systems is EXPTIME-hard. In: Proceedings of CONCUR 2003. Lecture Notes in Computer Science, vol. 2761, pp. 237–250. Springer, Heidelberg (2003) · Zbl 1274.68134
[16] Sawa Z., Jančar P.: Behavioural equivalences on finite-state systems are PTIME-hard. Comput. Inform. 24(5), 513–528 (2005) · Zbl 1109.68052
[17] Shukla, S.K., Hunt, H.B., Rosenkrantz, D.J., Stearns, R.E.: On the complexity of relational problems for finite state processes. In: Proceedings of ICALP’96. Lecture Notes in Computer Science, vol. 1099, pp. 466–477. Springer, Heidelberg (1996) · Zbl 1046.68627
[18] Valmari, A., Kervinen, A.: Alphabet-based synchronisation is exponentially cheaper. In: Proceedings of CONCUR 2002. Lecture Notes in Computer Science, vol. 2421, pp. 161–176 (2002) · Zbl 1012.68123
[19] Warmuth M.K., Haussler D.: On the complexity of iterated shuffle. J. Comp. Syst. Sci. 28(3), 345–358 (1984) · Zbl 0549.68039 · doi:10.1016/0022-0000(84)90018-7
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.