Towards Algebraic Semantics of Circus Time

TY - GEN

T1 - Towards Algebraic Semantics of Circus Time

AU - Wei, Kun

AU - Woodcock, Jim

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

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-14806-9_5

DO - 10.1007/978-3-319-14806-9_5

M3 - Conference contribution

VL - 8963

T3 - Lecture Notes in Computer Science

SP - 84

EP - 104

BT - Unifying Theories of Programming - 5th International Symposium, UTP 2014, Singapore, May 13, 2014, Revised Selected Papers

A2 - Naumann, David

PB - Springer

ER -