Title: Parameter Synthesis for One-Counter Automata
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. During this talk we will focus on parameter synthesis problems 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. We will see that said fragment, called EARPAD, is unfortunately undecidable. Fortunately, there is an alternative encoding of the problem into a decidable restriction of EARPAD. Finally, we will study an alternative solution going via alternating two-way automata. The latter gives us 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.