[en] In [BBBBG08] 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.
Disciplines :
Electrical & electronics engineering
Author, co-author :
Bertrand, Nathalie
Bouyer, Patricia
Brihaye, Thomas ; Université de Mons > Faculté des Sciences > Logique mathématique
Markey, Nicolas
Language :
English
Title :
Quantitative Model-Checking of One-Clock Timed Automata under Probabilistic Semantics