Metric semantics for true concurrent real time

Christel Baier, Joost P. Katoen, Diego Latella

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

    15 Citations (Scopus)

    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
    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
    CountryDenmark
    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