When Model-Checking Freeze LTL over Counter Machines Becomes Decidable

We study the decidability status of model-checking freeze LTL over various subclasses of counter machines for which the reachability problem is known to be decidable (reversal-bounded counter machines, vector additions systems with states, flat counter machines, one-counter machines). In freeze LTL, a register can store a counter value and at some future position an equality test can be done between a register and a counter value. Herein, we complete an earlier work started on one-counter machines (Demri, Lazic, Sangnier; FOSSACS 08) by considering other subclasses of counter machines, and especially the class of reversal-bounded counter machines. This gives us the opportuniy to provide a systematic classification that distinguishes determinism vs. nondeterminism and we consider subclasses of formulae by restricting the set of atomic formulae or/and the polarity of the occurrences of the freeze operators, leading to the flat fragment. In some places, we shall take advantage of recent results about parameterized one-counter machines (Haase, Kreutzer, Ouaknine, Worrell; CONCUR 09).  

This is a joint work with Arnaud Sangnier.