Towards Algebraic Semantics of Circus Time

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.