Title: Abstraction-based Computation of Reward Measures for Markov Automata

Speaker: Ralf Wimmer (Freiburg University, Germany)

         www2.informatik.uni-freiburg.de/~wimmer

Time: 2nd December 2014, 10:30

Venue: Seminar Room (334), Level 3, Building 5, Institute of Software, CAS

Abstract:

Markov automata allow us to model a wide range of complex real-life systems by combining continuous stochastic timing with probabilistic transitions and nondeterministic choices. By adding a reward function it is possible to model costs like the energy consumption of a system as well. However, models of real-life systems tend to be large, and the analysis methods for such powerful models like Markov (reward) automata do not scale well, which limits their applicability. To solve this problem we present an abstraction technique for Markov reward automata, based on stochastic games, together with automatic refinement methods for the computation of time-bounded accumulated reward properties. Experiments show a significant speed-up and reduction in system size compared to direct analysis methods.

Biography:

Ralf Wimmer is a post-doctoral researcher at the Chair of Computer Architecture at Freiburg University, Germany. His research interests include symbolic methods and solver technologies for the verification of embedded system, focusing on state space reduction and counterexample generation for probabilistic systems. He has written over 30 refereed publications and serves as a member of the program committee of TACAS 2013. Three most relevant publications in recent years:

[1] Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika ábrahám, Joost-Pieter Katoen, Bernd Becker: High-level counterexamples for Probabilistic Automata. Proc. of the Int'l Conf. on Quantitative Evaluation of Systems 2013 (to appear)

[2] Ralf Wimmer, Bernd Becker, Nils Jansen, Erika ábrahám, Joost-Pieter Katoen: Minimal Critical Subsystems for Discrete-Time Markov Models.

Proc. of the Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems 2012, pp. 299-314, Lecture Notes in Computer Science vol. 7214, Springer

[3] Ralf Wimmer, Salem Derisavi, Holger Hermanns: Symbolic Partition Refinement with Automatic Balancing of Time and Space. Performance Evaluation 67(9), pp. 815-835, 2010