Sciweavers

Share
QEST
2008
IEEE

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

8 years 8 months ago
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.
Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye
Added 01 Jun 2010
Updated 01 Jun 2010
Type Conference
Year 2008
Where QEST
Authors Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, Nicolas Markey
Comments (0)
books