Stochastic Timed Automata

A stochastic timed automaton is a purely stochastic process defined on atimed automaton, in which both delays and discrete choices are made randomly.We study the almost-sure model-checking problem for this model, that is, givena stochastic timed automaton A and a property $\Phi$, we want to decide whetherA satisfies $\Phi$ with probability 1. In this paper, we identify severalclasses of automata and of properties for which this can be decided. The proofrelies 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 thealmost-sure model-checking problem. Correctness of the abstraction holds whenautomata are almost-surely fair, which we show, is the case for two largeclasses of systems, single- clock automata and so-called weak-reactiveautomata. Techniques employed in this article gather tools from real-timeverification and probabilistic verification, as well as topological gamesplayed on timed automata.Comment: 40 pages + appendi