# Se doctoró Carlos Budde

El 29 de Mayo pasado Carlos E. Budde defendió su tesis doctoral titulada *"Automation of Importance Splitting Techniques for Rare Event Simulation"*. Su jurado de tesis estuvo formado por Arnd Hartmanns, Germán Regis y Damián Barsotti.

**Doctorado:** *Carlos E. Budde***Título de la tesis:** *Automation of Importance Splitting Techniques for Rare Event Simulation*

**Resumen:**

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 approach 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, i.e. more simulation is needed. When the value to estimate depends on the occurrence of rare events which are seldom observed, 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.

Specialized 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 later 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.

A prototypical yet extensible tool has been implemented to test the feasibility and efficiency of these automatic techniques which face the rare event simulation problem. Some insight into its implementation and the results of experimentation are presented along the thesis.