Bertrand, Nathalie and Bouyer, Patricia and Brihaye, Thomas and Menet, Quentin and Baier, Christelet al. - Stochastic Timed Automata

lmcs:1092 - Logical Methods in Computer Science, December 9, 2014, Volume 10, Issue 4
Stochastic Timed Automata

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

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.


Source : oai:arXiv.org:1410.2128
DOI : 10.2168/LMCS-10(4:6)2014
Volume: Volume 10, Issue 4
Published on: December 9, 2014
Submitted on: June 25, 2015
Keywords: Computer Science - Logic in Computer Science


Share

Browsing statistics

This page has been seen 115 times.
This article's PDF has been downloaded 44 times.