Name
Abstract | ||
|---|---|---|
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, singleclock 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. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.2168/LMCS-10(4:6)2014 | LOGICAL METHODS IN COMPUTER SCIENCE |
Keywords | Field | DocType |
Timed automata,Model checking,Probability,Topology | Discrete mathematics,Quantum finite automata,Automata theory,Deterministic automaton,Mobile automaton,Computer science,Theoretical computer science,Timed automaton,Stochastic cellular automaton,Probabilistic automaton,ω-automaton | Journal |
Volume | Issue | ISSN |
10 | 4 | 1860-5974 |
Citations | PageRank | References |
9 | 0.50 | 16 |
Authors | ||
7 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Nathalie Bertrand | 1 | 250 | 17.84 |
| Patricia Bouyer | 2 | 735 | 37.19 |
| Thomas Brihaye | 3 | 460 | 35.91 |
| Quentin Menet | 4 | 18 | 2.02 |
| Christel Baier | 5 | 3053 | 185.85 |
| Marcus Größer | 6 | 334 | 18.23 |
| Marcin Jurdzinski | 7 | 426 | 29.31 |