Artículo
Better automated importance splitting for transient rare events
Fecha de publicación:
10/2017
Editorial:
Springer Verlag Berlín
Revista:
Lecture Notes in Computer Science
ISSN:
0302-9743
Idioma:
Inglés
Tipo de recurso:
Artículo publicado
Clasificación temática:
Resumen
Statistical model checking uses simulation to overcome the state space explosion problem in formal verification. Yet its runtime explodes when faced with rare events, unless a rare event simulation method like importance splitting is used. The effectiveness of importance splitting hinges on nontrivial model-specific inputs: an importance function with matching splitting thresholds. This prevents its use by non-experts for general classes of models. In this paper, we propose new method combinations with the goal of fully automating the selection of all parameters for importance splitting. We focus on transient (reachability) properties, which particularly challenged previous techniques, and present an exhaustive practical evaluation of the new approaches on case studies from the literature. We find that using Restart simulations with a compositionally constructed importance function and thresholds determined via a new expected success method most reliably succeeds and performs very well. Our implementation within the Modest Toolset supports various classes of formal stochastic models and is publicly available.
Archivos asociados
Licencia
Identificadores
Colecciones
Articulos(CCT - CORDOBA)
Articulos de CTRO.CIENTIFICO TECNOL.CONICET - CORDOBA
Articulos de CTRO.CIENTIFICO TECNOL.CONICET - CORDOBA
Citación
Budde, Carlos Ernesto; D'argenio, Pedro Ruben; Hartmanns, Arnd; Better automated importance splitting for transient rare events; Springer Verlag Berlín; Lecture Notes in Computer Science; 10606 LNCS; 10-2017; 42-58
Compartir
Altmétricas