The Modest Toolset Contact us Documentation Examples Publications Download

Home

Models Languages Tools Download

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.

Models

At the core of the Modest Toolset is the model of networks of stochastic hybrid automata (SHA), which combine nondeterministic choices, 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.

Languages

The Modest Toolset currently supports the following input languages:

• Modest: a high-level compositional modelling language for stochastic hybrid systems [HHHK13].
• JANI: a model exchange format for networks of quantitative automata [BDHHJT17], part of the JANI specification.

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.

Tools

The Modest Toolset comprises the following tools:

• mcsta is a disk-based explicit-state model checker for STA, PTA and MDP.
• moconv converts models between the Toolset's input languages, in particular from Modest to jani-model and back.
• modes [BDHS18] is a statistical model checker for SHA, STA, PTA and MDP.
• modysh [MKHH21] is a probabilistic model checker for MDP based on dynamic search and heuristic planning techniques.
• mosta visualises the SHA semantics of a model by generating a graphical representation of the automata.
• prohver [HHHK13] is a safety model checker for SHA.

Download

The Modest Toolset can be downloaded for evaluation purposes.
We provide binaries for Windows, Linux and Mac OS. (System requirements)