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.
|Title of host publication||Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part I|
|Editors||Armin Biere, David Parker|
|Number of pages||9|
|Publication status||Published - 17 Apr 2020|
|Event||26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020 - Dublin, Ireland|
Duration: 25 Apr 2020 → 30 Apr 2020
Conference number: 26
|Name||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
|Conference||26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020|
|Period||25/04/20 → 30/04/20|
FingerprintDive into the research topics of 'FIG: The Finite Improbability Generator'. Together they form a unique fingerprint.
Software artefact for FIG: the Finite Improbability Generator
Budde, C. E. (Creator), 4TU.Centre for Research Data, 12 May 2020