Skip to main content
SpringerLink
Log in

A Comparison of Succinctly Represented Finite-State Systems

  • Conference paper
CONCUR 2012 – Concurrency Theory (CONCUR 2012)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7454))

Included in the following conference series:

Abstract

We study the succinctness of different classes of succinctly presented finite transition systems with respect to bisimulation equivalence. Our results show that synchronized product of finite automata, hierarchical graphs, and timed automata are pairwise incomparable in this sense. We moreover study the computational complexity of deciding simulation preorder and bisimulation equivalence on these classes.

This work has been partly supported by project ImpRo (ANR-10-BLAN-0317).

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. Aceto, L., Ingólfsdóttir, A., Larsen, K.G., Srba, J.: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, NY (2007)

    Book  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  3. Alur, R., Yannakakis, M.: Model checking of hierarchical state machines. ACM Trans. Program. Lang. Syst. 23(3), 273–303 (2001)

    Article  Google Scholar 

  4. Bengtsson, J.E., Yi, W.: Timed Automata: Semantics, Algorithms and Tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  5. Bozzelli, L., Legay, A., Pinchinat, S.: Hardness of Preorder Checking for Basic Formalisms. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 119–135. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  6. Göller, S., Lohrey, M.: Fixpoint logics over hierarchical structures. Theory Comput. Syst. 48(1), 93–131 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  7. Harel, D., Kupferman, O., Vardi, M.Y.: On the complexity of verifying concurrent transition systems. Inf. Comput. 173, 143–161 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  8. Janin, D., Walukiewicz, I.: On the Expressive Completeness of the Propositional mu-Calculus with Respect to Monadic Second Order Logic. In: Montanari, U., Sassone, V. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 263–277. Springer, Heidelberg (1996)

    Chapter  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. Jurdziński, M., Laroussinie, F., Sproston, J.: Model Checking Probabilistic Timed Automata with One or Two Clocks. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 170–184. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  11. Kučera, A., Mayr, R.: Why Is Simulation Harder than Bisimulation? In: Brim, L., Jančar, P., Křetínský, M., Kučera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 594–610. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  12. Kučera, A., Mayr, R.: On the complexity of checking semantic equivalences between pushdown processes and finite-state processes. Information and Computation 208(7), 772–796 (2010)

    Article  MathSciNet  MATH  Google Scholar 

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

  14. Lengauer, T., Wanke, E.: Efficient solution of connectivity problems on hierarchically defined graphs. SIAM J. Comput. 17(6), 1063–1080 (1988)

    Article  MathSciNet  MATH  Google Scholar 

  15. Lohrey, M.: Model-checking hierarchical structures. J. Comput. Syst. Sci. 78(2), 461–490 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  16. Moller, F., Rabinovich, A.M.: Counting on CTL*: on the expressive power of monadic path logic. Inf. Comput. 184(1), 147–159 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  17. Muscholl, A., Walukiewicz, I.: A lower bound on web services composition. Logical Methods in Computer Science 4(2) (2008)

    Google Scholar 

  18. Srba, J.: Comparing the Expressiveness of Timed Automata and Timed Extensions of Petri Nets. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 15–32. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  19. van Benthem, J.: Modal Correspondence Theory. PhD thesis, University of Amsterdam (1976)

    Google Scholar 

  20. van Glabbeek, R.J.: The Linear Time-Branching Time Spectrum (Extended Abstract). In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 278–297. Springer, Heidelberg (1990)

    Google Scholar 

  21. van Glabbeek, R.J.: The Linear Time - Branching Time Spectrum II. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 66–81. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LSV, CNRS & ENS Cachan, France

    Romain Brenguier & Ocan Sankur

  2. Institut für Informatik, Universität Bremen, Germany

    Stefan Göller

Authors
  1. Romain Brenguier
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Stefan Göller
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Ocan Sankur
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computing Science, Newcastle University, Claremont Tower, Claremont Road, NE1 7RU, Newcastle upon Tyne, UK

    Maciej Koutny

  2. Department of Computer Science, University of Leicester, Computer Science Building, University Road, LE1 7RH, Leicester, UK

    Irek Ulidowski

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Brenguier, R., Göller, S., Sankur, O. (2012). A Comparison of Succinctly Represented Finite-State Systems. In: Koutny, M., Ulidowski, I. (eds) CONCUR 2012 – Concurrency Theory. CONCUR 2012. Lecture Notes in Computer Science, vol 7454. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32940-1_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-32940-1_12

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-32939-5

  • Online ISBN: 978-3-642-32940-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation