Automated compositional importance splitting

Abstract

In the formal verification of stochastic systems, statistical model checking usessimulation to overcome the state space explosion problem of probabilistic modelchecking. Yet its runtime explodes when faced with rare events, unless a rareevent simulation method like importance splitting is used. The effectiveness ofimportance splitting hinges on nontrivial model-specific inputs: an importancefunction with matching splitting thresholds. This prevents its use by non-expertsfor general classes of models. In this paper, we present an automated methodto derive the importance function. It considers both the structure of the modeland of the formula characterising the rare event. It is memory-efficient by ex-ploiting the compositional nature of formal models. We experimentally evaluateit in various combinations with two approaches to threshold selection as well asdifferent splitting techniques for steady-state and transient properties. We findthatRestartsplitting combined with thresholds determined via a new expectedsuccess method most reliably succeeds and performs very well for transient proper-ties. It remains competitive in the steady-state case, which is however challengingto all combinations we consider. All methods are implemented in themodes tool of the Modest Toolset and the Figrare event simulator.