Document Open Access Logo

Invariants for One-Counter Automata with Disequality Tests

Authors Dmitry Chistikov , Jérôme Leroux, Henry Sinclair-Banks , Nicolas Waldburger

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2024.17.pdf
  • Filesize: 0.94 MB
  • 21 pages

Document Identifiers

Author Details

Dmitry Chistikov
  • Centre for Discrete Mathematics and its Applications (DIMAP) & Department of Computer Science, University of Warwick, Coventry, UK
Jérôme Leroux
  • LaBRI, CNRS, Univ. Bordeaux, France
Henry Sinclair-Banks
  • Centre for Discrete Mathematics and its Applications (DIMAP) & Department of Computer Science, University of Warwick, Coventry, UK
Nicolas Waldburger
  • IRISA, Université de Rennes, France

Funding

  • Chistikov, Dmitry: Supported in part by the Engineering and Physical Sciences Research Council [EP/X03027X/1].
  • Sinclair-Banks, Henry: Supported by EPSRC Standard Research Studentship (DTP), grant number EP/T51794X/1. Also supported in part by the International Emerging Actions grant (IEA'22) and by the ANR grant VeSyAM (ANR-22-CE48-0005).
  • Waldburger, Nicolas: Supported in part by the International Emerging Actions grant (IEA'22) and by the ANR grant VeSyAM (ANR-22-CE48-0005).

Acknowledgements

We would like to thank Mahsa Shirmohammadi, without whom this work would not have been possible, for many ideas and encouragement. We are also grateful to Thomas Colcombet, Rayna Dimitrova, and James Worrell for useful discussions.

Cite AsGet BibTex

Dmitry Chistikov, Jérôme Leroux, Henry Sinclair-Banks, and Nicolas Waldburger. Invariants for One-Counter Automata with Disequality Tests. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 17:1-17:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CONCUR.2024.17

Abstract

We study the reachability problem for one-counter automata in which transitions can carry disequality tests. A disequality test is a guard that prohibits a specified counter value. This reachability problem has been known to be NP-hard and in PSPACE, and characterising its computational complexity has been left as a challenging open question by Almagor, Cohen, Pérez, Shirmohammadi, and Worrell (2020). We reduce the complexity gap, placing the problem into the second level of the polynomial hierarchy, namely into the class coNP^NP. In the presence of both equality and disequality tests, our upper bound is at the third level, P^NP^NP. To prove this result, we show that non-reachability can be witnessed by a pair of invariants (forward and backward). These invariants are almost inductive. They aim to over-approximate only a "core" of the reachability set instead of the entire set. The invariants are also leaky: it is possible to escape the set. We complement this with separate checks as the leaks can only occur in a controlled way.

Subject Classification

ACM Subject Classification
  • Theory of computation → Models of computation
Keywords
  • Inductive invariant
  • Vector addition system
  • One-counter automaton

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Shaull Almagor, Nathann Cohen, Guillermo A. Pérez, Mahsa Shirmohammadi, and James Worrell. Coverability in 1-VASS with disequality tests. In Igor Konnov and Laura Kovács, editors, 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), volume 171 of LIPIcs, pages 38:1-38:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. Google Scholar
  2. Rajeev Alur and Pavol Černý. Streaming transducers for algorithmic verification of single-pass list-processing programs. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, pages 599-610, 2011. Google Scholar
  3. Nicolas Amat, Silvano Dal-Zilio, and Thomas Hujsa. Property directed reachability for generalized Petri nets. In Dana Fisman and Grigore Rosu, editors, Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I, volume 13243 of Lecture Notes in Computer Science, pages 505-523. Springer, 2022. Google Scholar
  4. Pascal Baumann, Moses Ganardi, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche. Context-bounded verification of context-free specifications. Proc. ACM Program. Lang., 7(POPL):2141-2170, 2023. Google Scholar
  5. Michael Blondin, Matthias Englert, Alain Finkel, Stefan Göller, Christoph Haase, Ranko Lazic, Pierre McKenzie, and Patrick Totzke. The reachability problem for two-dimensional vector addition systems with states. J. ACM, 68(5):34:1-34:43, 2021. Google Scholar
  6. Michael Blondin, Alain Finkel, Christoph Haase, and Serge Haddad. Approaching the coverability problem continuously. In Marsha Chechik and Jean-François Raskin, editors, Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9636 of Lecture Notes in Computer Science, pages 480-496. Springer, 2016. Google Scholar
  7. Michael Blondin, Alain Finkel, Christoph Haase, and Serge Haddad. The logical view on continuous Petri nets. ACM Trans. Comput. Log., 18(3):24:1-24:28, 2017. Google Scholar
  8. Michael Blondin, Christoph Haase, and Philip Offtermatt. Directed reachability for infinite-state systems. In Jan Friso Groote and Kim Guldstrand Larsen, editors, Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II, volume 12652 of Lecture Notes in Computer Science, pages 3-23. Springer, 2021. Google Scholar
  9. Michael Blondin, Tim Leys, Filip Mazowiecki, Philip Offtermatt, and Guillermo A. Pérez. Continuous one-counter automata. ACM Trans. Comput. Log., 24(1):3:1-3:31, 2023. Google Scholar
  10. Stanislav Böhm, Stefan Göller, and Petr Jancar. Equivalence of deterministic one-counter automata is NL-complete. In Dan Boneh, Tim Roughgarden, and Joan Feigenbaum, editors, Symposium on Theory of Computing Conference, STOC'13, Palo Alto, CA, USA, June 1-4, 2013, pages 131-140. ACM, 2013. Google Scholar
  11. Benedikt Bollig, Karin Quaas, and Arnaud Sangnier. The complexity of flat freeze LTL. Log. Methods Comput. Sci., 15(3), 2019. Google Scholar
  12. Itshak Borosh and Leon Bruce Treybig. Bounds on positive integral solutions of linear Diophantine equations. Proceedings of the American Mathematical Society, 55(2):299-304, 1976. Google Scholar
  13. Aaron R. Bradley. SAT-based model checking without unrolling. In Ranjit Jhala and David A. Schmidt, editors, Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings, volume 6538 of Lecture Notes in Computer Science, pages 70-87. Springer, 2011. Google Scholar
  14. Aaron R. Bradley. Understanding IC3. In Alessandro Cimatti and Roberto Sebastiani, editors, Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings, volume 7317 of Lecture Notes in Computer Science, pages 1-14. Springer, 2012. Google Scholar
  15. Daniel Bundala and Joël Ouaknine. On parametric timed automata and one-counter machines. Inf. Comput., 253:272-303, 2017. Google Scholar
  16. Dmitry Chistikov, Wojciech Czerwinski, Piotr Hofman, Michal Pilipczuk, and Michael Wehar. Shortest paths in one-counter systems. Log. Methods Comput. Sci., 15(1), 2019. Google Scholar
  17. Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement. In E. Allen Emerson and A. Prasad Sistla, editors, Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings, volume 1855 of Lecture Notes in Computer Science, pages 154-169. Springer, 2000. Google Scholar
  18. Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Robert M. Graham, Michael A. Harrison, and Ravi Sethi, editors, Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, pages 238-252. ACM, 1977. Google Scholar
  19. Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Filip Mazowiecki. The reachability problem for Petri nets is not elementary. J. ACM, 68(1):7:1-7:28, 2021. Google Scholar
  20. Wojciech Czerwinski and Lukasz Orlikowski. Reachability in vector addition systems is Ackermann-complete. In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022, pages 1229-1240. IEEE, 2021. Google Scholar
  21. Stéphane Demri and Arnaud Sangnier. When model-checking freeze LTL over counter machines becomes decidable. In C.-H. Luke Ong, editor, Foundations of Software Science and Computational Structures, 13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, volume 6014 of Lecture Notes in Computer Science, pages 176-190. Springer, 2010. Google Scholar
  22. Javier Esparza, Ruslán Ledesma-Garza, Rupak Majumdar, Philipp J. Meyer, and Filip Niksic. An SMT-based approach to coverability analysis. In Armin Biere and Roderick Bloem, editors, Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, volume 8559 of Lecture Notes in Computer Science, pages 603-619. Springer, 2014. Google Scholar
  23. John Fearnley and Marcin Jurdzinski. Reachability in two-clock timed automata is PSPACE-complete. Inf. Comput., 243:26-36, 2015. Google Scholar
  24. Alain Finkel, Serge Haddad, and Igor Khmelnitsky. Minimal coverability tree construction made complete and efficient. In Jean Goubault-Larrecq and Barbara König, editors, Foundations of Software Science and Computation Structures - 23rd International Conference, FOSSACS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, volume 12077 of Lecture Notes in Computer Science, pages 237-256. Springer, 2020. Google Scholar
  25. Seymour Ginsburg and Edwin H. Spanier. Semigroups, Presburger formulas and languages. Pacific Journal of Mathematics, 16(2):285-296, 1966. URL: https://doi.org/10.2140/pjm.1966.16.285.
  26. Stefan Göller, Christoph Haase, Joël Ouaknine, and James Worrell. Model checking succinct and parametric one-counter automata. In Samson Abramsky, Cyril Gavoille, Claude Kirchner, Friedhelm Meyer auf der Heide, and Paul G. Spirakis, editors, Automata, Languages and Programming, 37th International Colloquium, ICALP 2010, Bordeaux, France, July 6-10, 2010, Proceedings, Part II, volume 6199 of Lecture Notes in Computer Science, pages 575-586. Springer, 2010. Google Scholar
  27. Stefan Göller and Markus Lohrey. Branching-time model checking of one-counter processes and timed automata. SIAM J. Comput., 42(3):884-923, 2013. Google Scholar
  28. Christoph Haase, Stephan Kreutzer, Joël Ouaknine, and James Worrell. Reachability in succinct and parametric one-counter automata. In Mario Bravetti and Gianluigi Zavattaro, editors, CONCUR 2009 - Concurrency Theory, 20th International Conference, CONCUR 2009, Bologna, Italy, September 1-4, 2009. Proceedings, volume 5710 of Lecture Notes in Computer Science, pages 369-383. Springer, 2009. Google Scholar
  29. Michel Hack. Decidability questions for Petri nets. PhD thesis, MIT, 1975. URL: http://publications.csail.mit.edu/lcs/pubs/pdf/MIT-LCS-TR-161.pdf.
  30. Matthew Hague and Anthony Widjaja Lin. Model checking recursive programs with numeric data types. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 743-759. Springer, 2011. Google Scholar
  31. Matthew Hague and Anthony Widjaja Lin. Synchronisation- and reversal-bounded analysis of multithreaded programs with counters. In P. Madhusudan and Sanjit A. Seshia, editors, Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, volume 7358 of Lecture Notes in Computer Science, pages 260-276. Springer, 2012. Google Scholar
  32. Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. Software model checking for people who love automata. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, volume 8044 of Lecture Notes in Computer Science, pages 36-52. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39799-8_2.
  33. Alexander Kaiser, Daniel Kroening, and Thomas Wahl. Efficient coverability analysis by proof minimization. In Maciej Koutny and Irek Ulidowski, editors, CONCUR 2012 - Concurrency Theory - 23rd International Conference, CONCUR 2012, Newcastle upon Tyne, UK, September 4-7, 2012. Proceedings, volume 7454 of Lecture Notes in Computer Science, pages 500-515. Springer, 2012. Google Scholar
  34. Pascal Lafourcade, Denis Lugiez, and Ralf Treinen. Intruder deduction for AC-like equational theories with homomorphisms. In Jürgen Giesl, editor, Term Rewriting and Applications, 16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings, volume 3467 of Lecture Notes in Computer Science, pages 308-322. Springer, 2005. Google Scholar
  35. Antonia Lechner, Richard Mayr, Joël Ouaknine, Amaury Pouly, and James Worrell. Model checking flat freeze LTL on one-counter automata. Log. Methods Comput. Sci., 14(4), 2018. Google Scholar
  36. Jérôme Leroux. The general vector addition system reachability problem by Presburger inductive invariants. Log. Methods Comput. Sci., 6(3), 2010. Google Scholar
  37. Jérôme Leroux. Distance between mutually reachable Petri net configurations. In Arkadev Chattopadhyay and Paul Gastin, editors, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2019, December 11-13, 2019, Bombay, India, volume 150 of LIPIcs, pages 47:1-47:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. Google Scholar
  38. Jérôme Leroux. The reachability problem for Petri nets is not primitive recursive. In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022, pages 1241-1252. IEEE, 2021. Google Scholar
  39. Jérôme Leroux and Sylvain Schmitz. Reachability in vector addition systems is primitive-recursive in fixed dimension. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1-13. IEEE, 2019. Google Scholar
  40. Xie Li, Taolue Chen, Zhilin Wu, and Mingji Xia. Computing linear arithmetic representation of reachability relation of one-counter automata. In Jun Pang and Lijun Zhang, editors, Dependable Software Engineering. Theories, Tools, and Applications - 6th International Symposium, SETTA 2020, Guangzhou, China, November 24-27, 2020, Proceedings, volume 12153 of Lecture Notes in Computer Science, pages 89-107. Springer, 2020. Google Scholar
  41. Ernst W. Mayr. An algorithm for the general Petri net reachability problem. SIAM J. Comput., 13(3):441-460, 1984. Google Scholar
  42. Marvin L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, Inc., USA, 1967. Google Scholar
  43. Guillermo A. Pérez and Ritam Raha. Revisiting parameter synthesis for one-counter automata. In Florin Manea and Alex Simpson, editors, 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, Göttingen, Germany (Virtual Conference), volume 216 of LIPIcs, pages 33:1-33:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. Google Scholar
  44. Louis E. Rosier and Hsu-Chun Yen. A multiparameter analysis of the boundedness problem for vector addition systems. J. Comput. Syst. Sci., 32(1):105-135, 1986. URL: https://doi.org/10.1016/0022-0000(86)90006-1.
  45. Sylvain Schmitz. The complexity of reachability in vector addition systems. SIGLOG News, 3(1):4-21, 2016. Google Scholar
  46. Helmut Seidl, Thomas Schwentick, Anca Muscholl, and Peter Habermehl. Counting in trees for free. In Josep Díaz, Juhani Karhumäki, Arto Lepistö, and Donald Sannella, editors, Automata, Languages and Programming: 31st International Colloquium, ICALP 2004, Turku, Finland, July 12-16, 2004. Proceedings, volume 3142 of Lecture Notes in Computer Science, pages 1136-1149. Springer, 2004. Google Scholar
  47. Alistair Stewart, Kousha Etessami, and Mihalis Yannakakis. Upper bounds for Newton’s method on monotone polynomial systems, and P-time model checking of probabilistic one-counter automata. J. ACM, 62(4):30:1-30:33, 2015. Google Scholar
  48. Leslie G. Valiant and Mike Paterson. Deterministic one-counter automata. J. Comput. Syst. Sci., 10(3):340-350, 1975. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact