A Unary Semigroup Trace Algebra

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Full text download(s)



Publication details

Title of host publication18th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 2020)
DateAccepted/In press - 16 Dec 2019
Number of pages16
PublisherLecture Notes in Computer Science
Original languageEnglish


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.

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.

    Research areas

  • Semantics, Process algebra, Semigroups, UTP

Research outputs


Discover related content

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

View graph of relations