Evènement pour le groupe Modélisation et Verification


Date 2007-06-28  11:00-12:15
TitreA probabilistic semantic for timed automata 
RésuméLike most models used in model-checking, timed automata are an ideal mathematical model to represent systems with strong timing requirements. In such mathematical models, properties can be violated, due to unlikely events. Following ideas of Varacca and Völzer in their LICS'06 paper, we aim at defining a notion of ``fair'' correctness for timed systems. For this purpose, we introduce a probabilistic semantics for timed automata, which ignores unlikely events, and naturally raises a notion of almost-sure satisfaction of properties in timed systems. We prove that the almost-sure satisfaction has a corresponding topological interpretation in terms of largeness of the set of paths satisfying the property. Moreover, we show PSPACE-Completeness for the LTL model-checking problem over finite computations. Il s'agit d'un travail en collaboration avec Christel Baier, Nathalie Bertrand, Patricia Bouyer et Marcus Größer  
LieuSalle 178, LaBRI, Rez-de-chaussée 
OrateurThomas Brihaye 
EmailThomas.Brihaye@lsv.ens-cachan.fr 
UrlLSV, Cachan, France 



Aucun document lié à cet événement.

Retour
Retour à l'index