By the same authors

From the same journal

From the same journal

Angelic Processes for CSP via the UTP

Research output: Contribution to journalArticlepeer-review



Publication details

JournalTheoretical Computer Science
DateAccepted/In press - 8 Oct 2018
DateE-pub ahead of print (current) - 15 Oct 2018
Number of pages51
Early online date15/10/18
Original languageEnglish


Demonic and angelic nondeterminism play fundamental roles as abstraction mechanisms for formal modelling. In contrast with its demonic counterpart, in an angelic choice failure is avoided whenever possible. Although it has been extensively studied in refinement calculi, in the context of process algebras, and of the Communicating Sequential Processes (CSP) algebra for refinement, in particular, it has been elusive. We show here that a semantics for an extended version of CSP that includes both demonic and angelic choice can be provided using Hoare and He's Unifying Theories of Programming (UTP). Since CSP is given semantics in the UTP via reactive designs (pre and postcondition pairs) we have developed a theory of angelic designs and a conservative extension of the CSP theory using reactive angelic designs. To characterise angelic nondeterminism appropriately in an algebra of processes, however, a notion of divergence that can undo the history of events needs to be considered. Taking this view, we present a model for CSP where angelic choice completely avoids divergence just like in the refinement calculi for sequential programs.

Bibliographical note

This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy.

Discover related content

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

View graph of relations