Marius Bozga, Radu Iosif and Yassine Lakhnech
Flat Parametric Counter Automata (2005)
Flat Parametric Counter Automata (2005)
TR-2005-15.ps
Keywords: counter automata, diophantine systems
Abstract: In this paper we study the reachability problem for parametric flat counter automata, in relation with the satisfiability problem of three fragments of integer arithmetic. The equivalence between non-parametric flat counter automata and Presburger arithmetic has been established previously by Comon and Jurski cite{comon-jurski98}. We simplify their proof by introducing finite state automata defined over alphabets of a special kind of graphs (zigzags). This framework allows one to express also the reachability problem for parametric automata with one control loop as the existence of solutions of a {em 1-parametric linear Diophantine systems}. The latter problem is shown to be decidable, using a number-theoretic argument. Finally, the general reachability problem for parametric flat counter automata with more than one loops is shown to be undecidable, by reduction from Hilbert's Tenth Problem cite{hilbert}.
