We are happy to present Ritam Raha’s talk titled “One Counter Automata:
Reachability and Synthesis Problems”.

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.