2026-07-23T12:40:58Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:15753 2024-03-06T10:56:07Z ddc:004 open_access

Revisiting Parameter Synthesis for One-Counter Automata Pérez, Guillermo A. Raha, Ritam Parametric one-counter automata Reachability Software Verification 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Guillermo A. Pérez and Ritam Raha 2022 Is Part Of LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2022.33 urn:nbn:de:0030-drops-157534 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.33 eng https://creativecommons.org/licenses/by/4.0/legalcode