Document Open Access Logo

The Well Structured Problem for Presburger Counter Machines

Authors Alain Finkel, Ekanshdeep Gupta

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2019.41.pdf
  • Filesize: 0.54 MB
  • 15 pages

Document Identifiers

Author Details

Alain Finkel
  • LSV, ENS Paris-Saclay, CNRS, Université Paris-Saclay, IUF, France
Ekanshdeep Gupta
  • Chennai Mathematical Institute, Chennai, India

Funding

The work reported was carried out in the framework of ReLaX, UMI2000 (ENS Paris-Saclay, CNRS, Univ. Bordeaux, CMI, IMSc). This work was also supported by the grant ANR-17-CE40-0028 of the French National Research Agency ANR (project BRAVAS).
  • Finkel, Alain: UMI ReLaX and ANR-17-CE40-0028 of the French National Research Agency ANR (project BRAVAS)
  • Gupta, Ekanshdeep: UMI ReLaX and ANR-17-CE40-0028 of the French National Research Agency ANR (project BRAVAS)

Cite As Get BibTex

Alain Finkel and Ekanshdeep Gupta. The Well Structured Problem for Presburger Counter Machines. In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 41:1-41:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.FSTTCS.2019.41

Abstract

We introduce the well structured problem as the question of whether a model (here a counter machine) is well structured (here for the usual ordering on integers). We show that it is undecidable for most of the (Presburger-defined) counter machines except for Affine VASS of dimension one. However, the strong well structured problem is decidable for all Presburger counter machines. While Affine VASS of dimension one are not, in general, well structured, we give an algorithm that computes the set of predecessors of a configuration; as a consequence this allows to decide the well structured problem for 1-Affine VASS.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Verification by model checking
Keywords
  • Well structured transition systems
  • infinite state systems
  • Presburger counter machines
  • reachability
  • coverability

Metrics

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

Related Versions

References

  1. Michael Blondin, Christoph Haase, and Filip Mazowiecki. Affine Extensions of Integer Vector Addition Systems with States. In Sven Schewe and Lijun Zhang, editors, 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China, volume 118 of LIPIcs, pages 14:1-14:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.14.
  2. Michael Blondin and Mikhail Raskin. The Complexity of Reachability in Affine Vector Addition Systems with States. CoRR, 2019. URL: http://arxiv.org/abs/1909.02579.
  3. Bernard Boigelot and Pierre Wolper. Symbolic Verification with Periodic Sets. In Computer Aided Verification, 6th International Conference, CAV '94, Stanford, California, USA, June 21-23, 1994, Proceedings, pages 55-67, 1994. URL: https://doi.org/10.1007/3-540-58179-0_43.
  4. Rémi Bonnet, Alain Finkel, and M. Praveen. Extending the Rackoff technique to Affine nets. In Deepak D'Souza, Telikepalli Kavitha, and Jaikumar Radhakrishnan, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2012, December 15-17, 2012, Hyderabad, India, volume 18 of LIPIcs, pages 301-312. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2012. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2012.301.
  5. Ahmed Bouajjani, Javier Esparza, Alain Finkel, Oded Maler, Peter Rossmanith, Bernard Willems, and Pierre Wolper. An Efficient Automata Approach to some Problems on Context-Free Grammars. Information Processing Letters, 74(5-6):221-227, June 2000. URL: http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BEFMRWW-IPL2000.ps.
  6. Stéphane Demri, Alain Finkel, Valentin Goranko, and Govert van Drimmelen. Model-checking CTL* over flat Presburger counter systems. Journal of Applied Non-Classical Logics, 20(4):313-344, 2010. URL: https://doi.org/10.3166/jancl.20.313-344.
  7. Catherine Dufourd, Alain Finkel, and Philippe Schnoebelen. Reset Nets between Decidability and Undecidability. In Kim G. Larsen, Sven Skyum, and Glynn Winskel, editors, Proceedings of the 25th International Colloquium on Automata, Languages and Programming (ICALP'98), volume 1443 of Lecture Notes in Computer Science, pages 103-115, Aalborg, Denmark, July 1998. Springer. URL: https://doi.org/10.1007/BFb0055044.
  8. A. Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science, 256(1):63-92, 2001. ISS. URL: https://doi.org/10.1016/S0304-3975(00)00102-X.
  9. Alain Finkel. Reduction and covering of infinite reachability trees. Information and Computation, 89(2):144-179, 1990. Google Scholar
  10. Alain Finkel, Stefan Göller, and Christoph Haase. Reachability in Register Machines with Polynomial Updates. In Krishnendu Chatterjee and Jiří Sgall, editors, Proceedings of the 38th International Symposium on Mathematical Foundations of Computer Science (MFCS'13), volume 8087 of Lecture Notes in Computer Science, pages 409-420, Klosterneuburg, Austria, August 2013. Springer. URL: https://doi.org/10.1007/978-3-642-40313-2_37.
  11. Alain Finkel and Jérôme Leroux. How to Compose Presburger-Accelerations: Applications to Broadcast Protocols. In FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science, 22nd Conference Kanpur, India, December 12-14, 2002, Proceedings, pages 145-156, 2002. URL: https://doi.org/10.1007/3-540-36206-1_14.
  12. Alain Finkel, Jérôme Leroux, and Grégoire Sutre. Reachability for Two-Counter Machines with One Test and One Reset. In Sumit Ganguly and Paritosh Pandya, editors, Proceedings of the 38th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'18), Leibniz International Proceedings in Informatics, pages 31:1-31:14, Ahmedabad, India, December 2018. Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2018.31.
  13. Alain Finkel, Pierre McKenzie, and Claudine Picaronny. A Well-Structured Framework for Analysing Petri Net Extensions. Information and Computation, 195(1-2):1-29, November 2004. URL: https://doi.org/10.1016/j.ic.2004.01.005.
  14. Christoph Haase. A Survival Guide to Presburger Arithmetic. ACM SIGLOG News, 5(3):67-82, July 2018. URL: https://doi.org/10.1145/3242953.3242964.
  15. Christoph Haase and Simon Halfon. Integer Vector Addition Systems with States. In Joël Ouaknine, Igor Potapov, and James Worrell, editors, Reachability Problems - 8th International Workshop, RP 2014, Oxford, UK, Sept. 22-24, 2014. Proceedings, volume 8762 of Lecture Notes in Computer Science, pages 112-124. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-11439-2_9.
  16. Vesa Halava. Another proof of undecidability for the correspondence decision problem - Had I been Emil Post. CoRR, abs/1411.5197, 2014. URL: http://arxiv.org/abs/1411.5197.
  17. Matthias Horbach, Marco Voigt, and Christoph Weidenbach. The Universal Fragment of Presburger Arithmetic with Unary Uninterpreted Predicates is Undecidable. CoRR, abs/1703.01212, 2017. URL: http://arxiv.org/abs/1703.01212.
  18. Jérôme Leroux and Grégoire Sutre. On Flatness for 2-Dimensional Vector Addition Systems with States. In Philippa Gardner and Nobuko Yoshida, editors, CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings, volume 3170 of Lecture Notes in Computer Science, pages 402-416. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-28644-8_26.
  19. Jérôme Leroux, Grégoire Sutre, and Patrick Totzke. On the Coverability Problem for Pushdown Vector Addition Systems in One Dimension. In Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II, pages 324-336, 2015. URL: https://doi.org/10.1007/978-3-662-47666-6_26.
  20. Julien Reichert. Reachability games with counters : decidability and algorithms. (Décidabilité et complexité de jeux d'accessibilité sur des systèmes à compteurs). PhD thesis, École normale supérieure de Cachan, France, 2015. URL: https://tel.archives-ouvertes.fr/tel-01314414.
  21. Rüdiger Valk. Self-Modifying Nets, a Natural Extension of Petri Nets. In Giorgio Ausiello and Corrado Böhm, editors, Automata, Languages and Programming, Fifth Colloquium, Udine, Italy, July 17-21, 1978, Proceedings, volume 62 of Lecture Notes in Computer Science, pages 464-476. Springer, 1978. URL: https://doi.org/10.1007/3-540-08860-1_35.
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 About DROPS Imprint Privacy Contact