One-counter automata are well-studied classical models in the field of formal verification 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. In this talk, we focus on the synthesis problems for such automata that ask whether there exists a valuation of the parameters such that all infinite runs of the automaton satisfy some omega-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.

You can see the slides of the presentation here

Speaker

Ritam Raha is a 4th year PhD student at UAntwerp and LaBRI-Bordeaux University. His expertise concerns the specification, modellisation, and automatic verification of software systems.

Time and Place

Friday 21/10/2022 at 11:30am in M.A.143

Registration

Participation is free, but registration is compulsory. Make sure to fill in this form.

References and Related Reading

  • What is automata?
    • Introduction to the Theory of Computation (Book), Michael Sipser
    • Theory of Computation (Book), Dexter Kozen
    • Talen en Automaten (Course)
  • What is non-determinism and determinism?
    • All the same as above
    • Machines en Berekenbaarheid (Course)
  • What is mathematical logic?
    • Discrete Mathematics (Course)
    • Toegepaste Logica (Course)
    • Wiskundige Logica (Course)
  • What is (un)decidability? Complexity?
    • Machines en Berekenbaarheid (Course)
    • Algorithms and Complexity (Course)