Timed Processes: Models, Axioms and Decidability

Abstract

This thesis presents and studies a timed computational model of parallelism, a Timed Calculus of Communicating Systems or Timed CCS for short. Timed CCS is an extension of Milner's CCS with time. We allow time to be discrete, such as the natural numbers, or dense, such as the non-negative rationals or the non-negative reals. We make no assumption of the Maximal Progress Principle, but the calculus is consistent with the principle. Time variables in the language allow us to express a notion of time dependency and the language is more expressive than those without time variables or infinite summation. We extend the well known notion of bisimulation to timed processes and study the abstract sensation of timed processes. We show that strong equivalence (the largest strong bisimulation) is decidable for finite processes, i.e. processes without recursion. The decidability is independent of the choice of time domain. We also present a simple proof system for strong equivalence and the proof system is again independent of the choice of time domain. We show that the proof system is sound and complete for finite processes over dense time domains, but only complete for a restricted language over discrete time domains. We discuss how to modify the definition of time expressions to get the restricted language. We also study behavioural abstraction in timed processes.

The thesis also presents and studies a general model, Timed Synchronisation Trees, for timed calculi. Timed synchronisation trees are extensions of synchronisation trees with time. All constructions on timed synchronisation trees are continuous with respect to a natural complete partial order. We can interpret a wide range of real-time process algebras in timed synchronisation trees. As an example, we give a denotational semantics for Timed CCS based on timed synchronisation trees. We show that the denotational and operational semantics of Timed CCS coincide.

CCS is a symbolic calculus in the sense that it treats solely the observation of events of a system. The relative time, location and duration of events are abstracted away from the consideration. If we postulate that every action has a non-zero constant duration, we can observe the usual notions of causality, concurrency and conflict relations of events of a system. By interpreting CCS in Timed CCS based on a postulation that for any two events which are causally related there is at least a non-zero constant delay between them, we get a timed semantics for CCS. The timed semantics of CCS is a partial order or true concurrency semantics. As a consequence, we develop a partial order or true concurrency semantics based on an interleaving approach.