Probabilistic invariants for probabilistic machines

Thai Son Hoang, Zhendong Jin, Ken Robinson, Annabelle McIver, Carroll Morgan

Research output: Contribution to journalArticlepeer-review

14 Citations (Scopus)


Abrial's Generalised Substitution Language (GSL) [4] can be modified to operate on arithmetic expressions, rather than Boolean predicates, which allows it to be applied to probabilistic programs [13]. We add a new operator p⊕ to GSL, for probabilistic choice, and we get the probabilistic Generalised Substitution Language (pGSL): a smooth extension of GSL that includes random algorithms within its scope. In this paper we begin to examine the effect of pGSL on B's larger-scale structures: its machines. In particular, we suggest a notion of probabilistic machine invariant. We show how these invariants interact with pGSL, at a fine-grained level; and at the other extreme we investigate how they affect our general understanding "in the large" of probabilistic machines and their behaviour. Overall, we aim to initiate the development of probabilistic B (pB), complete with a suitable probabilistic AMN (pAMN). We discuss the practical extension of the B-Toolkit [5] to support pB, and we give examples to show how pAMN can be used to express and reason about probabilistic properties of a system.

Original languageEnglish
Pages (from-to)240-259
Number of pages20
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Publication statusPublished - 2003


  • Generalised substitutions
  • Probabilistic algorithms
  • Probability
  • Program correctness
  • The B Method (B)
  • Weakest preconditions

Fingerprint Dive into the research topics of 'Probabilistic invariants for probabilistic machines'. Together they form a unique fingerprint.

Cite this