Stochastic timed automata

Abstract : A stochastic timed automaton is a purely stochastic process defined on a timed automaton, in which both delays and discrete choices are made randomly. We study the almost-sure model-checking problem for this model, that is, given a stochastic timed automaton A and a property ϕ, we want to decide whether A satisfies ϕ with probability 1. In this paper, we identify several classes of automata and of properties for which this can be decided. The proof relies on the construction of a finite abstraction, called the thick graph, that we interpret as a finite Markov chain, and for which we can decide the almost-sure model-checking problem. Correctness of the abstraction holds when automata are almost-surely fair, which we show, is the case for two large classes of systems, single-clock automata and so-called weak-reactive automata. Techniques employed in this article gather tools from real-time verification and probabilistic verification, as well as topological games played on timed automata.
Type de document :
Article dans une revue
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2014, 10 (4), pp.73. 〈10.2168/LMCS-10(4:6)2014〉
Liste complète des métadonnées

Littérature citée [36 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01102368
Contributeur : Nathalie Bertrand <>
Soumis le : lundi 12 janvier 2015 - 16:04:37
Dernière modification le : mercredi 16 mai 2018 - 11:24:07
Document(s) archivé(s) le : vendredi 11 septembre 2015 - 06:36:00

Fichier

1410.2128.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, Quentin Menet, Christel Baier, et al.. Stochastic timed automata. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2014, 10 (4), pp.73. 〈10.2168/LMCS-10(4:6)2014〉. 〈hal-01102368〉

Partager

Métriques

Consultations de la notice

675

Téléchargements de fichiers

136