Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata
Contributor : Nathalie Bertrand <>
Submitted on : Friday, October 16, 2009 - 10:59:25 AM
Last modification on : Tuesday, March 30, 2021 - 12:12:08 PM

Links full text



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. pp.55-64, ⟨10.1109/QEST.2008.19⟩. ⟨inria-00424518⟩



Record views