Quantitative Modelling and Verification
The Modest Toolset supports the modelling and analysis of hybrid, real-time, distributed and stochastic systems.
A modular framework centered around the stochastic hybrid automata formalism [HHHK13]
and supporting the JANI specification,
it provides a variety of input languages and analysis backends.
At the core of the Modest Toolset is the model of networks of stochastic hybrid automata (SHA), which combine
continuous system dynamics,
stochastic decisions and timing, and
real-time behaviour, including nondeterministic delays.
A wide range of well-known and extensively studied formalisms in modelling and verification can be seen as special cases of SHA:
STA (stochastic timed automata), the original semantic foundation of Modest [BDHK06],
are SHA without complex continuous behaviour (i.e. without variables whose evolution over time is governed by differential equations or inclusions, except for clock variables).
PTA (probabilistic timed automata) are obtained from STA by restricting stochastic decisions to choices based on finite-support probability distributions
(such as the discrete uniform or the Bernoulli distribution).
TA (timed automata) are nonprobabilistic PTA. Delays and discrete choices can still be nondeterministic, but not stochastic.
TA are widely used to model real-time systems and requirements.
PA/MDP (probabilistic automata/Markov decision processes), on the other hand, can be seen as PTA without the notion of time, i.e. without clock variables or delays.
PA theory focuses on compositionality and simulation relations between models, while MDP are usually considered with costs or rewards, but both are essentially the same model.
LTS (labelled transition systems), alternatively Kripke structures or finite automata, are the most basic, fundamental model for verification.
Allowing nondeterministic choices, they are supported by a wide range of model-checking tools of impressive scalability.
DTMC (discrete-time Markov chains) are the basic discrete probabilistic model. As a model without nondeterminism, they are not only amenable to a wide range of numerical
analysis approaches, but also ideally suited for simulation.
CTMC, IMC and MA (continuous-time Markov chains, interactive Markov chains and Markov automata) form the family of stochastic models based on the
notion of exponentially distributed delays, which can be represented in STA via a combination of sampling from the exponential distribution and subsequently waiting the
sampled amount of time using a dedicated clock variable.
The Modest Toolset currently supports the following input languages:
a high-level compositional modelling language for stochastic hybrid systems [HHHK13].
a model exchange format for networks of quantitative automata [BDHHJT17],
part of the JANI specification.
an extension of scenario-aware dataflow with continuous probability distributions, nondeterminism, and costs [HHB16].
Due to the toolset's modular nature, new input languages can easily be added by implementing a small set of interfaces and providing a semantics in terms of SHA.
The Modest Toolset comprises the following tools:
is a disk-based explicit-state model checker for STA, PTA and MDP.
is a statistical model checker for SHA, STA, PTA and MDP.
is a safety model checker for SHA.
visualises the SHA semantics of a model by generating a graphical representation of the automata.
converts models between the Toolset's input languages, in particular from Modest to jani-model and back.
The Modest Toolset can be downloaded for evaluation purposes.
All tools have been tested to work on Windows, Linux and Mac OS. (System requirements)