|
|
|
Intitulé:
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, flat 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 classification 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 flat 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 |
Email | sangnier@di.unito.it |
Url | Dipartimento di Informatica Università degli studi di Torino, Italy |
Aucun document lié à cet événement. RetourRetour à l'index
| |