This paper introduces the statistical model checker FIGV, that estimates transient and steady-state reachability properties in stochastic automata. This software tool specialises in Rare Event Simulation via importance splitting, and implements the algorithms RESTART and Fixed Effort. FIG is push-button automatic since the user need not define an importance function: this function is derived from the model specification plus the property query. The tool operates with Input/Output Stochastic Automata with Urgency, aka IOSA models, described either in the native syntax or in the JANI exchange format. The theory backing FIG has demonstrated good efficiency, comparable to optimal importance splitting implemented ad hoc for specific models. Written in C++, FIG can outperform other state-of-the-art tools for Rare Event Simulation.

FIG: The Finite Improbability Generator / Budde, Carlos E.. - ELETTRONICO. - 12078:(2020), pp. 483-491. (Intervento presentato al convegno 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020 tenutosi a Dublin, Ireland nel 25–30, April 2020) [10.1007/978-3-030-45190-5_27].

FIG: The Finite Improbability Generator

Carlos E. Budde
2020-01-01

Abstract

This paper introduces the statistical model checker FIGV, that estimates transient and steady-state reachability properties in stochastic automata. This software tool specialises in Rare Event Simulation via importance splitting, and implements the algorithms RESTART and Fixed Effort. FIG is push-button automatic since the user need not define an importance function: this function is derived from the model specification plus the property query. The tool operates with Input/Output Stochastic Automata with Urgency, aka IOSA models, described either in the native syntax or in the JANI exchange format. The theory backing FIG has demonstrated good efficiency, comparable to optimal importance splitting implemented ad hoc for specific models. Written in C++, FIG can outperform other state-of-the-art tools for Rare Event Simulation.
2020
Tools and Algorithms for the Construction and Analysis of Systems 26th International Conference, TACAS 2020
Cham, Svizzera
Springer Nature Switzerland
978-3-030-45189-9
978-3-030-45190-5
Budde, Carlos E.
FIG: The Finite Improbability Generator / Budde, Carlos E.. - ELETTRONICO. - 12078:(2020), pp. 483-491. (Intervento presentato al convegno 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020 tenutosi a Dublin, Ireland nel 25–30, April 2020) [10.1007/978-3-030-45190-5_27].
File in questo prodotto:
File Dimensione Formato  
paper_camera_ready.pdf

accesso aperto

Descrizione: Article camera-ready
Tipologia: Post-print referato (Refereed author’s manuscript)
Licenza: Creative commons
Dimensione 777.7 kB
Formato Adobe PDF
777.7 kB Adobe PDF Visualizza/Apri
978-3-030-45190-5_27.pdf

accesso aperto

Tipologia: Versione editoriale (Publisher’s layout)
Licenza: Creative commons
Dimensione 330.38 kB
Formato Adobe PDF
330.38 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/314701
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 4
  • ???jsp.display-item.citation.isi??? ND
social impact