|When Model-Checking Freeze LTL over Counter Machines Becomes Decidable|
du groupe Modélisation et Verification
|Date|| 2010-04-01 11:30-12:45|
|Titre||When Model-Checking Freeze LTL over Counter Machines Becomes Decidable |
|Résumé||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 (one-counter machines, reversal-bounded counter machines, vector additions systems with states, ﬂat counter machines). Freeze LTL is an extension of the linear temporal logic to which registers are added. In this logic, 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. We provide a systematic classiﬁcation for the model-checking problem of freeze LTL over counter machines that distinguishes determinism vs. nondeterminism and we also 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 ﬂat fragment.
This is a joint work with Stéphane Demri (LSV, CNRS, ENS de Cachan) and Ranko Lazic (Department of Computer Science, University of Warwick).
|Lieu||Salle 076, LaBRI, Rez-de-chaussée |
|Orateur||Arnaud Sangnier |
|Url||Dipartimento di Informatica Università degli studi di Torino, Italy |
Aucun document lié à cet événement.RetourRetour à l'index