Document Open Access Logo

Branching Bisimilarity for Processes with Time-Outs

Authors Gaspard Reghem, Rob J. van Glabbeek

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2024.36.pdf
  • Filesize: 0.84 MB
  • 22 pages

Document Identifiers

Author Details

Gaspard Reghem
  • ENS Paris-Saclay, Université Paris-Saclay, France
Rob J. van Glabbeek
  • School of Informatics, University of Edinburgh, UK
  • School of Computer Science and Engineering, University of New South Wales, Sydney, Australia

Funding

Supported by Royal Society Wolfson Fellowship RSWF\R1\221008.

Cite AsGet BibTex

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)
https://doi.org/10.4230/LIPIcs.CONCUR.2024.36

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
Keywords
  • Reactive Systems
  • Time-outs
  • Branching Bisimilarity
  • Modal Characterisation
  • Congruence
  • Axiomatisation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Jos C.M. Baeten and W. Peter Weijland. Process Algebra. Cambridge Tracts in Theoretical Computer Science 18. Cambridge University Press, 1990. URL: https://doi.org/10.1017/CBO9780511624193.
  2. Stephen D. Brookes, Tony (C.A.R.) Hoare, and Bill (A.W.) Roscoe. A theory of communicating sequential processes. Journal of the ACM, 31(3):560-599, 1984. URL: https://doi.org/10.1145/828.833.
  3. Olav Bunte, Jan Friso Groote, Jeroen J. A. Keiren, Maurice Laveaux, Thomas Neele, Erik P. de Vink, Wieger Wesselink, Anton Wijs, and Tim A. C. Willemse. The mCRL2 toolset for analysing concurrent systems - improvements in expressivity and usability. In Tomáš Vojnar and Lijun Zhang, editors, Proc. 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS'19, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS'19, Prague, Czech Republic, volume 11428 of LNCS, pages 21-39. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17465-1_2.
  4. Wan J. Fokkink. Introduction to Process Algebra. Texts in Theoretical Computer Science, An EATCS Series. Springer, 2000. URL: https://doi.org/10.1007/978-3-662-04293-9.
  5. Wan J. Fokkink, Rob J. van Glabbeek, and Bas Luttik. Divide and congruence III: From decomposition of modal formulas to preservation of stability and divergence. Information and Computation, 268:104435, 2019. URL: https://doi.org/10.1016/j.ic.2019.104435.
  6. Hubert Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe. CADP 2010: A toolbox for the construction and analysis of distributed processes. In Parosh Aziz Abdulla and K. Rustan M. Leino, editors, Proceedings Tools and Algorithms for the Construction and Analysis of Systems, TACAS '11, volume 6605 of LNCS, pages 372-387. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-19835-9_33.
  7. Rob J. van Glabbeek. The linear time - branching time spectrum II; the semantics of sequential systems with silent moves (extended abstract). In E. Best, editor, Proceedings CONCUR'93, 4^ th International Conference on Concurrency Theory, Hildesheim, Germany, August 1993, volume 715 of LNCS, pages 66-81. Springer, 1993. URL: https://doi.org/10.1007/3-540-57208-2_6.
  8. Rob J. van Glabbeek. Lean and full congruence formats for recursion. In Proceedings 32^nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'17, Reykjavik, Iceland, June 2017. IEEE Computer Society Press, 2017. URL: https://doi.org/10.1109/LICS.2017.8005142.
  9. Rob J. van Glabbeek. Failure trace semantics for a process algebra with time-outs. Logical Methods in Computer Science, 17(2), 2021. URL: https://doi.org/10.23638/LMCS-17(2:11)2021.
  10. Rob J. van Glabbeek. Modelling mutual exclusion in a process algebra with time-outs. Information and Computation, 294, 2023. URL: https://doi.org/10.1016/j.ic.2023.105079.
  11. Rob J. van Glabbeek. Reactive bisimulation semantics for a process algebra with timeouts. Acta Informatica, 60(1):11-57, 2023. URL: https://doi.org/10.1007/s00236-022-00417-1.
  12. Rob J. van Glabbeek and Peter Höfner. Progress, justness and fairness. ACM Computing Surveys, 52(4), August 2019. URL: https://doi.org/10.1145/3329125.
  13. Rob J. van Glabbeek and W. Peter Weijland. Branching time and abstraction in bisimulation semantics. Journal of the ACM, 43(3):555-600, 1996. URL: https://doi.org/10.1145/233551.233556.
  14. Clemens Grabmayer and Wan J. Fokkink. A complete proof system for 1-free regular expressions modulo bisimilarity. In H. Hermanns, L. Zhang, N. Kobayashi, and D. Miller, editors, Proc. 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'20, pages 465-478. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394744.
  15. Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137-161, 1985. URL: https://doi.org/10.1145/2455.2460.
  16. Xinxin Liu and Tingting Yu. Canonical solutions to recursive equations and completeness of equational axiomatisations. In I. Konnov and L. Kovacs, editors, Proceedings 31st International Conference on Concurrency Theory (CONCUR 2020), volume 171 of Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.35.
  17. Robin Milner. Operational and algebraic semantics of concurrent processes. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 19, pages 1201-1242. Elsevier Science Publishers B.V. (North-Holland), 1990. Alternatively see Communication and Concurrency, Prentice-Hall, Englewood Cliffs, 1989, of which an earlier version appeared as A Calculus of Communicating Systems, LNCS 92, Springer, 1980, doi: URL: http:dx.doi.org/10.1007/3-540-10235-3.
  18. Ernst-Ruediger Olderog and Tony (C.A.R.) Hoare. Specification-oriented semantics for communicating processes. Acta Informatica, 23:9-66, 1986. URL: https://doi.org/10.1007/BF00268075.
  19. Maximilian Pohlmann. Reducing strong reactive bisimilarity to strong bisimilarity. Bachelor’s thesis, Technische Universität Berlin, 2021. URL: https://maxpohlmann.github.io/Reducing-Reactive-to-Strong-Bisimilarity/thesis.pdf.
  20. Gaspard Reghem and Rob J. van Glabbeek. Branching bisimilarity for processes with time-outs. technical report, full version of the present paper, 2024. URL: https://arxiv.org/abs/2408.10117.
  21. Gaspard Reghem and Rob J. van Glabbeek. Concrete branching bisimilarity for processes with time-outs, 2024. URL: https://theory.stanford.edu/~rvg/abstracts.html#167.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact