An algebraic theory of multiple clocks

Abstract

This paper develops a temporal process algebra, CSA, for reasoning about distributed systems that involve qualitative timing constraints. It is a conservative extension of Milner's CCS that combines the idea of multiple clocks from the algebra PMC with the assumption of maximal progress familiar from timed process algebras such as TPL. Using a typical class of examples drawn from hardware design, we motivate why these features are useful and in some cases necessary for modeling and verifying distributed systems. We also present fully-abstract behavioral congruences based on the notion of strong bisimulation and observational equivalence, respectively. For temporal strong bisimulation we give sound and complete axiomatizations for several classes of processes.