Projects per year
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.
|Title of host publication||18th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 2020)|
|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
|Name||Lecture Notes in Computer Science|
|Conference||18th International Conference on Relational and Algebraic Methods in Computer Science|
|Period||8/04/20 → 11/04/20|
Bibliographical noteThis 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.
- Process algebra