Probabilistic Semantics for RoboChart A Weakest Completion Approach

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


We outline a probabilistic denotational semantics for the RoboChart language, a diagrammatic, domain-specific notation for de- scribing robotic controllers with their hardware platforms and operating environments. We do this using a powerful (but perhaps not so well known) semantic technique: He, Morgan, and McIver’s weakest completion semantics, which is based on Hoare and He’s Unifying Theories of Programming. In this approach, we do the following: (1) start with the standard semantics for a nondeterministic programming language; (2) propose a new probabilistic semantic domain; (3) propose a forgetful function from the probabilistic semantic domain to the standard semantic domain; (4) use the converse of the forgetful function to embed the standard semantic domain in the probabilistic semantic domain; (5) demonstrate that this embedding preserves program structure; (6) define the probabilistic choice operator. Weakest completion semantics guides the semantic definition of new languages by building on existing semantics and, in this case, tackling a notoriously thorny issue: the relationship between demonic and probabilistic choice. Consistency ensures that programming intuitions, development techniques, and proof methods can be carried over from the standard language to the probabilistic one. We largely follow He et al., our contribution being an explication of the technique with meticulous proofs suitable for mechanisation in Isabelle/UTP.
Original languageEnglish
Title of host publicationUnifying Theories of Programming
Subtitle of host publication7th International Symposium, UTP 2019, Dedicated to Tony Hoare on the Occasion of His 85th Birthday, Porto, Portugal, October 8, 2019, Proceedings
EditorsPedro Ribeiro, Augusto Sampaio
ISBN (Electronic)978-3-030-31038-7
ISBN (Print)978-3-030-31037-0
Publication statusPublished - 4 Nov 2019

Publication series

NameLecture Notes in Computer Science


  • RoboChart language
  • Robotic controllers
  • Statecharts
  • Probabilistic semantics
  • Relational calculus
  • Unifying Theories of Programming (UTP)
  • Weakest completion semantics

Cite this