Automated Reasoning for Probabilistic Sequential Programs with Theorem Proving

Kangfeng Ye*, Simon Foster, Jim Woodcock

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Semantics for nondeterministic probabilistic sequential pro- grams has been well studied in the past decades. In a variety of semantic models, how nondeterministic choice interacts with probabilistic choice is the most significant difference. In He, Morgan, and McIver’s relational model, probabilistic choice refines nondeterministic choice. This model is general because of its predicative-style semantics in Hoare and He’s Unifying Theories of Programming, and suitable for automated reasoning because of its algebraic feature. Previously, we gave probabilistic semantics to the RoboChart notation based on this model, and also formalised the proof that the semantic embedding is a homomorphism, and revealed interesting details. In this paper, we present our mechanisation of the proof in Isabelle/UTP enabling automated reasoning for probabilistic sequential programs including a subset of the RoboChart language. With mechanisation, we even reveal more interesting questions, hidden in the original model. We demonstrate several examples, including an ex- ample to illustrate the interaction between nondeterministic choice and probabilistic choice, and a RoboChart model for randomisation based on binary probabilistic choice.
Original languageEnglish
Title of host publicationRelational and Algebraic Methods in Computer Science - 19th International Conference, RAMiCS 2021, Proceedings
EditorsUli Fahrenberg, Mai Gehrke, Luigi Santocanale, Michael Winter
Number of pages18
ISBN (Print)9783030887001
Publication statusPublished - 22 Oct 2021
Event19th International Conference on Relational and Algebraic Methods in Computer Science, RAMiCS 2021 - Marseille, France
Duration: 2 Nov 20215 Nov 2021

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume13027 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference19th International Conference on Relational and Algebraic Methods in Computer Science, RAMiCS 2021

Bibliographical note

Funding Information:
This work is funded by the EPSRC projects RoboCalc (Grant EP/M025756/1), RoboTest (Grant EP/R025479/1), and CyPhyAssure (CyPhyAssure Project: (Grant EP/S001190/1). The icons used in RoboChart have been made by Sarfraz Shoukat, Freepik, Google, Icomoon and Madebyoliver from, and are licensed under CC 3.0 BY.

Publisher Copyright:
© 2021, Springer Nature Switzerland AG.


  • probabilistic programs
  • relational semantics
  • formal verification
  • theorem proving
  • modelling of uncertainty
  • Unifying Theories of Programming
  • RoboChart

Cite this