Abstract
Original language | English |
---|---|
Pages (from-to) | 90 - 108 |
Number of pages | 19 |
Journal | Science of computer programming |
Volume | 174 |
DOIs | |
Publication status | Published - 2019 |
Fingerprint
Keywords
- Rare event simulation
- Importance splitting
- Statistical model checking
Cite this
}
Automated compositional importance splitting. / Budde, Carlos E.; D'Argenio, Pedro R.; Hartmanns, Arnd (Corresponding Author).
In: Science of computer programming, Vol. 174, 2019, p. 90 - 108.Research output: Contribution to journal › Article › Academic › peer-review
TY - JOUR
T1 - Automated compositional importance splitting
AU - Budde, Carlos E.
AU - D'Argenio, Pedro R.
AU - Hartmanns, Arnd
PY - 2019
Y1 - 2019
N2 - In the formal verification of stochastic systems, statistical model checking uses simulation to overcome the state space explosion problem of probabilistic model checking. 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 present an automated method to derive the importance function. It considers both the structure of the model and of the formula characterising the rare event. It is memory-efficient by exploiting the compositional nature of formal models. We experimentally evaluate it in various combinations with two approaches to threshold selection as well as different splitting techniques for steady-state and transient properties. We find that Restart splitting combined with thresholds determined via a new expected success method most reliably succeeds and performs very well for transient properties. It remains competitive in the steady-state case, which is however challenging to all combinations we consider. All methods are implemented in the modes tool of the Modest Toolset and in the Fig rare event simulator.
AB - In the formal verification of stochastic systems, statistical model checking uses simulation to overcome the state space explosion problem of probabilistic model checking. 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 present an automated method to derive the importance function. It considers both the structure of the model and of the formula characterising the rare event. It is memory-efficient by exploiting the compositional nature of formal models. We experimentally evaluate it in various combinations with two approaches to threshold selection as well as different splitting techniques for steady-state and transient properties. We find that Restart splitting combined with thresholds determined via a new expected success method most reliably succeeds and performs very well for transient properties. It remains competitive in the steady-state case, which is however challenging to all combinations we consider. All methods are implemented in the modes tool of the Modest Toolset and in the Fig rare event simulator.
KW - Rare event simulation
KW - Importance splitting
KW - Statistical model checking
U2 - 10.1016/j.scico.2019.01.006
DO - 10.1016/j.scico.2019.01.006
M3 - Article
VL - 174
SP - 90
EP - 108
JO - Science of computer programming
JF - Science of computer programming
SN - 0167-6423
ER -