期刊
LOGICAL METHODS IN COMPUTER SCIENCE
卷 10, 期 4, 页码 -出版社
LOGICAL METHODS COMPUTER SCIENCE E V
DOI: 10.2168/LMCS-10(4:6)2014
关键词
Timed automata; Model checking; Probability; Topology
资金
- ANR project ImpRo [ANR-10-BLAN-0317]
- ERC Starting grant EQualIS [308087]
- ARC project [AUWB-2010-10/15-UMONS-3]
- F.R.S.-FNRS
- FRFC project [2.4545.11]
- EU-FP7 project CASST-ING [601148]
- grant of FRIA
- German Research Council (DFG) through the collaborative research centre 912 Highly-Adaptive Energy-Efficient Computing (HAEC)
- cluster of excellence Centre for Advancing Electronics Dresden (cfAED)
- EU-FP7 project MEALS [295261]
- EU
- State Saxony through the ESF young researcher groups IMData [100098198]
- SREX [100111037]
- Agence Nationale de la Recherche (ANR) [ANR-10-BLAN-0317] Funding Source: Agence Nationale de la Recherche (ANR)
- EPSRC [EP/D063191/1] Funding Source: UKRI
- Engineering and Physical Sciences Research Council [EP/D063191/1] Funding Source: researchfish
- European Research Council (ERC) [308087] Funding Source: European Research Council (ERC)
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.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据