Nicolas Markey

Abstract

In [Baier et al., Probabilistic and Topological Semantics for Timed Automata, FSTTCS'07] 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 ω-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.

@inproceedings{qest2008-BBBM,
  author =              {Bertrand, Nathalie and Bouyer, Patricia and Brihaye,
                         {\relax Th}omas and Markey, Nicolas},
  title =               {Quantitative Model-Checking of One-Clock Timed
                         Automata under Probabilistic Semantics},
  booktitle =           {{P}roceedings of the 5th {I}nternational
                         {C}onference on {Q}uantitative {E}valuation of
                         {S}ystems ({QEST}'08)},
  acronym =             {{QEST}'08},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {55-64},
  year =                {2008},
  month =               sep,
  doi =                 {10.1109/QEST.2008.19},
  abstract =            {In [Baier \emph{et~al.}, \textit{Probabilistic and
                         Topological Semantics for Timed Automata},
                         FSTTCS'07] 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.\par 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.},
}