References & Citations
Computer Science > Logic in Computer Science
Title: Revisiting Synthesis for One-Counter Automata
(Submitted on 3 May 2020 (this version), latest version 19 Oct 2021 (v6))
Abstract: 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. We revisit the parameter synthesis problem for such automata. That is, we ask whether there exists a valuation of the parameters such that all infinite runs of the automaton satisfy some omega-regular property. The problem has been shown to be encodable in a restricted one-alternation fragment of Presburger arithmetic with divisibility. In this work (i) we argue that said fragment of the logic is unfortunately undecidable. Nevertheless, by reduction to a class of partial observation games, (ii) we prove the synthesis problem is decidable. Finally, (iii) we give a polynomial-space algorithm for the problem if 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.