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.

Automated compositional importance splitting / Budde, Carlos E.; D'Argenio, Pedro R.; Hartmanns, Arnd. - In: SCIENCE OF COMPUTER PROGRAMMING. - ISSN 0167-6423. - ELETTRONICO. - 174:(2019), pp. 90-108. [10.1016/j.scico.2019.01.006]

Automated compositional importance splitting

Carlos E. Budde;
2019-01-01

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.
2019
Budde, Carlos E.; D'Argenio, Pedro R.; Hartmanns, Arnd
Automated compositional importance splitting / Budde, Carlos E.; D'Argenio, Pedro R.; Hartmanns, Arnd. - In: SCIENCE OF COMPUTER PROGRAMMING. - ISSN 0167-6423. - ELETTRONICO. - 174:(2019), pp. 90-108. [10.1016/j.scico.2019.01.006]
File in questo prodotto:
File Dimensione Formato  
paper.pdf

accesso aperto

Descrizione: Article camera-ready
Tipologia: Post-print referato (Refereed author’s manuscript)
Licenza: Creative commons
Dimensione 705.62 kB
Formato Adobe PDF
705.62 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/314709
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 14
  • ???jsp.display-item.citation.isi??? 4
social impact