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

In [3] 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 modelchecking problem for ω-regular properties: we aim at computing the exact probability that a given timed automaton satisfies an ω-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: Conference
• Year: 2008
• Where: QEST
• Authors: Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, Nicolas Markey
• Keywords: QEST 2008, Quantitative Evaluation Of Systems, Single-clock Timed Automata, Timed Automata, Timed Automaton