Metric semantics for true concurrent real time

This paper investigates the use of a complete metric space framework for pr oviding denotational semantics to a real-time process algebra. The study is carried out in a non-interleaving setting and is based on a timed extensio n of Langerak's bundle event structures, a variant of Winskel's event struc tures. The distance function of the metric is based on the amount of time t o which event structures do 'agree'. We show that this intuitive notion of distance is a pseudo-metric (but not a metric) on the set of timed event st ructures. A generalisation to equivalence classes of timed event structures in which we abstract from event identities and non-executable events (even ts that can never occur) is shown to be a complete ultra-metric space. We p resent an operational semantics for the considered language and show that t he metric semantics is an abstraction of it, The operational semantics is c haracterised by the absence of synchronisation on the advance of time as op posed to the operational semantics of most real-time calculi. The consisten cy between our metric and an existing cpo-based denotational semantics is b riefly investigated. (C) 2001 Elsevier Science B.V. All rights reserved.