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

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

Publikováno v: EPTCS 154, 2014, pp. 48-63

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 diffi

Externí odkaz: http://arxiv.org/abs/1406.2068

Abstraction-Based Computation of Reward Measures for Markov Automata.

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

Publikováno v: Verification, Model Checking & Abstract Interpretation 16th International Conference, VMCAI 2015, Mumbai, India, January 12-14, 2015. Proceedings; 2015, p172-189, 18p

Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model Checking.

Autor: Wimmer, Ralf, Braitling, Bettina, Becker, Bernd

Publikováno v: Verification, Model Checking & Abstract Interpretation (9783540938996); 2009, p366-380, 15p

SUPERB

Autor: Engelke, Piet, Becker, Bernd, Renovell, Michel, Schloeffel, Juergen, Braitling, Bettina, Polian, Ilia

Publikováno v: ACM Transactions on Design Automation of Electronic Systems; August 2009, Vol. 14 Issue: 4 p1-21, 21p