Revisiting Parameter Synthesis Problems for One-Counter Automata

Abstract

One-counter automata are well studied classical model that extend 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. We will discuss how these problems relate to different restricted fragments of Presburger arithmetic with divisibility. Using this connection, I will present decidability results for the above mentioned synthesis problems. I will also present polynomial-space algorithms for the special cases of the problem where parameters can only be used in counter tests. This talk is primarily based on joint work with my supervisor Guillermo Perez.

Bio

Ritam Raha is a joint PhD student at the University of Antwerp in Belgium and LaBRI, University of Bordeaux in France. He is working under the supervision of Prof. Guillermo Perez and Prof. Nathanael Fijalkow. His research mainly focuses on verification of complex systems against learnt specifications.
Find his website here.