Generating counterexamples for quantitative safety specifications in probabilistic B

Ukachukwu Ndukwu

Research output: Contribution to journalArticlepeer-review

Abstract

Probabilistic annotations generalise standard Hoare Logic [20] to quantitative properties of probabilistic programs. They can be used to express critical expected values over program variables that must be maintained during program execution. As for standard program development, probabilistic assertions can be checked mechanically relative to an appropriate program semantics. In the case that a mechanical prover is unable to complete such validity checks then a counterexample to show that the annotation is incorrect can provide useful diagnostic information. In this paper, we provide a definition of counterexamples as failure traces for probabilistic assertions within the context of the pB language [19], an extension of the standard B method [1] to cope with probabilistic programs. In addition, we propose algorithmic techniques to find counterexamples where they exist, and suggest a ranking mechanism to return 'the most useful diagnostic information' to the pB developer to aid the resolution of the problem.
Original languageEnglish
Pages (from-to)26-45
Number of pages20
JournalJournal of Logic and Algebraic Programming
Volume81
Issue number1
DOIs
Publication statusPublished - 2012

Keywords

  • Counterexamples
  • Expectations
  • Failures
  • Probabilistic B
  • Quantitative safety

Fingerprint Dive into the research topics of 'Generating counterexamples for quantitative safety specifications in probabilistic B'. Together they form a unique fingerprint.

Cite this