On the automation of RES via Importance Splitting

Carlos E. Budde
University of Twente
When: Tuesday, July 10, 2018, at 10:00am
Where: Meeting Room n. 515 (Sala Riunioni DINFO, Santa Marta)



In formal model analysis, simulation based approaches like “Statistical 
Model Checking” may suffer from long execution times.
This is exacerbated when the property value to approximate depends on 
an event seldom observed; in those cases rare event simulation (RES) 
techniques can be employed to reduce the variance of the statistical 
estimator and thus speed up convergence [0].
RES techniques typically require non-trivial and domain-specific (or 
even model-specific) user input, which is a setback w.r.t. the 
push-button approach of standard model checking [1,2].
In this talk I will briefly discuss methods to automate the 
implementation of Importance Splitting techniques for RES.
The focus will be on selecting “importance thresholds” and 
“splitting/effort factors”: I will compare two algorithms which (try 
to) automate the choice of these key parameters.
A good performance of the outcomes of these algorithms has been 
empirically demonstrated with several case studies [3].
[0] Rubino, G., Tuffin, B. (eds.): Rare Event Simulation Using Monte 
Carlo Methods. Wiley (2009)
[1] Garvels, M.J.J., Van Ommeren, J.K.C.W., Kroese, D.P.: On the 
importance function in splitting simulation. Eur. Trans. on Telecommun 
[2] Zimmermann, A., Maciel, P.: Importance function derivation for 
RESTART simulations of Petri nets. RESIM 2012 (2012)
[3] Budde, C.E., D’Argenio, P.R., Hartmanns, A.: Better automated 
importance splitting for transient rare events. SETTA 2017 (to appear)