A Unary Semigroup Trace Algebra

Pedro Fernando De Oliveira Salazar Ribeiro

A Unary Semigroup Trace Algebra

Pedro Fernando De Oliveira Salazar Ribeiro

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

The Unifying Theories of Programming (UTP) of Hoare and He promote the unification of semantics catering for different concerns, such as, termination, data modelling, concurrency and time. Process calculi like Circus and CSP can be given semantics in the UTP using reactive designs whose traces can be abstractly specified using a monoid trace algebra. The prefix order over traces is defined in terms of the monoid operator. This order, however, is inadequate to characterise a broader family of timed process algebras whose traces are preordered instead. To accommodate these, we propose a unary semigroup trace algebra that is weaker than the monoid algebra. This structure satisfies some of the axioms of restriction semigroups and is a right P-Ehresmann semigroup. Reactive designs specified using it satisfy core laws that have been mechanised so far in Isabelle/UTP. More importantly, our results improve the support for unifying trace models in the UTP.

Original language	English
Title of host publication	18th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 2020)
Publisher	Springer
Number of pages	16
Publication status	Accepted/In press - 16 Dec 2019
Event	18th International Conference on Relational and Algebraic Methods in Computer Science - École polytechnique, Paris, France Duration: 8 Apr 2020 → 11 Apr 2020 Conference number: 2020 http://ramics18.gforge.inria.fr/

Publication series

Name	Lecture Notes in Computer Science

Conference

Conference	18th International Conference on Relational and Algebraic Methods in Computer Science
Abbreviated title	RAMiCS
Country/Territory	France
City	Paris
Period	8/04/20 → 11/04/20
Internet address	http://ramics18.gforge.inria.fr/

Bibliographical note

This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy. Further copying may not be permitted; contact the publisher for details.

Keywords

Semantics
Process algebra
Semigroups
UTP

Access to Document

RAMiCS2020
This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy. Further copying may not be permitted; contact the publisher for details.
Accepted author manuscript, 293 KB

1 Finished

A Calculus for Software Engineering of Mobile and Autonomous Robots
Cavalcanti, A. L. C. (Principal investigator), Timmis, J. (Co-investigator), Woodcock, J. (Co-investigator), Foster, S. D. (Researcher), Li, W. (Researcher), Miyazawa, A. (Researcher) & Ribeiro, P. (Researcher)
EPSRC
1/09/15 → 30/06/21
Project: Research project (funded) › Research

Cite this

@inproceedings{b239a72044b149bdb2553914aaf60426,

title = "A Unary Semigroup Trace Algebra",

abstract = "The Unifying Theories of Programming (UTP) of Hoare and He promote the unification of semantics catering for different concerns, such as, termination, data modelling, concurrency and time. Process calculi like Circus and CSP can be given semantics in the UTP using reactive designs whose traces can be abstractly specified using a monoid trace algebra. The prefix order over traces is defined in terms of the monoid operator. This order, however, is inadequate to characterise a broader family of timed process algebras whose traces are preordered instead. To accommodate these, we propose a unary semigroup trace algebra that is weaker than the monoid algebra. This structure satisfies some of the axioms of restriction semigroups and is a right P-Ehresmann semigroup. Reactive designs specified using it satisfy core laws that have been mechanised so far in Isabelle/UTP. More importantly, our results improve the support for unifying trace models in the UTP.",

keywords = "Semantics, Process algebra, Semigroups, UTP",

author = "{De Oliveira Salazar Ribeiro}, {Pedro Fernando}",

note = "This is an author-produced version of the published paper. Uploaded in accordance with the publisher{\textquoteright}s self-archiving policy. Further copying may not be permitted; contact the publisher for details. ; 18th International Conference on Relational and Algebraic Methods in Computer Science, RAMiCS ; Conference date: 08-04-2020 Through 11-04-2020",

year = "2019",

month = dec,

day = "16",

language = "English",

series = " Lecture Notes in Computer Science",

publisher = "Springer",

booktitle = "18th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 2020)",

address = "Germany",

url = "http://ramics18.gforge.inria.fr/",

}

TY - GEN

T1 - A Unary Semigroup Trace Algebra

AU - De Oliveira Salazar Ribeiro, Pedro Fernando

N1 - Conference code: 2020

PY - 2019/12/16

Y1 - 2019/12/16

N2 - The Unifying Theories of Programming (UTP) of Hoare and He promote the unification of semantics catering for different concerns, such as, termination, data modelling, concurrency and time. Process calculi like Circus and CSP can be given semantics in the UTP using reactive designs whose traces can be abstractly specified using a monoid trace algebra. The prefix order over traces is defined in terms of the monoid operator. This order, however, is inadequate to characterise a broader family of timed process algebras whose traces are preordered instead. To accommodate these, we propose a unary semigroup trace algebra that is weaker than the monoid algebra. This structure satisfies some of the axioms of restriction semigroups and is a right P-Ehresmann semigroup. Reactive designs specified using it satisfy core laws that have been mechanised so far in Isabelle/UTP. More importantly, our results improve the support for unifying trace models in the UTP.

AB - The Unifying Theories of Programming (UTP) of Hoare and He promote the unification of semantics catering for different concerns, such as, termination, data modelling, concurrency and time. Process calculi like Circus and CSP can be given semantics in the UTP using reactive designs whose traces can be abstractly specified using a monoid trace algebra. The prefix order over traces is defined in terms of the monoid operator. This order, however, is inadequate to characterise a broader family of timed process algebras whose traces are preordered instead. To accommodate these, we propose a unary semigroup trace algebra that is weaker than the monoid algebra. This structure satisfies some of the axioms of restriction semigroups and is a right P-Ehresmann semigroup. Reactive designs specified using it satisfy core laws that have been mechanised so far in Isabelle/UTP. More importantly, our results improve the support for unifying trace models in the UTP.

KW - Semantics

KW - Process algebra

KW - Semigroups

KW - UTP

M3 - Conference contribution

T3 - Lecture Notes in Computer Science

BT - 18th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 2020)

PB - Springer

T2 - 18th International Conference on Relational and Algebraic Methods in Computer Science

Y2 - 8 April 2020 through 11 April 2020

ER -

A Unary Semigroup Trace Algebra

Abstract

Publication series

Conference

Bibliographical note

Keywords

Access to Document

Projects

A Calculus for Software Engineering of Mobile and Autonomous Robots

Cite this