The computation of counterexamples for probabilistic systems has gained a lot of attention during the last few years. All of the proposed methods focus on the situation when the probabilities of certain events are too high. In this paper we investigate how counterexamples for properties concerning expected costs (or, equivalently, expected rewards) of events can be computed. We propose methods to extract a minimal subsystem which already leads to costs beyond the allowed bound. Besides these exact methods, we present heuristic approaches based on path search and on best-first search, which are applicable to very large systems when deriving a minimum subsystem becomes infeasible due to the system size. Experiments show that we can compute counterexamples for systems with millions of states.
CITATION STYLE
Quatmann, T., Jansen, N., Dehnert, C., Wimmer, R., Àbrahàm, E., Katoen, J. P., & Becker, B. (2015). Counterexamples for expected rewards. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9109, pp. 435–452). Springer Verlag. https://doi.org/10.1007/978-3-319-19249-9_27
Mendeley helps you to discover research relevant for your work.