Metric semantics for true concurrent real time

Citation
Jp. Katoen et al., Metric semantics for true concurrent real time, THEOR COMP, 254(1-2), 2001, pp. 501-542
Citations number
41
Categorie Soggetti
Computer Science & Engineering
Journal title
THEORETICAL COMPUTER SCIENCE
ISSN journal
03043975 → ACNP
Volume
254
Issue
1-2
Year of publication
2001
Pages
501 - 542
Database
ISI
SICI code
0304-3975(20010306)254:1-2<501:MSFTCR>2.0.ZU;2-Y
Abstract
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.