Automation of Importance Splitting Techniques for Rare Event Simulation

Many efficient analytic and numeric approaches exist to study and verify formal descriptions of probabilistic systems. Probabilistic model checking is a prominent example, which can handle several modelling formalisms through various study angles and degrees of detail. However its core resolution algorithms depend on the memoryless property, meaning only Markovian models can be studied, with few limited exceptions. Furthermore the state- space of the model needs to fit in the physical memory of the computer. Discrete-event Monte Carlo simulation provides an alternative for the generality of automata-based stochastic processes. The term statistical model checking has been coined to signify the application of simulation in a model checking environment, where systems are formally described and properties written in some temporal logic (LTL, CSL, PCTL∗, etc.) are answered within the confidence criteria requested by the user. Such simulation approaches can however fail yielding no answer to the query. This typically happens when statistic analysis of the paths generated shows the data available is insufficient to meet the requested confidence criteria, and then more simulation is needed. When the value to estimate depends on the occurrence of rare events, viz. events which are seldom observed in the normal operation of the system, the situation degenerates to infeasible requirements, e.g. two months of standard Monte Carlo simulation may be needed to provide the desired 90% confidence interval. Specialised simulation strategies exist to combat this problem, which lower the variance of the estimator and hence reduce simulation time. Importance splitting is one such technique, which requires a guiding function to steer the generation of paths towards the rare event. This importance function is typically given in an ad hoc fashion by an expert in the field of the model under study. An inadequate choice may lead to inefficient simulation and long computation times. This thesis presents automatic approaches to derive the importance function, based on a formal description of the model and of the property to estimate. Since the basis of estimations is discrete event simulation, general stochastic processes can be covered with these approaches. The modelling formalism is Input/Output Stochastic Automata (IOSA, [DLM16]) and both transient and steady-state (probabilistic) properties involving rare events can be estimated. Since IOSA is a modular formalism, the efficiency of two different techniques has been studied: deriving the importance function from the fully composed model, and deriving it locally in the individual system modules. The latter option alleviates some memory issues but requires composing the locally generated functions into a global importance function, which provided another subject of research also included in this thesis. Prototypical yet extensible tools have been implemented to test the feasibility and efficiency of these automatic techniques which face the rare event simulation problem. Some insight into their implementation and the results of experimentation are presented in the thesis.