
TL;DR
This paper develops a formal semantics for angelic nondeterminism within CSP using the relational framework of UTP, enabling the modeling of angelic choices that avoid divergence in reactive systems.
Contribution
It introduces a theory of angelic designs and reactive angelic designs in UTP, providing a novel way to incorporate angelic nondeterminism into CSP semantics.
Findings
A relational model for angelic nondeterminism in CSP is developed.
The model characterizes processes that avoid divergence through angelic choice.
A theory of angelic designs suitable for reactive systems is established.
Abstract
In the formal modelling of systems, demonic and angelic nondeterminism play fundamental roles as abstraction mechanisms. The angelic nature of a choice pertains to the property of avoiding failure whenever possible. As a concept, angelic choice first appeared in automata theory and Turing machines, where it can be implemented via backtracking. It has traditionally been studied in the refinement calculus, and has proved to be useful in a variety of applications and refinement techniques. Recently it has been studied within relational, multirelational and higher-order models. It has been employed for modelling user interactions, game-like scenarios, theorem proving tactics, constraint satisfaction problems and control systems. When the formal modelling of state-rich reactive systems is considered, it only seems natural that both types of nondeterministic choice should be considered.…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Logic, programming, and type systems · Formal Methods in Verification
