Skip to main content
SpringerLink
Log in

Flat Counter Automata Almost Everywhere!

  • Conference paper
Book cover Automated Technology for Verification and Analysis (ATVA 2005)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 3707))

Abstract

This paper argues that flatness appears as a central notion in the verification of counter automata. A counter automaton is called flat when its control graph can be “replaced”, equivalently w.r.t. reachability, by another one with no nested loops. From a practical view point, we show that flatness is a necessary and sufficient condition for termination of accelerated symbolic model checking, a generic semi-algorithmic technique implemented in successful tools like Fast, Lash or TReX. From a theoretical view point, we prove that many known semilinear subclasses of counter automata are flat: reversal bounded counter machines, lossy vector addition systems with states, reversible Petri nets, persistent and conflict-free Petri nets, etc. Hence, for these subclasses, the semilinear reachability set can be computed using a uniform accelerated symbolic procedure (whereas previous algorithms were specifically designed for each subclass).

This work was supported by the French Ministry of Research (Project Persée of the ACI Sécurité et Informatique).

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. Annichini, A., Bouajjani, A., Sighireanu, M.: TReX: A tool for reachability analysis of complex systems. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 368–372. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  2. Araki, T., Kasami, T.: Decidable problems on the strong connectivity of Petri net reachability sets. Theoretical Computer Science 4(1), 99–119 (1977)

    Article  MATH  MathSciNet  Google Scholar 

  3. Bouziane, Z., Finkel, A.: Cyclic petri net reachability sets are semi-linear effectively constructible. In: Proc. 2nd Int. Workshop on Verification of Infinite State Systems (INFINITY 1997), Bologna, Italy, July 1997. Electronic Notes in Theor. Comp. Sci, vol. 9. Elsevier, Amsterdam (1997)

    Google Scholar 

  4. Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: Fast Acceleration of Symbolic Transition systems. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 118–121. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  5. Boigelot, B., Godefroid, P., Willems, B., Wolper, P.: The power of QDDs. In: Van Hentenryck, P. (ed.) SAS 1997. LNCS, vol. 1302, pp. 172–186. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  6. Bouajjani, A., Habermehl, P.: Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations. Theoretical Computer Science 221(1–2), 211–250 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  7. Bouajjani, A., Mayr, R.: Model checking lossy vector addition systems. In: Meinel, C., Tison, S. (eds.) STACS 1999. LNCS, vol. 1563, pp. 323–333. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  8. Boigelot, B.: On iterating linear transformations over recognizable sets of integers. Theoretical Computer Science 309(2), 413–468 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  9. Boigelot, B., Wolper, P.: Symbolic verification with periodic sets. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 55–67. Springer, Heidelberg (1994)

    Google Scholar 

  10. Comon, H., Jurski, Y.: Multiple counters automata, safety analysis and Presburger arithmetic. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 268–279. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  11. Dickson, L.E.: Finiteness of the odd perfect and primitive abundant numbers with r distinct prime factors. Amer. Journal Math. 35, 413–422 (1913)

    Article  MATH  Google Scholar 

  12. Dufourd, C., Jančar, P., Schnoebelen, P.: Boundedness of Reset P/T nets. In: Wiedermann, J., Van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol. 1644, pp. 301–310. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  13. Esparza, J.: Petri nets, commutative context-free grammars, and basic parallel processes. Fundamenta Informaticae 31(1), 13–25 (1997)

    MATH  MathSciNet  Google Scholar 

  14. Finkel, A., Iyer, S.P., Sutre, G.: Well-abstracted transition systems: Application to FIFO automata. Information and Computation 181(1), 1–31 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  15. Finkel, A., Leroux, J.: How to compose Presburger-accelerations: Applications to broadcast protocols. In: Agrawal, M., Seth, A.K. (eds.) FSTTCS 2002. LNCS, vol. 2556, pp. 145–156. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  16. Fribourg, L., Olsén, H.: A decompositional approach for computing least fixed-points of Datalog programs with Z-counters. Constraints 2(3/4), 305–335 (1997)

    Article  MATH  MathSciNet  Google Scholar 

  17. Finkel, A., Sutre, G.: An algorithm constructing the semilinear post * for 2-dim reset/transfer vass. In: Nielsen, M., Rovan, B. (eds.) MFCS 2000. LNCS, vol. 1893, pp. 353–362. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  18. Finkel, A., Sutre, G.: Decidability of reachability problems for classes of two counters automata. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 346–357. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  19. Ginsburg, S., Spanier, E.H.: Semigroups, Presburger formulas and languages. Pacific J. Math. 16(2), 285–296 (1966)

    MATH  MathSciNet  Google Scholar 

  20. Hirshfeld, Y.: Congruences in commutative semigroups. Research report ECS-LFCS-94-291, Laboratory for Foundations of Computer Science, University of Edinburgh, UK (1994)

    Google Scholar 

  21. Hopcroft, J.E., Pansiot, J.-J.: On the reachability problem for 5-dimensional vector addition systems. Theoretical Computer Science 8(2), 135–159 (1979)

    Article  MATH  MathSciNet  Google Scholar 

  22. Ibarra, O.H.: Reversal-bounded multicounter machines and their decision problems. Journal of the ACM 25(1), 116–133 (1978)

    Article  MATH  MathSciNet  Google Scholar 

  23. Kosaraju, S.R.: Decidability of reachability in vector addition systems. In: Proc. 14th ACM Symp. Theory of Computing (STOC 1982), San Francisco, CA, May 1982, pp. 267–281 (1982)

    Google Scholar 

  24. Lash homepage, http://www.montefiore.ulg.ac.be/~boigelot/research/lash/

  25. Latour, L.: From automata to formulas: Convex integer polyhedra. In: Proc. 19th Annual IEEE Symposium on Logic in Computer Science (LICS 2004), Turku, Finland 2004, pp. 120–129. IEEE Comp. Soc. Press, Los Alamitos (2004)

    Chapter  Google Scholar 

  26. Landweber, L.H., Robertson, E.L.: Properties of conflict-free and persistent petri nets. Journal of the ACM 25(3), 352–364 (1978)

    Article  MATH  MathSciNet  Google Scholar 

  27. Leroux, J., Sutre, G.: On flatness for 2-dimensional vector addition systems with states. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 402–416. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  28. Mayr, E.W.: Persistence of vector replacement systems is decidable. Acta Informatica 15, 309–318 (1981)

    Article  MATH  MathSciNet  Google Scholar 

  29. Mayr, E.W.: An algorithm for the general Petri net reachability problem. SIAM J. Comput. 13(3), 441–460 (1984)

    Article  MATH  MathSciNet  Google Scholar 

  30. Minsky, M.L.: Computation: Finite and Infinite Machines, 1st edn. Prentice-Hall, London (1967)

    MATH  Google Scholar 

  31. Taiclin, M.A.: Algorithmic problems for commutative semigroups. Soviet Math. Doklady 9(1), 201–204 (1968)

    MathSciNet  Google Scholar 

  32. Valk, R., Vidal-Naquet, G.: Petri nets and regular languages. Journal of Computer and System Sciences 23(3), 299–325 (1981)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IRISA, Vertecs Project, Campus de Beaulieu, Rennes, France

    Jérôme Leroux

  2. LaBRI, CNRS UMR 5800, Domaine Universitaire, Talence, France

    Grégoire Sutre

Authors
  1. Jérôme Leroux
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Grégoire Sutre
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Bar Ilan University, 52900, Ramat Gan, Israel

    Doron A. Peled

  2. Department of Information Management, National Taiwan University, Taiwan

    Yih-Kuen Tsay

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Leroux, J., Sutre, G. (2005). Flat Counter Automata Almost Everywhere!. In: Peled, D.A., Tsay, YK. (eds) Automated Technology for Verification and Analysis. ATVA 2005. Lecture Notes in Computer Science, vol 3707. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11562948_36

Download citation

  • DOI: https://doi.org/10.1007/11562948_36

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-29209-8

  • Online ISBN: 978-3-540-31969-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation