Concrete branching bisimilarity for processes with time-outs

Gaspard Reghem; Rob J. van Glabbeek

doi:10.48550/arXiv.2412.19805

Concrete branching bisimilarity for processes with time-outs

Gaspard Reghem^*, Rob J. van Glabbeek^*

^*Corresponding author for this work

Research output: Book/Report › Commissioned report

Abstract

This paper provides an adaptation of branching bisimilarity to reactive systems with time-outs that does not enable eliding of time-out transitions. Multiple equivalent definitions are procured, along with a modal characterisation and a proof of its congruence property for a standard process algebra with recursion. The last section presents a complete axiomatisation for guarded processes without infinite sequences of unobservable actions.

Original language	English
Publisher	Schloss Dagstuhl - Leibniz-Zentrum für Informatik
Number of pages	53
DOIs	https://doi.org/10.48550/arXiv.2412.19805
Publication status	Published - 7 Oct 2024
Event	The 35th International Conference on Concurrency Theory - Best Western Plus Village Park Inn, Calgary, Canada Duration: 9 Sept 2024 → 13 Sept 2024 Conference number: 35 https://confest2024.github.io/

Publication series

Name	Computing Research Repository (CoRR)
Publisher	Schloss Dagstuhl - Leibniz-Zentrum für Informatik
ISSN (Electronic)	2331-8422

Keywords / Materials (for Non-textual outputs)

reactive systems
time-outs
branching bisimilarity
modal characterisation
congruence
axiomatisation

Access to Document

10.48550/arXiv.2412.19805Licence: Creative Commons: Attribution (CC-BY)

ReghemAndvanGlabbeekConcur2024ConcreteBranchingBisimilarityforProcesseswithTime-outsFinal published version, 1.11 MBLicence: Creative Commons: Attribution (CC-BY)

1 Active

Ensuring Liveness Properties of Distributed Systems with Justness
Bradfield, J. (Principal Investigator)
Other (Learned Society)
1/08/22 → 31/08/27
Project: Research

1 Conference contribution

Branching bisimilarity for processes with time-outs
Reghem, G. & van Glabbeek, R. J., 29 Aug 2024, 35th International Conference on Concurrency Theory (CONCUR 2024). Majumdar, R. & Silva, A. (eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Vol. 311. p. 1-22 22 p. (Leibniz International Proceedings in Informatics).
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Open Access
File

Cite this

@book{aef9865bf2ec42ccbb565541e15cde4c,

title = "Concrete branching bisimilarity for processes with time-outs",

abstract = "This paper provides an adaptation of branching bisimilarity to reactive systems with time-outs that does not enable eliding of time-out transitions. Multiple equivalent definitions are procured, along with a modal characterisation and a proof of its congruence property for a standard process algebra with recursion. The last section presents a complete axiomatisation for guarded processes without infinite sequences of unobservable actions.",

keywords = "reactive systems, time-outs, branching bisimilarity, modal characterisation, congruence, axiomatisation",

author = "Gaspard Reghem and {van Glabbeek}, {Rob J.}",

year = "2024",

month = oct,

day = "7",

doi = "10.48550/arXiv.2412.19805",

language = "English",

series = "Computing Research Repository (CoRR)",

publisher = "Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik",

note = "The 35th International Conference on Concurrency Theory, CONCUR 2024 ; Conference date: 09-09-2024 Through 13-09-2024",

url = "https://confest2024.github.io/",

}

TY - BOOK

T1 - Concrete branching bisimilarity for processes with time-outs

AU - Reghem, Gaspard

AU - van Glabbeek, Rob J.

N1 - Conference code: 35

PY - 2024/10/7

Y1 - 2024/10/7

N2 - This paper provides an adaptation of branching bisimilarity to reactive systems with time-outs that does not enable eliding of time-out transitions. Multiple equivalent definitions are procured, along with a modal characterisation and a proof of its congruence property for a standard process algebra with recursion. The last section presents a complete axiomatisation for guarded processes without infinite sequences of unobservable actions.

AB - This paper provides an adaptation of branching bisimilarity to reactive systems with time-outs that does not enable eliding of time-out transitions. Multiple equivalent definitions are procured, along with a modal characterisation and a proof of its congruence property for a standard process algebra with recursion. The last section presents a complete axiomatisation for guarded processes without infinite sequences of unobservable actions.

KW - reactive systems

KW - time-outs

KW - branching bisimilarity

KW - modal characterisation

KW - congruence

KW - axiomatisation

U2 - 10.48550/arXiv.2412.19805

DO - 10.48550/arXiv.2412.19805

M3 - Commissioned report

T3 - Computing Research Repository (CoRR)

BT - Concrete branching bisimilarity for processes with time-outs

PB - Schloss Dagstuhl - Leibniz-Zentrum für Informatik

T2 - The 35th International Conference on Concurrency Theory

Y2 - 9 September 2024 through 13 September 2024

ER -

Concrete branching bisimilarity for processes with time-outs

Abstract

Publication series

Keywords / Materials (for Non-textual outputs)

Access to Document

Fingerprint

Projects

Ensuring Liveness Properties of Distributed Systems with Justness

Research output

Branching bisimilarity for processes with time-outs

Cite this