Quantitative Evaluation of Systems, International Conference on (2012)

London, United Kingdom United Kingdom

Sept. 17, 2012 to Sept. 20, 2012

ISBN: 978-1-4673-2346-8

pp: 138-147

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/QEST.2012.10

ABSTRACT

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.

INDEX TERMS

Automata, Stochastic processes, Clocks, Cost accounting, Delay, Exponential distribution, Cooling

CITATION

P. Bouyer, T. Brihaye, M. Jurdzinski and Q. Menet, "Almost-Sure Model-Checking of Reactive Timed Automata,"

*Quantitative Evaluation of Systems, International Conference on(QEST)*, London, United Kingdom United Kingdom, 2012, pp. 138-147.

doi:10.1109/QEST.2012.10

CITATIONS

SEARCH