Nathalie Bertrand ; Patricia Bouyer ; Thomas Brihaye ; Quentin Menet ; Christel Baier et al. - Stochastic Timed Automata

lmcs:1092 - Logical Methods in Computer Science, December 9, 2014, Volume 10, Issue 4 - https://doi.org/10.2168/LMCS-10(4:6)2014
Stochastic Timed AutomataArticle

Authors: Nathalie Bertrand ORCID; Patricia Bouyer ; Thomas Brihaye ; Quentin Menet ; Christel Baier ORCID; Marcus Groesser ; Marcin Jurdzinski

    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.


    Volume: Volume 10, Issue 4
    Published on: December 9, 2014
    Imported on: March 28, 2013
    Keywords: Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • EQualIS : Enhancing the Quality of Interacting Systems; Funder: European Commission; Code: 308087

    30 Documents citing this article

    Consultation statistics

    This page has been seen 1708 times.
    This article's PDF has been downloaded 746 times.