Automated compositional importance splitting

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

    Research output: Contribution to journalArticleAcademicpeer-review

    1 Citation (Scopus)
    64 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

    Keywords

    • Rare event simulation
    • Importance splitting
    • Statistical model checking

    Fingerprint Dive into the research topics of 'Automated compositional importance splitting'. Together they form a unique fingerprint.

  • Cite this