Automated compositional importance splitting

Carlos E. Budde, Pedro R. D'Argenio, Arnd Hartmanns (Corresponding Author)

Research output: Contribution to journalArticleAcademicpeer-review

30 Downloads (Pure)

Abstract

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.
Original languageEnglish
Pages (from-to)90 - 108
Number of pages19
JournalScience of computer programming
Volume174
DOIs
Publication statusPublished - 2019

Fingerprint

Model checking
Stochastic systems
Hinges
Explosions
Simulators
Data storage equipment
Statistical Models
Formal verification

Keywords

  • Rare event simulation
  • Importance splitting
  • Statistical model checking

Cite this

Budde, Carlos E. ; D'Argenio, Pedro R. ; Hartmanns, Arnd. / Automated compositional importance splitting. In: Science of computer programming. 2019 ; Vol. 174. pp. 90 - 108.
@article{cb88a74aa6d340bdbc7d8b5790fce9f7,
title = "Automated compositional importance splitting",
abstract = "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.",
keywords = "Rare event simulation, Importance splitting, Statistical model checking",
author = "Budde, {Carlos E.} and D'Argenio, {Pedro R.} and Arnd Hartmanns",
year = "2019",
doi = "10.1016/j.scico.2019.01.006",
language = "English",
volume = "174",
pages = "90 -- 108",
journal = "Science of computer programming",
issn = "0167-6423",
publisher = "Elsevier",

}

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 journalArticleAcademicpeer-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 -