State-of-the-art probabilistic model checkers perform verification on explicit-state Markov models defined in a high-level programming formalism like the PRISM modeling language. Typically, the low-level models resulting from such program-like specifications exhibit lots of structure such as repeating subpatterns. Established techniques like probabilistic bisimulation minimization are able to exploit these structures; however, they operate directly on the explicit-state model. On the other hand, methods for reducing structured state spaces by reasoning about the high-level program have not been investigated that much. In this paper, we present a new, simple, and fully automatic program-level technique to reduce the underlying Markov model. Our approach aims at computing the summary behavior of adjacent locations in the program's control-flow graph, thereby obtaining a program with fewer "control states". This reduction is immediately reflected in the program's operational semantics, enabling more efficient model checking. A key insight is that in principle, each (combination of) program variable(s) with finite domain can play the role of the program counter that defines the flow structure. Unlike most other reduction techniques, our approach is property-directed and naturally supports unspecified model parameters. Experiments demonstrate that our simple method yields state-space reductions of up to 80% on practically relevant benchmarks.
翻译:常规情况下,由类似程序规格产生的低级别模型展示了大量结构,例如重复子流。 常规情况下,由类似程序规格生成的低级别模型展示了大量结构,例如重复子流体。 常规中,概率优化最小化等既定技术能够利用这些结构; 但是,它们直接在明确状态模型上运作。 另一方面,通过对高级方案进行推理来减少结构化国家空间的方法没有得到如此多的调查。 在本文中,我们提出了一个新的、简单和完全自动的程序级技术,用于减少基底的马尔科夫模型。 我们的方法旨在计算方案控制流图中相邻地点的概要行为,从而获得一个较少“控制状态”的程序。 这种减少立即反映在方案的操作结构精度模型中,使得能够更高效地进行模型检查。 关键的观点是,在原则上,每个具有有限域的(组合)程序变量都可以发挥程序反作用,从而界定流动结构。 与大多数简单化的缩小空间参数相比,我们的实际减少率方法是不受限制的。