484
C. E. Budde
distributions. In spite of gallant efforts, this is still out of reach for most other
model checking approaches, making smc unique. The down are rare events.
If there is a very low probability to visit the states characterised by the property ϕ, then most traces will not visit them. Thus the estimate ˆ
γ is either (an
incorrect) 0 or, if a few traces do visit these states, statistical error quantification make ε skyrocket. To counter such phenomenon, n must increase as γ
decreases. Unfortunately, for typical estimates such as the sample mean, it takes
n 384 /γ to build a (rather lax!) ci where δ = 0.95 and ε =
γ
10 . If e.g. γ ≈ 10
−8
then n 38400000000 traces are needed, causing trace-sampling times to grow
unacceptably long. Rare Event Simulation (res [24]) methods tackle this issue.
The two main res methods are importance sampling (is) and importance
splitting (isplit). is compromises the aforementioned up, since it must tamper
the stochastic transitions of the model. Given that the study of non-Markovian
systems is a chief reason to use smc, FIG, a statistical model checker specialised
in res, implements isplit. To deploy an efficient implementation, however,
both importance sampling and splitting require expert knowledge. The novelty
of FIG lies on its automatic derivation of the importance function (and thresholds
and splitting values) required by isplit. This derivation exploits the model and
property under study, resulting in a push-button application of res for smc.
Outline. The way in which FIG approaches res is explained in Sec. 2. Its model
and properties input syntax are presented in Sec. 3. Finally, Sec. 4 mentions some
features of FIG 1.2, before ending the paper with the briefest experimental display.
Related work. Other statistical model checkers offer res methods to some
degree of automation. Plasma Lab implements automatic is [18] and semiautomatic isplit [21] for Markov chains. Its isplit engine offers a wizard that
guides the user to choose an importance function. The wizard exploits a layered decomposition of the property query—not the system model. Via apis,
the isplit engine of Plasma Lab could be extended beyond dtmc models.
SBIP 2.0 [22] implements the same (semiautomatic, property-based) engine for
dtmcs. SBIP offers a richer set of temporal logics to define the property query
in. Cosmos [1] and ftres [26] implement importance sampling on Markov
chains, the latter specialising in systems described as repairable Dynamic Fault
Trees (dfts). All these tools can operate directly on Markovian models, and
none offers fully automated isplit. Instead, the smc tool modes [5] supports
non-Markovian probability distributions and is much closer to the capabilities
of FIG, offering a similar degree of automation. As a matter of fact, all core res
algorithms in modes were inspired in or motivated by the theory behind FIG. On
the one hand, FIG is restricted to fully-stochastic iosa models, whereas modes
can also cope with nondeterminism (e.g. in Markov automata) using the LSS
algorithm [10, 5]. On the other hand, using the batch means method, FIG can
estimate steady-state properties, which modes cannot currently do. Moreover,
FIG 1.2 implements basic functionality to tailor importance functions for dfts.
Previous versions of FIG have been used for scientific experimentation and
research: the theory of [6] was first implemented and exercised with FIG 1.0; and
FIG 1.1 was presented in [2], and last used in an extended journal version of [5].
C. E. Budde
distributions. In spite of gallant efforts, this is still out of reach for most other
model checking approaches, making smc unique. The down are rare events.
If there is a very low probability to visit the states characterised by the property ϕ, then most traces will not visit them. Thus the estimate ˆ
γ is either (an
incorrect) 0 or, if a few traces do visit these states, statistical error quantification make ε skyrocket. To counter such phenomenon, n must increase as γ
decreases. Unfortunately, for typical estimates such as the sample mean, it takes
n 384 /γ to build a (rather lax!) ci where δ = 0.95 and ε =
γ
10 . If e.g. γ ≈ 10
−8
then n 38400000000 traces are needed, causing trace-sampling times to grow
unacceptably long. Rare Event Simulation (res [24]) methods tackle this issue.
The two main res methods are importance sampling (is) and importance
splitting (isplit). is compromises the aforementioned up, since it must tamper
the stochastic transitions of the model. Given that the study of non-Markovian
systems is a chief reason to use smc, FIG, a statistical model checker specialised
in res, implements isplit. To deploy an efficient implementation, however,
both importance sampling and splitting require expert knowledge. The novelty
of FIG lies on its automatic derivation of the importance function (and thresholds
and splitting values) required by isplit. This derivation exploits the model and
property under study, resulting in a push-button application of res for smc.
Outline. The way in which FIG approaches res is explained in Sec. 2. Its model
and properties input syntax are presented in Sec. 3. Finally, Sec. 4 mentions some
features of FIG 1.2, before ending the paper with the briefest experimental display.
Related work. Other statistical model checkers offer res methods to some
degree of automation. Plasma Lab implements automatic is [18] and semiautomatic isplit [21] for Markov chains. Its isplit engine offers a wizard that
guides the user to choose an importance function. The wizard exploits a layered decomposition of the property query—not the system model. Via apis,
the isplit engine of Plasma Lab could be extended beyond dtmc models.
SBIP 2.0 [22] implements the same (semiautomatic, property-based) engine for
dtmcs. SBIP offers a richer set of temporal logics to define the property query
in. Cosmos [1] and ftres [26] implement importance sampling on Markov
chains, the latter specialising in systems described as repairable Dynamic Fault
Trees (dfts). All these tools can operate directly on Markovian models, and
none offers fully automated isplit. Instead, the smc tool modes [5] supports
non-Markovian probability distributions and is much closer to the capabilities
of FIG, offering a similar degree of automation. As a matter of fact, all core res
algorithms in modes were inspired in or motivated by the theory behind FIG. On
the one hand, FIG is restricted to fully-stochastic iosa models, whereas modes
can also cope with nondeterminism (e.g. in Markov automata) using the LSS
algorithm [10, 5]. On the other hand, using the batch means method, FIG can
estimate steady-state properties, which modes cannot currently do. Moreover,
FIG 1.2 implements basic functionality to tailor importance functions for dfts.
Previous versions of FIG have been used for scientific experimentation and
research: the theory of [6] was first implemented and exercised with FIG 1.0; and
FIG 1.1 was presented in [2], and last used in an extended journal version of [5].