Prioritized slotted-Circus

peer-reviewedThis paper describes an extension adding priority to slotted-Circus, a generic framework for reasoning about discretely timed and/or synchronously clocked systems. The semantics of prioritised external choice is given using the Unifying Theories of Programming framework (UTP). The resulting language is similar to Prioritized Timed CSP, but its semantics is not based on trace ordering, and neither does it use the notion of acceptances (e.g. PCSP). Instead, the semantics is based on the notion of refusal sets already widely used in theories of CSP, Circus and slotted-Circus. We introduce priority as a lightweight extension of slotted-Circus, which can be easily adapted to define a similar extension of Timed CSP. We also discuss why priority can most easily be added to specific history models, and the fact that requiring the clock to tick after every communication event results in a more tractable theory. ICTAC'10 Proceedings of the 7th International colloquium conference on Theoretical aspects of computing Pages 91-105 DOI