In addition to rigorously checking whether a system conforms to a specification, model checking can provide valuable feedback in the form of succinct and understandable counterexamples. In the context of probabilistic systems, path- and subsystem-based counterexamples at the state-space level can be of limited use in debugging. As many probabilistic systems are described in a guarded command language like the one used by the popular model checker Prism, a technique identifying a subset of critical commands has recently been proposed. Based on repeatedly solving MaxSat instances, our novel approach to computing a minimal critical command set achieves a speed-up of up to five orders of magnitude over the previously existing technique.
CITATION STYLE
Dehnert, C., Jansen, N., Wimmer, R., Ábrahám, E., & Katoen, J. P. (2014). Fast debugging of PRISM models. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8837, pp. 146–162). Springer Verlag. https://doi.org/10.1007/978-3-319-11936-6_11
Mendeley helps you to discover research relevant for your work.