Successful Termination in Timed CSP

In previous work the authors investigated the inconsistencies of how successful termination was modelled in Hoare, Brookes and Roscoe’s original CSP. This led to the definition of a variant of CSP, called CSP_T . CSP_T presents a solution to these problems by means of adding a termination axiom to the original process axioms. In this paper we investigate how successful process termination is modelled in Reed and Roscoe’s Timed CSP, which is the temporal version of Hoare’s original untimed CSP. We discuss the issues that need to be considered when selecting termination axioms for Timed CSP, based on our experiences in defining CSP_T . The outcome of this investigation and discussion is a collection of candidate successful termination axioms that could be added to the existing Timed CSP models, leading to an improved treatment of successful termination within the Timed CSP framework. We outline how these termination axioms would be added to the family of semantic models for Timed CSP. Finally, we outline what further work needs to be done once these new models for Timed CSP have been defined. For example, it would then be possible to define timed versions of the new more flexible parallel operators introduced in CSP_T.