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

TL;DR

This paper introduces a novel abstraction and refinement method for Markov automata, enabling significant size reduction and improved manageability of complex models with probabilistic and nondeterministic features.

Contribution

It presents a new game-based and menu-based abstraction technique specifically designed for Markov automata, addressing their complexity and size issues.

Findings

Significant reduction in model size through abstraction

Effective handling of probabilistic and nondeterministic features

Potential for improved analysis of complex systems

Abstract

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.