Skip to main content
SpringerLink
Log in

Hardness of Preorder Checking for Basic Formalisms

  • Conference paper
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2010)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 6355))

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  2. Balcázar, J.L., Gabarró, J., Santha, M.: Deciding bisimilarity is p-complete. Formal Asp. Comput. 4(6A), 638–648 (1992)

    Article  MATH  Google Scholar 

  3. Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. Journal of the ACM 28(1), 114–133 (1981)

    Article  MathSciNet  MATH  Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  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. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1984)

    MATH  Google Scholar 

  8. Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley, Reading (1979)

    MATH  Google Scholar 

  9. Jategaonkar, L., Meyer, A.R.: Deciding true concurrency equivalences on safe, finite nets. Theoretical Computer Science 154(1), 107–143 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  12. Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)

    MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  14. Rabinovich, A.M.: Complexity of equivalence problems for concurrent systems of finite agents. Information and Computation 139(2), 111–129 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  15. Sawa, Z., Jančar, P.: Behavioural equivalences on finite-state systems are PTIME-hard. Computing and Informatics 24(5) (2005)

    Google Scholar 

  16. Sawa, Z., Jančar, P.: Hardness of equivalence checking for composed finite-state systems. Acta Informatica 46(3), 169–191 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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 

Download references

Author information

Authors and Affiliations

  1. IRISA, Campus de Beaulieu Cedex, 35042, Rennes, France

    Laura Bozzelli, Axel Legay & Sophie Pinchinat

Authors
  1. Laura Bozzelli
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Axel Legay
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Sophie Pinchinat
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Carnegie Mellon University, USA

    Edmund M. Clarke

  2. School of Computer Science, University of Manchester, Kilburn Building, Oxford Road, M13 9PL, Manchester, UK

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bozzelli, L., Legay, A., Pinchinat, S. (2010). Hardness of Preorder Checking for Basic Formalisms. In: Clarke, E.M., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2010. Lecture Notes in Computer Science(), vol 6355. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17511-4_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-17511-4_8

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-17510-7

  • Online ISBN: 978-3-642-17511-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation