A consistent causality-based view on a timed process algebra including urgent interactions

Joost-Pieter Katoen, Rom Langerak, Ed Brinksma, Diego Latella, Tommaso Bolognesi

    Research output: Contribution to journalArticleAcademicpeer-review

    14 Citations (Scopus)

    Abstract

    This paper discusses a timed variant of a process algebra akin to LOTOS, baptized UPA, in a causality-based setting. Two timed features are incorporated—a delay function which constrains the occurrence time of atomic actions and an urgency operator that forces (local or synchronized) actions to happen urgently. Timeouts are typical urgent phenomena. A novel timed extension of event structures is introduced and used as a vehicle to provide a denotational causality-based semantics for UPA. Recursion is dealt with by using standard fixpoint theory. In addition, an operational semantics is presented based on separate time- and action-transitions that is shown to be consistent with the event structure semantics. An interleaving semantics for UPA is immediately obtained from the operational semantics. By adopting this dual approach the well-developed timed interleaving view is extended with a consistent timed partial order view and a comparison is facilitated of the partial order model and the variety of existing (interleaved) timed process algebras.
    Original languageEnglish
    Pages (from-to)189-216
    Number of pages28
    JournalFormal methods in system design
    Volume12
    Issue number2
    DOIs
    Publication statusPublished - 1998

      Fingerprint

    Keywords

    • FMT-PA: PROCESS ALGEBRAS
    • FMT-NIM: NON-INTERLEAVING MODELS
    • Process Algebra
    • Urgency
    • Semantics
    • LOTOS
    • Causality
    • True concurrency
    • Consistency of semantics
    • Time
    • Event structure

    Cite this