Article (Scientific journals)
Quantitative Model-Checking of One-Clock Timed Automata under Probabilistic Semantics
Bertrand, Nathalie; Bouyer, Patricia; Brihaye, Thomas et al.
2008In IEEE proceedings, p. 55-64
Peer reviewed
 

Files


Full Text
BRIHAYE-2008-10-JOURNAL.pdf
Author postprint (266.95 kB)
Request a copy

All documents in ORBi UMONS are protected by a user license.

Send to



Details



Abstract :
[en] 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.
Disciplines :
Electrical & electronics engineering
Author, co-author :
Bertrand, Nathalie
Bouyer, Patricia
Brihaye, Thomas  ;  Université de Mons > Faculté des Sciences > Logique mathématique
Markey, Nicolas
Language :
English
Title :
Quantitative Model-Checking of One-Clock Timed Automata under Probabilistic Semantics
Publication date :
01 September 2008
Journal title :
IEEE proceedings
ISSN :
2473-2001
Pages :
55-64
Peer reviewed :
Peer reviewed
Research unit :
S820 - Mathématiques effectives
Available on ORBi UMONS :
since 10 July 2010

Statistics


Number of views
0 (0 by UMONS)
Number of downloads
0 (0 by UMONS)

OpenCitations
 
15

Bibliography


Similar publications



Contact ORBi UMONS