Probabilistic Semantics for RoboChart A Weakest Completion Approach

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

Full text download(s)



Publication details

Title of host publicationUnifying Theories of Programming
DateAccepted/In press - 22 Aug 2019
DatePublished (current) - 4 Nov 2019
PublisherLecture Notes in Computer Science
EditorsPedro Ribeiro, Augusto Sampaio
Original languageEnglish
ISBN (Electronic)978-3-030-31038-7
ISBN (Print)978-3-030-31037-0


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.

    Research areas

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


Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations