High-level Counterexamples for Probabilistic Automata

Ralf Wimmer; Nils Jansen; Erika Ã?brahÃ?m; Joost-Pieter Katoen

doi:10.2168/LMCS-11(1:15)2015

Ralf Wimmer ; Nils Jansen ; Erika Ã?brahÃ?m ; Joost-Pieter Katoen - High-level Counterexamples for Probabilistic Automata

lmcs:945 - Logical Methods in Computer Science, March 31, 2015, Volume 11, Issue 1 - https://doi.org/10.2168/LMCS-11(1:15)2015

High-level Counterexamples for Probabilistic AutomataArticle

Authors: Ralf Wimmer ; Nils Jansen ; Erika Ã?brahÃ?m ; Joost-Pieter Katoen

Providing compact and understandable counterexamples for violated system properties is an essential task in model checking. Existing works on counterexamples for probabilistic systems so far computed either a large set of system runs or a subset of the system's states, both of which are of limited use in manual debugging. Many probabilistic systems are described in a guarded command language like the one used by the popular model checker PRISM. In this paper we describe how a smallest possible subset of the commands can be identified which together make the system erroneous. We additionally show how the selected commands can be further simplified to obtain a well-understandable counterexample.

https://doi.org/10.2168/LMCS-11(1:15)2015

Source: arXiv.org:1305.5055

Volume: Volume 11, Issue 1

Published on: March 31, 2015

Imported on: January 6, 2014

Keywords: Computer Science - Software Engineering,Computer Science - Logic in Computer Science

Licence: arXiv.org - Non-exclusive license to distribute

Funding:

Source : OpenAIRE Graph