Towards Algebraic Semantics of Circus Time

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


Over the years, the Circus family of notation has been used for specification, programming, and verification by refinement in many applications. Circus Time, a timed variant of Circus, plays a key role in dealing with timed behaviours. While most of the semantic developments of Circus Time have tended to focus on the denotational and operational sides, the work on its algebraic semantics is frustrated by the fact that the parallel operators are difficult to be reduced to other primitives in both discrete-time and continuous-time CSP models. In this paper, we present an algebraic operational semantics (AOS) of the discrete-time CSP in Circus Time. The related AOS form is identified in the timed context, and a complete set of algebraic laws are provided to transform any finite Circus Time programs into the AOS form. The AOS provides a solution to sequentialise the parallel operators and is also the major step towards a fully algebraic semantics.
Original languageEnglish
Title of host publicationUnifying Theories of Programming - 5th International Symposium, UTP 2014, Singapore, May 13, 2014, Revised Selected Papers
EditorsDavid Naumann
Number of pages21
Publication statusPublished - 2015

Publication series

NameLecture Notes in Computer Science

Bibliographical note

Self-archiving of publisher's PDF not supported by the publisher.

Cite this