Angelic Processes for CSP via the UTP

Pedro Fernando De Oliveira Salazar Ribeiro; Ana Lucia Caneca Cavalcanti

doi:10.1016/j.tcs.2018.10.008

Angelic Processes for CSP via the UTP

Pedro Fernando De Oliveira Salazar Ribeiro, Ana Lucia Caneca Cavalcanti

Computer Science

Research output: Contribution to journal › Article › peer-review

Abstract

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.

Original language	English
Number of pages	51
Journal	Theoretical Computer Science
Early online date	15 Oct 2018
DOIs	https://doi.org/10.1016/j.tcs.2018.10.008
Publication status	E-pub ahead of print - 15 Oct 2018

Bibliographical note

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

Access to Document

10.1016/j.tcs.2018.10.008

Angelic Processes for CSP via the UTP
This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy.
Accepted author manuscript, 1.22 MBLicence: CC BY-NC-ND

https://www-users.cs.york.ac.uk/~pfr/publications/TCS2018.pdfLicence: CC BY-NC-ND

Cite this

@article{a62e086a305243f49214cff70997eb30,

title = "Angelic Processes for CSP via the UTP",

abstract = "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.",

author = "{De Oliveira Salazar Ribeiro}, {Pedro Fernando} and Cavalcanti, {Ana Lucia Caneca}",

note = "This is an author-produced version of the published paper. Uploaded in accordance with the publisher{\textquoteright}s self-archiving policy. ",

year = "2018",

month = oct,

day = "15",

doi = "10.1016/j.tcs.2018.10.008",

language = "English",

journal = "Theoretical Computer Science",

issn = "0304-3975",

publisher = "Elsevier",

}

TY - JOUR

T1 - Angelic Processes for CSP via the UTP

AU - De Oliveira Salazar Ribeiro, Pedro Fernando

AU - Cavalcanti, Ana Lucia Caneca

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

PY - 2018/10/15

Y1 - 2018/10/15

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

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

U2 - 10.1016/j.tcs.2018.10.008

DO - 10.1016/j.tcs.2018.10.008

M3 - Article

SN - 0304-3975

JO - Theoretical Computer Science

JF - Theoretical Computer Science

ER -