By the same authors

Automated Reasoning for Probabilistic Sequential Programs with Theorem Proving

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

Author(s)

Department/unit(s)

Publication details

Title of host publicationRelational and Algebraic Methods in Computer Science - 19th International Conference, RAMiCS 2021, Proceedings
DateSubmitted - 4 Jun 2021
DateAccepted/In press - 23 Jul 2021
DatePublished (current) - 22 Oct 2021
Pages465-482
Number of pages18
PublisherSpringer Science and Business Media Deutschland GmbH
EditorsUli Fahrenberg, Mai Gehrke, Luigi Santocanale, Michael Winter
Original languageEnglish
ISBN (Print)9783030887001

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

Abstract

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.

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: https://www.cs.york.ac.uk/circus/CyPhyAssure/) (Grant EP/S001190/1). The icons used in RoboChart have been made by Sarfraz Shoukat, Freepik, Google, Icomoon and Madebyoliver from www.flaticon.com, and are licensed under CC 3.0 BY.

Publisher Copyright:
© 2021, Springer Nature Switzerland AG.

    Research areas

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

Discover related content

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

View graph of relations