Automated Reasoning for Probabilistic Sequential Programs with Theorem Proving

TY - GEN

T1 - Automated Reasoning for Probabilistic Sequential Programs with Theorem Proving

AU - Ye, Kangfeng

AU - Foster, Simon

AU - Woodcock, Jim

N1 - 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.

PY - 2021/10/22

Y1 - 2021/10/22

N2 - 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.

AB - 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.

KW - probabilistic programs

KW - relational semantics

KW - formal verification

KW - theorem proving

KW - modelling of uncertainty

KW - Unifying Theories of Programming

KW - RoboChart

U2 - 10.1007/978-3-030-88701-8_28

DO - 10.1007/978-3-030-88701-8_28

M3 - Conference contribution

AN - SCOPUS:85118936769

SN - 9783030887001

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 465

EP - 482

BT - Relational and Algebraic Methods in Computer Science - 19th International Conference, RAMiCS 2021, Proceedings

A2 - Fahrenberg, Uli

A2 - Gehrke, Mai

A2 - Santocanale, Luigi

A2 - Winter, Michael

PB - Springer

T2 - 19th International Conference on Relational and Algebraic Methods in Computer Science, RAMiCS 2021

Y2 - 2 November 2021 through 5 November 2021

ER -