THE ALGEBRA OF TIMED PROCESSES, ATP - THEORY AND APPLICATION

The algebra of timed processes, ATP, uses a notion of discrete global time and suggests a conceptual framework for introducing time by exten ding untimed languages. The action vocabularly of ATP contains a speci al element representing the progress of time. The algebra has, apart f rom standard operators of process algebras such as prefixing by an act ion, alternative choice, and parallel composition, a primitive unit-de lay operator. For two arguments, processes P and e, this operator give s a process which behaves as P before the execution of a time event an d behaves as e afterwards. It is shown that several d-unit delay const ructs such as timeouts and watchdogs can be expressed in terms of the unit-delay operator and standard process algebra operators. A sound an d complete axiomatization for bisimulation semantics is studied and tw o examples illustrating the adequacy of the language for the descripti on of timed systems are given. Finally we provide a comparison with ex isting timed process algebras. (C) 1994 Academic Press, Inc.