Successful Termination in Timed CSP

Abstract. In previous work the authors investigated the inconsistencies of how suc-cessful termination was modelled in Hoare, Brookes and Roscoe’s original CSP. This led to the definition of a variant of CSP, called CSPT. CSPT presents a solution to these problems by means of adding a termination axiom to the original process ax-ioms. 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 un-timed CSP. We discuss the issues that need to be considered when selecting termina-tion axioms for Timed CSP, based on our experiences in defining CSPT. 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 CSPT