Heuristic Search for Bounded Model Checking of Probabilistic Automata

We describe a new method for bounded model-checking of probabilistic automata (PAs), based on heuristic search and integrated into the PRISM model-checker. PA models include both probabilistic transitions and nondeterministic choice transitions. Our search-based approach aims to ad- dress weaknesses in statistical and dynamic-programming approaches to checking bounded PCTL properties of proba- bilistic automata. To model-check properties of PA models, we must demonstrate that the property will be satisfied even in the face of an adversary that optimally resolves nondeter- ministic choices. We use heuristically guided AO* search to find the optimal adversary policy and estimate the prob- ability of properties. We adapt techniques from Artificial Intelligence Planning to develop a heuristic that is based on a relaxation of the underlying probability model. This heuristic provides critical guidance to the search algorithm: without it, even very small models are unsolvable. We have implemented our algorithm in the PRISM model-checker, and show cases where it outperforms PRISM’s dynamic pro- gramming methods. We also describe promising directions for future work in search-based PA model-checking, notably introducing further abstraction into the heuristic to address memory issues.