DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2024.36

Branching Bisimilarity for Processes with Time-Outs

Authors: Gaspard Reghem and Rob J. van Glabbeek

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract

This paper provides an adaptation of branching bisimilarity to reactive systems with time-outs. 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.

Cite as

Gaspard Reghem and Rob J. van Glabbeek. Branching Bisimilarity for Processes with Time-Outs. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 36:1-36:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{reghem_et_al:LIPIcs.CONCUR.2024.36,
  author =	{Reghem, Gaspard and van Glabbeek, Rob J.},
  title =	{{Branching Bisimilarity for Processes with Time-Outs}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{36:1--36:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.36},
  URN =		{urn:nbn:de:0030-drops-208082},
  doi =		{10.4230/LIPIcs.CONCUR.2024.36},
  annote =	{Keywords: Reactive Systems, Time-outs, Branching Bisimilarity, Modal Characterisation, Congruence, Axiomatisation}
}

Document

DOI: 10.4230/LIPIcs.CSL.2017.25

Precongruence Formats with Lookahead through Modal Decomposition

Authors: Wan Fokkink and Rob J. van Glabbeek

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

Abstract

Bloom, Fokkink & van Glabbeek (2004) presented a method to decompose formulas from Hennessy-Milner logic with regard to a structural operational semantics specification. A term in the corresponding process algebra satisfies a Hennessy-Milner formula if and only if its subterms satisfy certain formulas, obtained by decomposing the original formula. They used this decomposition method to derive congruence formats in the realm of structural operational semantics. In this paper it is shown how this framework can be extended to specifications that include bounded lookahead in their premises. This extension is used in the derivation of a congruence format for the partial trace preorder.

Cite as

Wan Fokkink and Rob J. van Glabbeek. Precongruence Formats with Lookahead through Modal Decomposition. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 25:1-25:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{fokkink_et_al:LIPIcs.CSL.2017.25,
  author =	{Fokkink, Wan and van Glabbeek, Rob J.},
  title =	{{Precongruence Formats with Lookahead through Modal Decomposition}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{25:1--25:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.25},
  URN =		{urn:nbn:de:0030-drops-76776},
  doi =		{10.4230/LIPIcs.CSL.2017.25},
  annote =	{Keywords: Structural Operational Semantics, Compositionality, Congruence, Modal Logic, Modal Decomposition, Lookahead}
}

Search Results

Documents authored by van Glabbeek, Rob J.

Branching Bisimilarity for Processes with Time-Outs

Abstract

Cite as

Precongruence Formats with Lookahead through Modal Decomposition

Abstract

Cite as

Thanks for your feedback!

Could not send message