A Modest Approach to Markov Automata
本文扩展了MODEST语言以简洁模块化地描述大型马尔可夫自动机模型，并评估了mcsta模型检测器在时间有界和长期平均奖励属性上的性能与可扩展性，同时介绍了基于BRTDP的部分探索方法和轻量级调度器采样以应对状态空间爆炸和非确定性挑战。
Markov automata are a compositional modelling formalism with continuous stochastic time, discrete probabilities, and nondeterministic choices. In this article, we present extensions to M ODEST , an expressive high-level language with roots in process algebra, that allow large Markov automata models to be specified in a succinct, modular way. We illustrate the advantages of M ODEST over alternative languages. Model checking Markov automata models requires dedicated algorithms for time-bounded and long-run average reward properties. We describe and evaluate the state-of-the-art algorithms implemented in the mcsta model checker of the M ODEST T OOLSET . We find that mcsta improves the performance and scalability of Markov automata model checking compared to earlier and alternative tools. We explain a partial-exploration approach based on the BRTDP method designed to mitigate the state space explosion problem of model checking, and experimentally evaluate its effectiveness. This problem can be avoided entirely by purely simulation-based techniques, but the nondeterminism in Markov automata hinders their straightforward application. We explain how lightweight scheduler sampling can make simulation possible, and provide a detailed evaluation of its usefulness on several benchmarks using the M ODEST T OOLSET ’s modes simulator.