MeGARA: Menu-based Game Abstraction and Abstraction Refinement of Markov Automata

Bettina Braitling
Luis María Ferrer Fioriti
Hassan Hatefi
Ralf Wimmer
Bernd Becker
Holger Hermanns

Markov automata combine continuous time, probabilistic transitions, and nondeterminism in a single model. They represent an important and powerful way to model a wide range of complex real-life systems. However, such models tend to be large and difficult to handle, making abstraction and abstraction refinement necessary. In this paper we present an abstraction and abstraction refinement technique for Markov automata, based on the game-based and menu-based abstraction of probabilistic automata. First experiments show that a significant reduction in size is possible using abstraction.

In Nathalie Bertrand and Luca Bortolussi: Proceedings Twelfth International Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2014), Grenoble, France, 12-13 April 2014, Electronic Proceedings in Theoretical Computer Science 154, pp. 48–63.
Published: 6th June 2014.

ArXived at: https://dx.doi.org/10.4204/EPTCS.154.4 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org