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

Joost-Pieter Katoen, Romanus 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

Process Algebra
Causality
Algebra
Event Structures
Interleaving
Semantics
Operational Semantics
Partial Order
Interaction
Fixpoint
Recursion
Immediately
Specification languages
Operator
Model

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

@article{4a3e35d488514e5d987370a349762dec,
title = "A consistent causality-based view on a timed process algebra including urgent interactions",
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.",
keywords = "FMT-PA: PROCESS ALGEBRAS, FMT-NIM: NON-INTERLEAVING MODELS, Process Algebra, Urgency, Semantics, LOTOS, Causality, True concurrency, Consistency of semantics, Time, event structure",
author = "Joost-Pieter Katoen and Romanus Langerak and Ed Brinksma and Diego Latella and Tommaso Bolognesi",
year = "1998",
doi = "10.1023/A:1008649927166",
language = "English",
volume = "12",
pages = "189--216",
journal = "Formal methods in system design",
issn = "0925-9856",
publisher = "Springer",
number = "2",

}

A consistent causality-based view on a timed process algebra including urgent interactions. / Katoen, Joost-Pieter; Langerak, Romanus; Brinksma, Ed; Latella, Diego; Bolognesi, Tommaso.

In: Formal methods in system design, Vol. 12, No. 2, 1998, p. 189-216.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

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

AU - Katoen, Joost-Pieter

AU - Langerak, Romanus

AU - Brinksma, Ed

AU - Latella, Diego

AU - Bolognesi, Tommaso

PY - 1998

Y1 - 1998

N2 - 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.

AB - 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.

KW - FMT-PA: PROCESS ALGEBRAS

KW - FMT-NIM: NON-INTERLEAVING MODELS

KW - Process Algebra

KW - Urgency

KW - Semantics

KW - LOTOS

KW - Causality

KW - True concurrency

KW - Consistency of semantics

KW - Time

KW - event structure

U2 - 10.1023/A:1008649927166

DO - 10.1023/A:1008649927166

M3 - Article

VL - 12

SP - 189

EP - 216

JO - Formal methods in system design

JF - Formal methods in system design

SN - 0925-9856

IS - 2

ER -