*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.

*LFCS report ECS-LFCS-93-271 (also published as
CST-101-93)*

This report is available in the following formats:

Previous | Index | Next