Abstract
We show that any relation between the simulation preorder and bisimilarity is EXPTIME-hard when systems are given as networks of finite state systems (or equivalently as automata with boolean variables, etc.). We also show that any relation between trace inclusion and ready trace equivalence or possible-futures equivalence is EXPSPACE-hard for these systems.
These results match the already known upper bounds and partially answer a conjecture by Rabinovich. They strongly suggest that there is no way to escape the state explosion problem when checking behavioural relations.
For the branching-time relations, our proof uses a new construction that immediately applies to timed automata, a family of systems for which these complexity results are new.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183–235, 1994.
R. Alur, S. Kannan, and M. Yannakakis. Communicating hierarchical state machines. In Proc. 26th Int. Coll. Automata, Languages, and Programming (ICALP’99), Prague, Czech Republic, July 1999, volume 1644 of Lecture Notes in Computer Science, pages 169–178. Springer, 1999.
L. Aceto and F. Laroussinie. Is your model checker on time? In Proc. 24th Int. Symp. Math. Found. Comp. Sci. (MFCS’99), Szklarska Poreba, Poland, Sep. 1999, volume 1672 of Lecture Notes in Computer Science, pages 125–136. Springer, 1999.
H. R. Andersen. Verification of Temporal Properties of Concurrent Systems. PhD thesis, Aarhus University, Denmark, June 1993. Available as DAIMI PB-445.
M. C. Browne, E. M. Clarke, and O. Grumberg. Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science, 59(1–2):115–131, 1988.
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, 1992.
K. Čerāns. Decidability of bisimulation equivalence for parallel timer processes. In Proc. 4th Int. Workshop Computer Aided Verification (CAV’92), Montreal, Canada, June–July 1992, volume 663 of Lecture Notes in Computer Science, pages 302–315. Springer, 1993.
E. M. Clarke, O. Grumberg, and D. Long. Model-checking. In M. Broy, editor, Deductive Program Design, Proc. NATO-ASI Summer School, Marktoberdorf, Germany, 26 July–7 Aug 1994, volume F-152 of NATO ASI-Series. Springer, 1996.
A. K. Chandra, D. C. Kozen, and L. J. Stockmeyer. Alternation. Journal of the ACM, 28(1):114–133, 1981.
J. Esparza. Decidability and complexity of Petri net problems — an introduction. In Advances in Petri Nets 1998, volume 1491 of Lecture Notes in Computer Science, pages 374–428. Springer, 1998.
R. J. van Glabbeek. The linear time — branching time spectrum. In Proc. Theories of Concurrency (CONCUR’90), Amsterdam, NL, Aug. 1990, volume 458 of Lecture Notes in Computer Science, pages 278–297. Springer, 1990.
R. J. van Glabbeek. The linear time — branching time spectrum II: The semantics of sequential systems with silent moves. In Proc. 4th Int. Conf. Concurrency Theory (CONCUR’93), Hildesheim, Germany, Aug. 1993, volume 715 of Lecture Notes in Computer Science, pages 66–81. Springer, 1993.
D. Harel, O. Kupferman, and M. Y. Vardi. On the complexity of verifying concurrent transition systems. In Proc. 8th Int. Conf. Concurrency Theory (CONCUR’97), Warsaw, Poland, Jul. 1997, volume 1243 of Lecture Notes in Computer Science, pages 258–272. Springer, 1997.
P. Jančar. Undecidability of bisimilarity for Petri nets and some related problems. Theoretical Computer Science, 148(2):281–301, 1995.
L. Jategaonkar. Personal communication, August 1999.
L. Jategaonkar and A. R. Meyer. Deciding true concurrency equivalences on safe, finite nets. Theoretical Computer Science, 154(1):107–143, 1996.
O. Kupferman, M. Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking, 1998. Full version of the CAV’94 paper, accepted for publication in J. ACM.
R. Milner. Communication and Concurrency. Prentice Hall Int., 1989.
A. Muscholl, D. Peled, and Z. Su. Deciding properties for message sequence charts. In Proc. Int. Conf. Foundations of Software Science and Computation Structures (FOSSACS’98), Lisbon, Portugal, Mar.–Apr. 1999, volume 1378 of Lecture Notes in Computer Science, pages 226–242. Springer, 1998.
A. J. Mayer and L. J. Stockmeyer. Word problems—this time with interleaving. Information and Computation, 115(2):293–311, 1994.
A. Pnueli. Linear and branching structures in the semantics and logics of reactive systems. In Proc. 12th Coll. Automata, Languages and Programming (ICALP’85), Nafplion, Greece, Jul. 1985, volume 194 of Lecture Notes in Computer Science, pages 15–32. Springer, 1985.
A. Rabinovich. Complexity of equivalence problems for concurrent systems of finite agents. Information and Computation, 139(2):111–129, 1997.
A. Rabinovich. Symbolic model checking for μ-calculus requires exponential time. Tech. report, Dept. Comp. Sci., Tel Aviv University, Israel, August 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Laroussinie, F., Schnoebelen, P. (2000). The State Explosion Problem from Trace to Bisimulation Equivalence. In: Tiuryn, J. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2000. Lecture Notes in Computer Science, vol 1784. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46432-8_13
Download citation
DOI: https://doi.org/10.1007/3-540-46432-8_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67257-9
Online ISBN: 978-3-540-46432-7
eBook Packages: Springer Book Archive