Metric Semantics for True Concurrent Real Time

This paper investigates the use of a complete metric space framework for providing denotational semantics to a real-time process algebra. The study is carried out in a non-interleaving setting and is based on a timed extension of Langerak's bundle event structures, a variant of Winskel's event structures. The distance function is based on the amount of time to 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 structures. A generalisation to equivalence of timed event structures in which we abstract from event names and non-executable events (events that can never appear) is shown to be a complete ultra-metric space. We show that the resulting metric s is an abstraction of an existing cpo-based denotational and a related operational semantics for the considered language.

• Type: Conference
• Year: 1998
• Where: ICALP
• Authors: Christel Baier, Joost-Pieter Katoen, Diego Latella
• Keywords: Event Structures, ICALP 1998, Programming Languages, Timed Event Structures, Winskel's Event Structures