A Modest Approach to Modelling and Checking Markov Automata (Artifact)

Y. (Yuliya) Butkova
Markov automata are a compositional modelling formalism with continuous stochastic time, discrete probabilities, and nondeterministic choices. In our QEST 2019 paper titled "A Modest Approach to Modelling and Checking Markov Automata", we present extensions to the Modest language and the 'mcsta' model checker of the Modest Toolset to describe and analyse Markov automata models. The verification of Markov automata models requires dedicated algorithms for time-bounded probabilistic reachability and long-run average rewards. In the paper, we...
This data repository is not currently reporting usage information. For information on how your repository can submit usage information, please see our documentation.