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 .
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 .
 Rubino, G., Tuffin, B. (eds.): Rare Event Simulation Using Monte
Carlo Methods. Wiley (2009)
 Garvels, M.J.J., Van Ommeren, J.K.C.W., Kroese, D.P.: On the
importance function in splitting simulation. Eur. Trans. on Telecommun
 Zimmermann, A., Maciel, P.: Importance function derivation for
RESTART simulations of Petri nets. RESIM 2012 (2012)
 Budde, C.E., D’Argenio, P.R., Hartmanns, A.: Better automated
importance splitting for transient rare events. SETTA 2017 (to appear)