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 of the metric 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 classes of timed event structures in which we abstract from event identities and non-executable events (events that can never occur) is shown to be a complete ultra-metric space. We present an operational semantics for the considered language and show that the metric semantics is an abstraction of it. The operational semantics is characterised by the absence of synchronisation on the advance of time as opposed to the operational semantics of most real-time calculi. The consistency between our metric and an existing cpo-based denotational semantics is briefly investigated.

Metric semantics for true concurrent real time (Ext. Abs.)

LATELLA D
1998

Abstract

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 of the metric 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 classes of timed event structures in which we abstract from event identities and non-executable events (events that can never occur) is shown to be a complete ultra-metric space. We present an operational semantics for the considered language and show that the metric semantics is an abstraction of it. The operational semantics is characterised by the absence of synchronisation on the advance of time as opposed to the operational semantics of most real-time calculi. The consistency between our metric and an existing cpo-based denotational semantics is briefly investigated.
1998
Istituto di Scienza e Tecnologie dell'Informazione "Alessandro Faedo" - ISTI
3-540-64781-3
Consistency of semantics
Denotational semantics (bundle)
Event structure Interleaving
Metric space
Process algebra
Real time
Semantics
True concurrency
File in questo prodotto:
File Dimensione Formato  
prod_190725-doc_122395.pdf

solo utenti autorizzati

Descrizione: Metric semantics for true concurrent real time
Tipologia: Versione Editoriale (PDF)
Dimensione 193.87 kB
Formato Adobe PDF
193.87 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/20.500.14243/234582
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? 7
social impact