| HAL-Inria | Publications, software ... of Inria's scientists |
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.
https://hal.inria.fr/inria-00424518
Contributor : Nathalie Bertrand <>
Submitted on : Friday, October 16, 2009 - 10:59:25 AM
Last modification on : Tuesday, March 30, 2021 - 12:12:08 PM
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
