References & Citations
Computer Science > Logic in Computer Science
Title: Revisiting Parameter Synthesis for One-Counter Automata
(Submitted on 3 May 2020 (v1), last revised 19 Oct 2021 (this version, v6))
Abstract: We study the (parameter) 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 omega-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 AERPADPLUS, is unfortunately undecidable. Nevertheless, by a careful re-encoding of the problem into a decidable restriction of AERPADPLUS, (ii) we prove that the synthesis problem is decidable in general and in N2EXP for several fixed omega-regular properties. Finally, (iii) we give a polynomial-space algorithm for the special case of the problem where parameters can only be used in tests, and not updates, of the counter.
Submission history
From: Ritam Raha [view email][v1] Sun, 3 May 2020 12:30:11 GMT (55kb,D)
[v2] Thu, 1 Oct 2020 10:15:25 GMT (54kb)
[v3] Fri, 29 Jan 2021 11:16:52 GMT (121kb)
[v4] Thu, 29 Apr 2021 17:26:28 GMT (131kb,D)
[v5] Mon, 18 Oct 2021 12:34:30 GMT (264kb,D)
[v6] Tue, 19 Oct 2021 13:50:45 GMT (264kb,D)
Link back to: arXiv, form interface, contact.