Paper accepted at FM 2015

The paper “Counterexamples for Expected Rewards” by Tim Quatmann, Nils Jansen, Christian Dehnert, Ralf Wimmer, Erika ÁbrahámJoost-Pieter Katoen, and Bernd Becker was accepted for publication at the 20th International Symposium on Formal Methods (FM) 2015. The paper presents the first approaches on counterexamples for discrete-time Markov chains and expected reward properties. Methods are proposed to extract a minimal subsystem which already leads to costs beyond the allowed bound. Besides these exact methods, heuristic approaches based on path search and on best-first search, which are applicable to very large systems are given. Experiments show that counterexamples for systems with millions of states can be computed.