Stochastic Timed Automata
Publikation: Beitrag in Fachzeitschrift › Forschungsartikel › Beigetragen › Begutachtung
Beitragende
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
Originalsprache | Englisch |
---|---|
Seiten (von - bis) | 1–73 |
Fachzeitschrift | Logical methods in computer science : LMCS |
Jahrgang | 10 |
Ausgabenummer | 4 |
Publikationsstatus | Veröffentlicht - 8 Okt. 2014 |
Peer-Review-Status | Ja |
Externe IDs
Scopus | 84916919055 |
---|
Schlagworte
Schlagwörter
- cs.LO