Quantitative Model-Checking of One-Clock Timed Automata under Probabilistic Semantics.

Nathalie Bertrand 1 Patricia Bouyer 2 Thomas Brihaye 3 Nicolas Markey 2
1 VERTECS - Verification models and techniques applied to testing and control of reactive systems
Inria Rennes – Bretagne Atlantique
2 LSV - Laboratoire Spécification et Vérification [Cachan]
3 Institut de Mathématiques [Mons]
Abstract : In [BBBBG-lics08] a probabilistic semantics for timed automata has been defined in order to rule out unlikely (sequences of) events. The qualitative model-checking problem for LTL properties has been investigated, where the aim is to check whether a given LTL property holds with probability 1 in a timed automaton, and solved for the class of single-clock timed automata. In this paper, we consider the quantitative model-checking problem for omega-regular properties: we aim at computing the exact probability that a given timed automaton satisfies an omega-regular property. We develop a framework in which we can compute a closed-form expression for this probability; we furthermore give an approximation algorithm, and finally prove that we can decide the threshold problem in that framework.
Type de document :
Communication dans un congrès
5th International Conference on the Quantitative Evaluation of Systems (QEST'08), Sep 2008, Saint Malo, France. IEEE, pp.55-64, 2008, 〈10.1109/QEST.2008.19〉
Liste complète des métadonnées
https://hal.inria.fr/inria-00424518
Contributeur : Nathalie Bertrand <>
Soumis le : vendredi 16 octobre 2009 - 10:59:25
Dernière modification le : mercredi 11 avril 2018 - 01:51:58

Lien texte intégral

openaccess

Identifiants

Collections

INRIA | ENS-CACHAN

Citation

Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, Nicolas Markey. Quantitative Model-Checking of One-Clock Timed Automata under Probabilistic Semantics.. 5th International Conference on the Quantitative Evaluation of Systems (QEST'08), Sep 2008, Saint Malo, France. IEEE, pp.55-64, 2008, 〈10.1109/QEST.2008.19〉. 〈inria-00424518〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

144

Contact


archive-ouverte@inria.fr