 |
 |
|
Evènement pour le groupe Modélisation et Verification
| Date | 2007-06-28 11:00-12:15 |
| Titre | A 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
|
| Lieu | Salle 178, LaBRI, Rez-de-chaussée |
| Orateur | Thomas Brihaye |
| Email | Thomas.Brihaye@lsv.ens-cachan.fr |
| Url | LSV, Cachan, France |
Aucun document lié à cet événement. RetourRetour à l'index
| |