Almost-Sure Model-Checking of Reactive Timed Automata

We consider the model of stochastic timed automata, a model in which both delays and discrete choices are made probabilistically. We are interested in the almost-sure model-checking problem, which asks whether the automaton satisfies a given property with probability 1. While this problem was shown decidable for single-clock automata few years ago, it was also proven that the algorithm for this decidability result could not be used for general timed automata. In this paper we describe the subclass of reactive timed automata, and we prove decidability of the almost-sure model-checking problem under that restriction. Decidability relies on the fact that this model is almost-surely fair. As a desirable property of real systems, we show that reactive automata are almost-surely non-Zeno. Finally we show that the almost-sure model-checking problem can be decided for specifications given as deterministic timed automata.