Stochastic Timed Automata

Publikation: Beitrag in FachzeitschriftForschungsartikelBeigetragenBegutachtung


  • Nathalie Bertrand - , INRIA centre at Rennes University (Autor:in)
  • Patricia Bouyer - , Laboratoire Spécification et Vérification (Autor:in)
  • Thomas Brihaye - , Universite de Mons (Autor:in)
  • Quentin Menet - , Universite de Mons (Autor:in)
  • Christel Baier - , Technische Universität Dresden (Autor:in)
  • Marcus Groesser - , Technische Universität Dresden (Autor:in)
  • Marcin Jurdzinski - , University of Warwick (Autor:in)


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.


Seiten (von - bis)1–73
Fachzeitschrift Logical methods in computer science : LMCS
PublikationsstatusVeröffentlicht - 8 Okt. 2014

Externe IDs

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



  • cs.LO