eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
33:1
33:18
10.4230/LIPIcs.CSL.2022.33
article
Revisiting Parameter Synthesis for One-Counter Automata
Pérez, Guillermo A.
1
https://orcid.org/0000-0002-1200-4952
Raha, Ritam
2
3
https://orcid.org/0000-0003-1467-1182
University of Antwerp, Flanders Make, Belgium
University of Antwerp, Belgium
LaBRI, University of Bordeaux, France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.33/LIPIcs.CSL.2022.33.pdf
Parametric one-counter automata
Reachability
Software Verification