Document Open Access Logo

Revisiting Parameter Synthesis for One-Counter Automata

Authors Guillermo A. Pérez , Ritam Raha

PDF
Thumbnail PDF

File

LIPIcs.CSL.2022.33.pdf
  • Filesize: 0.88 MB
  • 18 pages

Document Identifiers

Author Details

Guillermo A. Pérez
  • University of Antwerp, Flanders Make, Belgium
Ritam Raha
  • University of Antwerp, Belgium
  • LaBRI, University of Bordeaux, France

Funding

This work was supported by the Belgian FWO "SAILor" project (G030020N).

Acknowledgements

We thank all anonymous reviewers who carefully read earlier version of this work and helped us polish the paper. We also thank Michaël Cadilhac, Nathanaël Fijalkow, Philip Offtermatt, and Mikhail R. Starchak for useful feedback; Antonia Lechner and James Worrell for having brought the inconsistencies in [Marius Bozga and Radu Iosif, 2005; Antonia Lechner, 2015] to our attention; Radu Iosif and Marius Bozga for having pointed out precisely what part of the argument in both papers is incorrect.

Cite AsGet BibTex

Guillermo A. Pérez and Ritam Raha. Revisiting Parameter Synthesis for One-Counter Automata. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 33:1-33:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.CSL.2022.33

Abstract

We study the synthesis problem for one-counter automata with parameters. One-counter automata are obtained by extending classical finite-state automata with a counter whose value can range over non-negative integers and be tested for zero. The updates and tests applicable to the counter can further be made parametric by introducing a set of integer-valued variables called parameters. The synthesis problem for such automata asks whether there exists a valuation of the parameters such that all infinite runs of the automaton satisfy some ω-regular property. Lechner showed that (the complement of) the problem can be encoded in a restricted one-alternation fragment of Presburger arithmetic with divisibility. In this work (i) we argue that said fragment, called ∀∃_RPAD^+, is unfortunately undecidable. Nevertheless, by a careful re-encoding of the problem into a decidable restriction of ∀∃_RPAD^+, (ii) we prove that the synthesis problem is decidable in general and in 2NEXP for several fixed ω-regular properties. Finally, (iii) we give polynomial-space algorithms for the special cases of the problem where parameters can only be used in counter tests.

Subject Classification

ACM Subject Classification
  • Theory of computation → Quantitative automata
  • Theory of computation → Logic and verification
Keywords
  • Parametric one-counter automata
  • Reachability
  • Software Verification

Metrics

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

Related Versions

References

  1. Frances E Allen. Control flow analysis. ACM Sigplan Notices, 5(7):1-19, 1970. Google Scholar
  2. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  3. A. P. Beltyukov. Decidability of the universal theory of natural numbers with addition and divisibility. Journal of Soviet Mathematics, 14(5):1436-1444, November 1980. URL: https://doi.org/10.1007/BF01693974.
  4. Benedikt Bollig, Karin Quaas, and Arnaud Sangnier. The complexity of flat freeze LTL. Logical Methods in Computer Science, 15(3), 2019. URL: https://doi.org/10.23638/LMCS-15(3:33)2019.
  5. Ahmed Bouajjani, Marius Bozga, Peter Habermehl, Radu Iosif, Pierre Moro, and Tomás Vojnar. Programs with lists are counter automata. In Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, pages 517-531, 2006. URL: https://doi.org/10.1007/11817963_47.
  6. Marius Bozga and Radu Iosif. On decidability within the arithmetic of addition and divisibility. In Vladimiro Sassone, editor, Foundations of Software Science and Computational Structures, 8th International Conference, FOSSACS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings, volume 3441 of Lecture Notes in Computer Science, pages 425-439. Springer, 2005. URL: https://doi.org/10.1007/978-3-540-31982-5_27.
  7. Daniel Bundala and Joël Ouaknine. On parametric timed automata and one-counter machines. Inf. Comput., 253:272-303, 2017. URL: https://doi.org/10.1016/j.ic.2016.07.011.
  8. Cristiana Chitic and Daniela Rosu. On validation of XML streams using finite state machines. In Proceedings of the Seventh International Workshop on the Web and Databases, WebDB 2004, June 17-18, 2004, Maison de la Chimie, Paris, France, Colocated with ACM SIGMOD/PODS 2004, pages 85-90, 2004. URL: https://doi.org/10.1145/1017074.1017096.
  9. Patrick Cousot and Radhia Cousot. A gentle introduction to formal verification of computer systems by abstract interpretation. In Javier Esparza, Bernd Spanfelner, and Orna Grumberg, editors, Logics and Languages for Reliability and Security, volume 25 of NATO Science for Peace and Security Series - D: Information and Communication Security, pages 1-29. IOS Press, 2010. URL: https://doi.org/10.3233/978-1-60750-100-8-1.
  10. Azadeh Farzan, Zachary Kincaid, and Andreas Podelski. Proofs that count. In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 151-164. ACM, 2014. URL: https://doi.org/10.1145/2535838.2535885.
  11. M. R. Garey and David S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman, 1979. Google Scholar
  12. 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. URL: https://doi.org/10.1007/978-3-642-14162-1_48.
  13. Christoph Haase. On the complexity of model checking counter automata. PhD thesis, University of Oxford, 2012. Google Scholar
  14. Christoph Haase. Subclasses of presburger arithmetic and the weak EXP hierarchy. In Thomas A. Henzinger and Dale Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, pages 47:1-47:10. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603092.
  15. Christoph Haase. A survival guide to presburger arithmetic. ACM SIGLOG News, 5(3):67-82, 2018. URL: https://dl.acm.org/citation.cfm?id=3242964.
  16. Christoph Haase, Stephan Kreutzer, Joël Ouaknine, and James Worrell. Reachability in succinct and parametric one-counter automata. In CONCUR 2009 - Concurrency Theory, 20th International Conference, CONCUR 2009, Bologna, Italy, September 1-4, 2009. Proceedings, pages 369-383, 2009. URL: https://doi.org/10.1007/978-3-642-04081-8_25.
  17. Oscar H. Ibarra, Tao Jiang, Nicholas Q. Trân, and Hui Wang. New decidability results concerning two-way counter machines. SIAM J. Comput., 24(1):123-137, 1995. URL: https://doi.org/10.1137/S0097539792240625.
  18. Oscar H. Ibarra, Jianwen Su, Zhe Dang, Tevfik Bultan, and Richard A. Kemmerer. Counter machines and verification problems. Theor. Comput. Sci., 289(1):165-189, 2002. URL: https://doi.org/10.1016/S0304-3975(01)00268-7.
  19. Orna Kupferman and Moshe Y. Vardi. Safraless decision procedures. In 46th Annual IEEE Symposium on Foundations of Computer Science (FOCS 2005), 23-25 October 2005, Pittsburgh, PA, USA, Proceedings, pages 531-542. IEEE Computer Society, 2005. URL: https://doi.org/10.1109/SFCS.2005.66.
  20. Mahler Kurt. On the Chinese remainder theorem. Mathematische Nachrichten, 18(1‐6):120-122, 1958. URL: https://doi.org/10.1002/mana.19580180112.
  21. Antonia Lechner. Synthesis problems for one-counter automata. In Mikolaj Bojanczyk, Slawomir Lasota, and Igor Potapov, editors, Reachability Problems - 9th International Workshop, RP 2015, Warsaw, Poland, September 21-23, 2015, Proceedings, volume 9328 of Lecture Notes in Computer Science, pages 89-100. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-24537-9_9.
  22. Antonia Lechner. Extensions of Presburger arithmetic and model checking one-counter automata. PhD thesis, University of Oxford, 2016. Google Scholar
  23. Antonia Lechner, Joël Ouaknine, and James Worrell. On the complexity of linear arithmetic with divisibility. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 667-676, 2015. URL: https://doi.org/10.1109/LICS.2015.67.
  24. 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. URL: https://doi.org/10.1007/978-3-030-62822-2_6.
  25. Anthony W. Lin and Rupak Majumdar. Quadratic word equations with length constraints, counter systems, and presburger arithmetic with divisibility. In Shuvendu K. Lahiri and Chao Wang, editors, Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings, volume 11138 of Lecture Notes in Computer Science, pages 352-369. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-01090-4_21.
  26. Leonard Lipshitz. The diophantine problem for addition and divisibility. Transactions of the American Mathematical Society, pages 271-283, 1978. Google Scholar
  27. Leonard Lipshitz. Some remarks on the diophantine problem for addition and divisibility. Bull. Soc. Math. Belg. Sér. B, 33(1):41-52, 1981. Google Scholar
  28. Ju V Matijasevic. Enumerable sets are diophantine. In Soviet Math. Dokl., volume 11, pages 354-358, 1970. Google Scholar
  29. Marvin L. Minsky. Recursive unsolvability of post’s problem of "tag" and other topics in theory of turing machines. Annals of Mathematics, 74(3):437-455, 1961. URL: http://www.jstor.org/stable/1970290.
  30. Julia Robinson. Definability and decision problems in arithmetic. The Journal of Symbolic Logic, 14(2):98-114, 1949. Google Scholar
  31. Olivier Serre. Parity games played on transition graphs of one-counter processes. In Luca Aceto and Anna Ingólfsdóttir, editors, Foundations of Software Science and Computation Structures, 9th International Conference, FOSSACS 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25-31, 2006, Proceedings, volume 3921 of Lecture Notes in Computer Science, pages 337-351. Springer, 2006. URL: https://doi.org/10.1007/11690634_23.
  32. A. Prasad Sistla and Edmund M. Clarke. The complexity of propositional linear temporal logics. J. ACM, 32(3):733-749, 1985. URL: https://doi.org/10.1145/3828.3837.
  33. Joachim von zur Gathen and Malte Sieveking. A bound on solutions of linear integer equalities and inequalities. Proceedings of the American Mathematical Society, 72(1):155-158, 1978. 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