Stochastic timed automata

Nathalie Bertrand (1) , Patricia Bouyer (2, 3) , Thomas Brihaye (4) , Quentin Menet (4) , Christel Baier (5) , Marcus Groesser (5) , Marcin Jurdzinski (6)

1 SUMO - SUpervision of large MOdular and distributed systems
2 ENS Cachan - École normale supérieure - Cachan
3 LSV - Laboratoire Spécification et Vérification [Cachan]
4 Institut de Mathématiques [Mons]
5 Department of Computer Science [Dresden]
6 Department of Computer Science [Warwick]

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.

Mots clés: Probability; Model checking; Timed automata; Topology

Domaines: Informatique [cs]

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