Affiliations: Verimag, CNRS, Université de Grenoble 2
Avenue de Vignate, 38610, Gières, France. {bozga,iosif,lakhnech}@imag.fr
Note: [] Address for correspondence: Verimag, 2 Avenue de Vignate, 38610,
Gières, France
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. 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 satisfiability of a 1-parametric linear
Diophantine systems. The latter problem is shown to be decidable, using a
number-theoretic argument. In general, the reachability problem for parametric
flat counter automata with more than one loops is shown to be undecidable, by
reduction from Hilbert's Tenth Problem. Finally, we study the
relation between flat counter automata, integer arithmetic, and another
important class of computational devices, namely the 2-way reversal bounded
counter machines.
Keywords: Counter machines, Reachability problems, Diophantine systems
