%0 Conference Proceedings
%F BBBM-qest08
%A Bertrand, N.
%A Bouyer, P.
%A Brihaye, Th.
%A Markey, N.
%T Quantitative Model-Checking of One-Clock Timed Automata under Probabilistic Semantics
%B Proceedings of the 5th International Conference on the Quantitative Evaluation of SysTems (QEST'08)
%P 55-64
%I IEEE Computer Society Press
%C Saint Malo, France
%X In 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
%U http://www.irisa.fr/vertecs/Publis/Ps/BBBM-qest08.pdf
%U http://dx.doi.org/10.1109/QEST.2008.19
%8 September
%D 2008