DI-UMONS : Dépôt institutionnel de l’université de Mons

Recherche transversale
(titres de publication, de périodique et noms de colloque inclus)
2008-09-01 - Article/Dans un journal avec peer-review - Anglais - 10 page(s)

Bertrand Nathalie, Bouyer Patricia, Brihaye Thomas , Markey Nicolas, "Quantitative Model-Checking of One-Clock Timed Automata under Probabilistic Semantics" in IEEE proceedings, 55-64

  • Codes CREF : Informatique mathématique (DI1160)
  • Unités de recherche UMONS : Mathématiques effectives (S820)
Texte intégral :

Abstract(s) :

(Anglais) In [BBBBG08] 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.

Identifiants :
  • DOI : 10.1109/QEST.2008.19