Evènement pour le groupe Modélisation et Verification

Date 2010-04-01  11:30-12:45
TitreWhen 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).  
LieuSalle 076, LaBRI, Rez-de-chaussée 
OrateurArnaud Sangnier 
UrlDipartimento di Informatica Università degli studi di Torino, Italy 

Aucun document lié à cet événement.

Retour à l'index