Hardness of Preorder Checking for Basic Formalisms

  • Laura Bozzelli
  • Axel Legay
  • Sophie Pinchinat
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6355)


We investigate the complexity of preorder checking when the specification is a flat finite-state system whereas the implementation is either a non-flat finite-state system or a standard timed automaton. In both cases, we show that simulation checking is Exptime-hard, and for the case of a non-flat implementation, the result holds even if there is no synchronization between the parallel components and their alphabets of actions are pairwise disjoint. Moreover, we show that the considered problems become Pspace-complete when the specification is assumed to be deterministic. Additionally, we establish that comparing a synchronous non-flat system with no hiding and a flat system is Pspace-hard for any relation between trace containment and bisimulation equivalence.


Turing Machine Label Transition System Valuation Tree Size Polynomial Partial Path 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Balcázar, J.L., Gabarró, J., Santha, M.: Deciding bisimilarity is p-complete. Formal Asp. Comput. 4(6A), 638–648 (1992)CrossRefzbMATHGoogle Scholar
  3. 3.
    Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. Journal of the ACM 28(1), 114–133 (1981)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Kupferman, O., Harel, D., Vardi, M.Y.: On the complexity of verifying concurrent transition systems. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 258–272. Springer, Heidelberg (1997)Google Scholar
  5. 5.
    Groote, J.F., Moller, F.: Verification of parallel systems via decomposition. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 62–76. Springer, Heidelberg (1992)CrossRefGoogle Scholar
  6. 6.
    Henzinger, M.R., Henzinger, T.A., Kopke, P.W.: Computing simulations on finite and infinite graphs. In: Proc. 36th FOCS, pp. 453–462. IEEE Computer Society, Los Alamitos (1995)Google Scholar
  7. 7.
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1984)zbMATHGoogle Scholar
  8. 8.
    Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley, Reading (1979)zbMATHGoogle Scholar
  9. 9.
    Jategaonkar, L., Meyer, A.R.: Deciding true concurrency equivalences on safe, finite nets. Theoretical Computer Science 154(1), 107–143 (1996)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Kučera, A., Jančar, P.: Equivalence-checking on infinite-state systems: Techniques and results. Theory and Practice of Logic Programming 6(3), 227–264 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Laroussinie, F., Schnoebelen, P.: The state explosion problem from trace to bisimulation equivalence. In: Tiuryn, J. (ed.) FOSSACS 2000. LNCS, vol. 1784, pp. 192–207. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  12. 12.
    Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)zbMATHGoogle Scholar
  13. 13.
    Muscholl, A., Walukiewicz, I.: A lower bound on web services composition. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol. 4423, pp. 274–286. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  14. 14.
    Rabinovich, A.M.: Complexity of equivalence problems for concurrent systems of finite agents. Information and Computation 139(2), 111–129 (1997)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Sawa, Z., Jančar, P.: Behavioural equivalences on finite-state systems are PTIME-hard. Computing and Informatics 24(5) (2005)Google Scholar
  16. 16.
    Sawa, Z., Jančar, P.: Hardness of equivalence checking for composed finite-state systems. Acta Informatica 46(3), 169–191 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Shukla, S.K., Hunt III, H.B., Rosenkrantz, D.J., Stearns, R.E.: On the complexity of relational problems for finite state processes. In: Meyer auf der Heide, F., Monien, B. (eds.) ICALP 1996. LNCS, vol. 1099, pp. 466–477. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  18. 18.
    Tasiran, S., Alur, R., Kurshan, R.P., Brayton, R.K.: Verifying abstractions of timed systems. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 546–562. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  19. 19.
    Čerāns, K.: Decidability of bisimulation equivalences for parallel timer processes. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, pp. 302–315. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  20. 20.
    Valmari, A., Kervinen, A.: Alphabet-based synchronisation is exponentially cheaper. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 161–176. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  21. 21.
    van Glabbeek, R.J.: The linear time-branching time spectrum. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 278–297. Springer, Heidelberg (1990)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Laura Bozzelli
    • 1
  • Axel Legay
    • 1
  • Sophie Pinchinat
    • 1
  1. 1.IRISARennesFrance

Personalised recommendations