Metric semantics for true concurrent real time

Christel Baier, Joost-Pieter Katoen, Diego Latella

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    15 Citations (Scopus)
    4 Downloads (Pure)

    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 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 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 semantics is an abstraction of an existing cpo-based denotational and a related operational semantics for the considered language.
    Original languageEnglish
    Title of host publicationAutomata, Languages and Programming
    Subtitle of host publication25th International Colloquium, ICALP'98 Aalborg, Denmark, July 13–17, 1998 Proceedings
    EditorsKim G. Larsen, Sven kyum, Glynn Winskel
    Place of PublicationBerlin, Heidelberg
    PublisherSpringer
    Pages568-580
    Number of pages13
    ISBN (Electronic)978-3-540-68681-1
    ISBN (Print)978-3-540-64781-2
    DOIs
    Publication statusPublished - 1998
    Event25th International Colloquium on Automata, Languages and Programming, ICALP 1998 - Aalborg, Denmark
    Duration: 13 Jul 199817 Jul 1998
    Conference number: 25

    Workshop

    Workshop25th International Colloquium on Automata, Languages and Programming, ICALP 1998
    Abbreviated titleICALP
    Country/TerritoryDenmark
    CityAalborg
    Period13/07/9817/07/98

    Keywords

    • FMT-NIM: NON-INTERLEAVING MODELS
    • FMT-PA: PROCESS ALGEBRAS
    • Event structure
    • Operational semantics
    • Parallel composition
    • Unique fixed point
    • Process algebra

    Fingerprint

    Dive into the research topics of 'Metric semantics for true concurrent real time'. Together they form a unique fingerprint.

    Cite this