When Model-Checking Freeze LTL over Counter Machines Becomes Decidable

Stéphane Demri (1, 2, 3) , Arnaud Sangnier (4)

1 LSV - Laboratoire Spécification et Vérification
2 CNRS - Centre National de la Recherche Scientifique
3 DAHU - Verification in databases
4 UNITO - Università degli studi di Torino = University of Turin

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 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\slash and the polarity of the occurrences of the freeze operators, leading to the flat fragment.

Mots clés: one-counter machine; flatness; vector addition system; complexity; parameterised counter machine; counter machine; linear-time temporal logic LTL; Freeze LTL; freeze quantifier; reversal-boundedness; one-counter machine

Domaines: Informatique [cs]; Logique en informatique [cs.LO]; Théorie et langage formel [cs.FL]

Stéphane Demri, Arnaud Sangnier. When Model-Checking Freeze LTL over Counter Machines Becomes Decidable. FOSSACS 2010 - Foundations of Software Science and Computational Structures, 13th International Conference, Luke Ong, Mar 2010, Paphos, Cyprus. pp.176-190, ⟨10.1007/978-3-642-12032-9_13⟩. ⟨hal-03201974⟩