A Modest Approach to Checking Probabilistic Timed Automata
A Modest Approach to Checking Probabilistic Timed Automata
复制标题
DOI：
10.1109/qest.2009.41
复制
发表时间：
2009-09
期刊：
影响因子：
--
通讯作者：
A. Hartmanns;H. Hermanns
中科院分区：
文献类型：
--
作者：
A. Hartmanns;H. Hermanns
概率时间自动机（PTA）联合收割机了离散概率选择、真实的性和非确定性。本文提出了一个全自动的工具，模型检查PTA的概率和预期的可达性。PTA是在Modest中指定的，Modest是一种高级组合建模语言，包括异常处理，动态并行和递归等功能，因此可以方便地指定模型。对于模型检查，我们使用时间的积分语义，用有界整数变量表示时钟。这使得使用概率模型检查器PRISM作为分析后端成为可能。我们描述的方法及其实施的细节，并报告三个不同的案例研究所获得的结果。
Probabilistic timed automata (PTA) combine discrete probabilistic choice, real time and nondeterminism. This paper presents a fully automatic tool for model checking PTA with respect to probabilistic and expected reachability properties. PTA are specified in Modest, a high-level compositional modelling language that includes features such as exception handling, dynamic parallelism and recursion, and thus enables model specification in a convenient fashion. For model checking, we use an integral semantics of time, representing clocks with bounded integer variables. This makes it possible to use the probabilistic model checker PRISM as analysis backend. We describe details of the approach and its implementation, and report results obtained for three different case studies.