FIG: the Finite Improbability Generator
Carlos E. Budde
1
Formal Methods and Tools, University of Twente,
Enschede, the Netherlands c.e.budde@utwente.nl
Abstract. This paper introduces the statistical model checker FIG 1.2,
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.
1 Introduction
In formal analysis of stochastic systems, statistical model checking (smc [33])
emerges as an alternative to numerical techniques such as (exhaustive) probabilistic model checking. Its partial, on-demand state exploration offers a memorylightweight option to exhaustive explorations. At its core, smc integrates Monte
Carlo simulation with formal models, where traces of states are generated dynamically e.g. via discrete event simulation. Such traces are samples of the states
where a (possibly non-Markovian) stochastic model usually ferrets. Given a temporal logic property ϕ that characterises certain states, an smc analysis yields
an estimate ˆ
γ of the actual probability γ with which the model satisfies ϕ. The
estimate ˆ
γ typically comes together with a quantification of the statistical error:
two numbers δ ∈ (0, 1) and ε > 0 such that ˆ
γ ∈ [γ − ε, γ + ε] with probability δ.
Thus, if n traces are sampled, the full smc outcome is the tuple (n, ˆ
γ, δ, ε).
With this statistical quantification—usually presented as a confidence interval (ci) around ˆ
γ—an idea of the quality of an estimation is conveyed. To
increase the quality one must increase the precision (smaller ε) or the confidence
(bigger δ). For fixed confidence, this means a narrower ci around ˆ
γ. The number
of traces n is inversely proportional to ε and to the ci width, so smc trades
memory for runtime or precision when compared to exhaustive methods [5].
This trade-off of smc comes with one up and one down. The up is the capability to analyse systems whose stochastic transitions can have non-Markovian
This work was partially funded by NWO, NS, and ProRail project 15474 (SEQUOIA) and EU project 102112 (SUCCESS).
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 483–491, 2020.
https://doi.org/10.1007/978-3-030-45190-5_27
TACAS
Evaluation
Artifact
2020
Accepted
Carlos E. Budde
1
Formal Methods and Tools, University of Twente,
Enschede, the Netherlands c.e.budde@utwente.nl
Abstract. This paper introduces the statistical model checker FIG 1.2,
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.
1 Introduction
In formal analysis of stochastic systems, statistical model checking (smc [33])
emerges as an alternative to numerical techniques such as (exhaustive) probabilistic model checking. Its partial, on-demand state exploration offers a memorylightweight option to exhaustive explorations. At its core, smc integrates Monte
Carlo simulation with formal models, where traces of states are generated dynamically e.g. via discrete event simulation. Such traces are samples of the states
where a (possibly non-Markovian) stochastic model usually ferrets. Given a temporal logic property ϕ that characterises certain states, an smc analysis yields
an estimate ˆ
γ of the actual probability γ with which the model satisfies ϕ. The
estimate ˆ
γ typically comes together with a quantification of the statistical error:
two numbers δ ∈ (0, 1) and ε > 0 such that ˆ
γ ∈ [γ − ε, γ + ε] with probability δ.
Thus, if n traces are sampled, the full smc outcome is the tuple (n, ˆ
γ, δ, ε).
With this statistical quantification—usually presented as a confidence interval (ci) around ˆ
γ—an idea of the quality of an estimation is conveyed. To
increase the quality one must increase the precision (smaller ε) or the confidence
(bigger δ). For fixed confidence, this means a narrower ci around ˆ
γ. The number
of traces n is inversely proportional to ε and to the ci width, so smc trades
memory for runtime or precision when compared to exhaustive methods [5].
This trade-off of smc comes with one up and one down. The up is the capability to analyse systems whose stochastic transitions can have non-Markovian
This work was partially funded by NWO, NS, and ProRail project 15474 (SEQUOIA) and EU project 102112 (SUCCESS).
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 483–491, 2020.
https://doi.org/10.1007/978-3-030-45190-5_27
TACAS
Evaluation
Artifact
2020
Accepted