Skip to main content
SpringerLink
Log in

The Ideal View on Rackoff’s Coverability Technique

  • Conference paper
  • First Online:
Reachability Problems (RP 2015)

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

Included in the following conference series:

Abstract

Rackoff’s small witness property for the coverability problem is the standard means to prove tight upper bounds in vector addition systems (VAS) and many extensions. We show how to derive the same bounds directly on the computations of the VAS instantiation of the generic backward coverability algorithm. This relies on a dual view of the algorithm using ideal decompositions of downwards-closed sets, which exhibits a key structural invariant in the VAS case. The same reasoning readily generalises to several VAS extensions.

Work funded in part by the Leverhulme Trust Visiting Professorship VP1-2014-041, and the EPSRC grant EP/M011801/1.

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 34.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 44.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. Abdulla, P.A., Čerāns, K., Jonsson, B., Tsay, Y.K.: Algorithmic analysis of programs with well quasi-ordered domains. Inform. and Comput. 160(1/2), 109–127 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  2. Blondin, M., Finkel, A., McKenzie, P.: Handling infinitely branching WSTS. In: Esparza, J., Fraigniaud, P., Husfeldt, T., Koutsoupias, E. (eds.) ICALP 2014, Part II. LNCS, vol. 8573, pp. 13–25. Springer, Heidelberg (2014)

    Google Scholar 

  3. Bonnet, R., Finkel, A., Praveen, M.: Extending the Rackoff technique to affine nets. FSTTCS 2012. LIPIcs, vol. 18, pp. 301–312. LZI (2012)

    Google Scholar 

  4. Bonnet, R.: On the cardinality of the set of initial intervals of a partially ordered set. Infinite and finite sets: to Paul Erdős on his 60th birthday, vol. 1, pp. 189–198. Coll. Math. Soc. János Bolyai, North-Holland (1975)

    Google Scholar 

  5. Bozzelli, L., Ganty, P.: Complexity analysis of the backward coverability algorithm for VASS. In: Delzanno, G., Potapov, I. (eds.) RP 2011. LNCS, vol. 6945, pp. 96–109. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  6. Courtois, J.-B., Schmitz, S.: Alternating vector addition systems with states. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds.) MFCS 2014, Part I. LNCS, vol. 8634, pp. 220–231. Springer, Heidelberg (2014)

    Google Scholar 

  7. Demri, S., Jurdziński, M., Lachish, O., Lazić, R.: The covering and boundedness problems for branching vector addition systems. J. Comput. Syst. Sci. 79(1), 23–38 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  8. Figueira, D., Figueira, S., Schmitz, S., Schnoebelen, P.: Ackermannian and primitive-recursive bounds with Dickson’s Lemma. In: LICS 2011, pp. 269–278. IEEE Computer Society (2011)

    Google Scholar 

  9. Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere!. Theor. Comput. Sci. 256(1–2), 63–92 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  10. Finkel, A., Goubault-Larrecq, J.: Forward analysis for WSTS, part I: Completions. In: Proc. STACS 2009. LIPIcs, vol. 3, pp. 433–444. LZI (2009)

    Google Scholar 

  11. Goubault-Larrecq, J., Karandikar, P., Narayan Kumar, K., Schnoebelen, P.: The ideal approach to computing closed subsets in well-quasi-orderings (in preparation) (2015)

    Google Scholar 

  12. Kochems, J., Ong, C.H.L.: Decidable models of recursive asynchronous concurrency (2015) (preprint) http://arxiv.org/abs/1410.8852

  13. Lazić, R., Schmitz, S.: Non-elementary complexities for branching VASS, MELL, and extensions. ACM Trans. Comput. Logic 16(3:20), 1–30 (2015)

    Google Scholar 

  14. Lipton, R.: The reachability problem requires exponential space. Tech. Rep. 62, Yale University (1976)

    Google Scholar 

  15. Majumdar, R., Wang, Z.: Expand, Enlarge, and Check for Branching Vector Addition Systems. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013 – Concurrency Theory. LNCS, vol. 8052, pp. 152–166. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  16. Rackoff, C.: The covering and boundedness problems for vector addition systems. Theor. Comput. Sci. 6(2), 223–231 (1978)

    Article  MathSciNet  MATH  Google Scholar 

  17. Schmitz, S.: Complexity hierarchies beyond Elementary (2013) (preprint) http://arxiv.org/abs/1312.5686

  18. Schmitz, S., Schnoebelen, P.: Algorithmic aspects of WQO theory. Lecture notes (2012). http://cel.archives-ouvertes.fr/cel-00727025

  19. Schnoebelen, P.: Revisiting Ackermann-hardness for lossy counter machines and reset Petri nets. In: Hliněný, P., Kučera, A. (eds.) MFCS 2010. LNCS, vol. 6281, pp. 616–628. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DIMAP, Department of Computer Science, University of Warwick, Coventry, UK

    Ranko Lazić & Sylvain Schmitz

  2. LSV, ENS Cachan and CNRS and INRIA, Cachan, France

    Sylvain Schmitz

Authors
  1. Ranko Lazić
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sylvain Schmitz
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sylvain Schmitz .

Editor information

Editors and Affiliations

  1. The Institute of Informatics, University of Warsaw, Warsaw, Poland

    Mikolai Bojanczyk

  2. The Institute of Informatics, University of Warsaw, Warsaw, Poland

    Slawomir Lasota

  3. University of Liverpool, Liverpool, United Kingdom

    Igor Potapov

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Lazić, R., Schmitz, S. (2015). The Ideal View on Rackoff’s Coverability Technique. In: Bojanczyk, M., Lasota, S., Potapov, I. (eds) Reachability Problems. RP 2015. Lecture Notes in Computer Science(), vol 9328. Springer, Cham. https://doi.org/10.1007/978-3-319-24537-9_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-24537-9_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-24536-2

  • Online ISBN: 978-3-319-24537-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation