Counterexample Generation in Probabilistic Model Checking

Tingting Han, Joost P. Katoen, B. Damman

Research output: Contribution to journalArticleAcademicpeer-review

70 Citations (Scopus)
44 Downloads (Pure)

Abstract

Providing evidence for the refutation of a property is an essential, if not the most important, feature of model checking. This paper considers algorithms for counterexample generation for probabilistic CTL formulae in discrete-time Markov chains. Finding the strongest evidence (i.e., the most probable path) violating a (bounded) until-formula is shown to be reducible to a single-source (hop-constrained) shortest path problem. Counterexamples of smallest size that deviate most from the required probability bound can be obtained by applying (small amendments to) k-shortest (hop-constrained) paths algorithms. These results can be extended to Markov chains with rewards, to LTL model checking, and are useful for Markov decision processes. Experimental results show that typically the size of a counterexample is excessive. To obtain much more compact representations, we present a simple algorithm to generate (minimal) regular expressions that can act as counterexamples. The feasibility of our approach is illustrated by means of two communication protocols: leader election in an anonymous ring network and the Crowds protocol.
Original languageUndefined
Article number10.1109/TSE.2009.5
Pages (from-to)241-257
Number of pages17
JournalIEEE transactions on software engineering
Volume35
Issue number2
DOIs
Publication statusPublished - 2009

Keywords

  • FMT-PM: PROBABILISTIC METHODS
  • FMT-MC: MODEL CHECKING
  • IR-68146
  • METIS-264046
  • EWI-16105

Cite this

@article{c064337c1a08421cbbb018c15850ed16,
title = "Counterexample Generation in Probabilistic Model Checking",
abstract = "Providing evidence for the refutation of a property is an essential, if not the most important, feature of model checking. This paper considers algorithms for counterexample generation for probabilistic CTL formulae in discrete-time Markov chains. Finding the strongest evidence (i.e., the most probable path) violating a (bounded) until-formula is shown to be reducible to a single-source (hop-constrained) shortest path problem. Counterexamples of smallest size that deviate most from the required probability bound can be obtained by applying (small amendments to) k-shortest (hop-constrained) paths algorithms. These results can be extended to Markov chains with rewards, to LTL model checking, and are useful for Markov decision processes. Experimental results show that typically the size of a counterexample is excessive. To obtain much more compact representations, we present a simple algorithm to generate (minimal) regular expressions that can act as counterexamples. The feasibility of our approach is illustrated by means of two communication protocols: leader election in an anonymous ring network and the Crowds protocol.",
keywords = "FMT-PM: PROBABILISTIC METHODS, FMT-MC: MODEL CHECKING, IR-68146, METIS-264046, EWI-16105",
author = "Tingting Han and Katoen, {Joost P.} and B. Damman",
note = "10.1109/TSE.2009.5",
year = "2009",
doi = "10.1109/TSE.2009.5",
language = "Undefined",
volume = "35",
pages = "241--257",
journal = "IEEE transactions on software engineering",
issn = "0098-5589",
publisher = "IEEE",
number = "2",

}

Counterexample Generation in Probabilistic Model Checking. / Han, Tingting; Katoen, Joost P.; Damman, B.

In: IEEE transactions on software engineering, Vol. 35, No. 2, 10.1109/TSE.2009.5, 2009, p. 241-257.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - Counterexample Generation in Probabilistic Model Checking

AU - Han, Tingting

AU - Katoen, Joost P.

AU - Damman, B.

N1 - 10.1109/TSE.2009.5

PY - 2009

Y1 - 2009

N2 - Providing evidence for the refutation of a property is an essential, if not the most important, feature of model checking. This paper considers algorithms for counterexample generation for probabilistic CTL formulae in discrete-time Markov chains. Finding the strongest evidence (i.e., the most probable path) violating a (bounded) until-formula is shown to be reducible to a single-source (hop-constrained) shortest path problem. Counterexamples of smallest size that deviate most from the required probability bound can be obtained by applying (small amendments to) k-shortest (hop-constrained) paths algorithms. These results can be extended to Markov chains with rewards, to LTL model checking, and are useful for Markov decision processes. Experimental results show that typically the size of a counterexample is excessive. To obtain much more compact representations, we present a simple algorithm to generate (minimal) regular expressions that can act as counterexamples. The feasibility of our approach is illustrated by means of two communication protocols: leader election in an anonymous ring network and the Crowds protocol.

AB - Providing evidence for the refutation of a property is an essential, if not the most important, feature of model checking. This paper considers algorithms for counterexample generation for probabilistic CTL formulae in discrete-time Markov chains. Finding the strongest evidence (i.e., the most probable path) violating a (bounded) until-formula is shown to be reducible to a single-source (hop-constrained) shortest path problem. Counterexamples of smallest size that deviate most from the required probability bound can be obtained by applying (small amendments to) k-shortest (hop-constrained) paths algorithms. These results can be extended to Markov chains with rewards, to LTL model checking, and are useful for Markov decision processes. Experimental results show that typically the size of a counterexample is excessive. To obtain much more compact representations, we present a simple algorithm to generate (minimal) regular expressions that can act as counterexamples. The feasibility of our approach is illustrated by means of two communication protocols: leader election in an anonymous ring network and the Crowds protocol.

KW - FMT-PM: PROBABILISTIC METHODS

KW - FMT-MC: MODEL CHECKING

KW - IR-68146

KW - METIS-264046

KW - EWI-16105

U2 - 10.1109/TSE.2009.5

DO - 10.1109/TSE.2009.5

M3 - Article

VL - 35

SP - 241

EP - 257

JO - IEEE transactions on software engineering

JF - IEEE transactions on software engineering

SN - 0098-5589

IS - 2

M1 - 10.1109/TSE.2009.5

ER -