2014/06/09 by Bettina Braitling, Luis María Ferrer Fioriti, Hassan Hatefi +3
Computer Science · #cs.LO
paper · pdf · doi:10.4204/eptcs.154.4
published as EPTCS 154, 2014, pp. 48-63 · In Proceedings QAPL 2014, arXiv:1406.1567
arxiv created 2014/06/09 · arxiv updated 2014/06/10
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.