Flat Parametric Counter Automata

Abstract. In this paper we study the reachability problem for parametric flatcounter automata, in relation with the satisfiability problem of three fragments of integer arithmetic. The equivalence between non-parametric flat counter au-tomata and Presburger arithmetic has been established previously by Comon and Jurski [5]. We simplify their proof by introducing finite state automata definedover alphabets of a special kind of graphs (zigzags). This framework allows one to express also the reachability problem for parametric automata with one controlloop as the existence of solutions of a 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'sTenth Problem [9]. 1 Introduction Flat counter automata [5, 6, 3, 4] have been extensively studied, as an important classof infinite-state systems, for which the reachability problem is decidable. The results obtained so far have been used in a number of successful verification tools, like FAST[2], LASH [18] or TREX [1]. Comon and Jurski show in [5] that the reachability problem for a flat counter au-tomaton can be expressed in Presburger arithmetic, given that the automata have transition guards that are conjunctions of relations of the form x- y < = c, where x and ydenote either the current or the future (primed) values of the counters, and c is an integer constant. To our knowledge, their result concerns the most general class of flatcounter automata, considered so far