文章基本信息

标题：Stochastic Timed Automata
本地全文：下载
作者：Nathalie Bertrand ; Patricia Bouyer ; Thomas Brihaye 等
期刊名称：Logical Methods in Computer Science
印刷版ISSN：1860-5974
电子版ISSN：1860-5974
出版年度：2014
卷号：10
期号：4
页码：1
DOI：10.2168/LMCS-10(4:6)2014
出版社：Technical University of Braunschweig
摘要：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 ϕ, we want to decide whether A satisfies ϕ 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.
其他关键词：Timed automata, Model checking, Probability, Topology.