Stochastic Timed Automata
Research output: Contribution to journal › Research article › Contributed › peer-review
Contributors
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, 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.
Details
Original language | English |
---|---|
Pages (from-to) | 1–73 |
Journal | Logical methods in computer science : LMCS |
Volume | 10 |
Issue number | 4 |
Publication status | Published - 8 Oct 2014 |
Peer-reviewed | Yes |
External IDs
Scopus | 84916919055 |
---|---|
ORCID | /0000-0002-5321-9343/work/142236769 |
Keywords
Keywords
- cs.LO