Stochastic Timed Automata

Research output: Contribution to journalResearch articleContributedpeer-review


  • Nathalie Bertrand - , INRIA centre at Rennes University (Author)
  • Patricia Bouyer - , Laboratoire Spécification et Vérification (Author)
  • Thomas Brihaye - , University of Mons (Author)
  • Quentin Menet - , University of Mons (Author)
  • Christel Baier - , Chair of Algebraic and Logical Foundations of Computer Science (Author)
  • Marcus Groesser - , Dresden University of Technology (Author)
  • Marcin Jurdzinski - , University of Warwick (Author)


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 $\Phi$, we want to decide whether A satisfies $\Phi$ 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.


Original languageEnglish
Pages (from-to)1–73
Journal Logical methods in computer science : LMCS
Issue number4
Publication statusPublished - 8 Oct 2014

External IDs

Scopus 84916919055
ORCID /0000-0002-5321-9343/work/142236769



  • cs.LO