We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
HIGH-LEVEL COUNTEREXAMPLES FOR PROBABILISTIC AUTOMATA.
- Authors
WIMMER, RALF; JANSEN, NILS; ÁBRAHÁM, ERIKA; KATOEN, JOOST-PIETER
- Abstract
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.
- Subjects
PROBABILISTIC automata; SYSTEMS theory; COMMAND languages (Computer science); DEBUGGING; COMPUTER systems
- Publication
Logical Methods in Computer Science (LMCS), 2015, Vol 11, Issue 1, p1
- ISSN
1860-5974
- Publication type
Article
- DOI
10.2168/LMCS-11(1:15)2015