The main implementation of probabilistic model checking (PMC) [1]}, [2]} in the Modest Toolset is in mcsta [3]}:
an explicit-state model checker that provides a unique disk-based approach to mitigate the state space explosion problem [3]}.
It includes efficient model reductions such as the essential states abstraction [5]}, and provides state-of-the-art algorithms for model checking MA [6]}.
The Modest Toolset's statistical model checker modes [7]}complements mcsta's capabilities for cases where model checking cannot be applied, such as when facing state space explosion or models with non-Markovian probability distributions like STA.
Statistical model checking (SMC) [8]} is, in essence, Monte Carlo simulation applied to formal models and properties.
A constant-memory technique, it however incurs an explosion in runtime when faced with rare events, and does not directly support nondeterministic models such as MDP.
The modes tool addresses these shortcomings by providing rare event simulation [9]} via a highly automated implementation of importance splitting [10]}, and by offering the lightweight scheduler sampling technique [11]} for MDP, PTA [12]}, [13]}, and (with limitations) stochastic-time models like MA and STA [14]}.
Other members of the Modest Toolset provide specialised analysis algorithms such as variants of the probabilistic planning algorithm LRTDP [15]} for MDP in modysh [16]} or an abstraction-based approach to safety verification of SHA in prohver [17]}.
