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

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 : jeudi 11 janvier 2018 - 06:20:13

Identifiants

Collections

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〉

Partager

Métriques

Consultations de la notice

132