Document Open Access Logo

Enabling Preserving Bisimulation Equivalence

Authors Rob van Glabbeek, Peter Höfner , Weiyou Wang

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2021.33.pdf
  • Filesize: 0.9 MB
  • 20 pages

Document Identifiers

Author Details

Rob van Glabbeek
  • Data61, CSIRO, Sydney, Australia
  • Computer Science and Engineering, University of New South Wales, Sydney, Australia
Peter Höfner
  • School of Computing, Australian National University, Canberra, Australia
  • Data61, CSIRO, Sydney, Australia
Weiyou Wang
  • School of Computing, Australian National University, Canberra, Australia

Acknowledgements

We are grateful to Filippo De Bortoli.

Cite As Get BibTex

Rob van Glabbeek, Peter Höfner, and Weiyou Wang. Enabling Preserving Bisimulation Equivalence. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 33:1-33:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.CONCUR.2021.33

Abstract

Most fairness assumptions used for verifying liveness properties are criticised for being too strong or unrealistic. On the other hand, justness, arguably the minimal fairness assumption required for the verification of liveness properties, is not preserved by classical semantic equivalences, such as strong bisimilarity. To overcome this deficiency, we introduce a finer alternative to strong bisimilarity, called enabling preserving bisimilarity. We prove that this equivalence is justness-preserving and a congruence for all standard operators, including parallel composition.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Process calculi
  • Theory of computation → Distributed computing models
Keywords
  • bisimilarity
  • liveness properties
  • fairness assumptions
  • process algebra

Metrics

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

Related Versions

References

  1. Gérard Boudol, Ilaria Castellani, Matthew Hennessy, and Astrid Kiehn. A theory of processes with localities. Formal Aspects Comput., 6(2):165-200, 1994. URL: https://doi.org/10.1007/BF01221098.
  2. Sjoerd Cranen, Mohammad Reza Mousavi, and Michel A. Reniers. A rule format for associativity. In F. van Breugel and M. Chechik, editors, Concurrency Theory (CONCUR '08), volume 5201 of LNCS, pages 447-461. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-85361-9_35.
  3. Victor Dyseryn, Robert J. van Glabbeek, and Peter Höfner. Analysing mutual exclusion using process algebra with signals. In Kirstin Peters and Simone Tini, editors, Proc. Combined 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics, volume 255 of Electronic Proceedings in Theoretical Computer Science, pages 18-34. Open Publishing Association, 2017. URL: https://doi.org/10.4204/EPTCS.255.2.
  4. Ansgar Fehnker, Robert J. van Glabbeek, Peter Höfner, Annabelle K. McIver, Marius Portmann, and Wee Lum Tan. A process algebra for wireless mesh networks used for modelling, verifying and analysing AODV. Technical Report 5513, NICTA, 2013. URL: http://arxiv.org/abs/1312.7645.
  5. Nissim Francez. Fairness. Springer, 1986. URL: https://doi.org/10.1007/978-1-4612-4886-6.
  6. Robert J. van Glabbeek. Bisimulations for higher dimensional automata. Email message, July 7, 1991, 1991. URL: http://theory.stanford.edu/~rvg/hda.
  7. Robert J. van Glabbeek. On specifying timeouts. In L. Aceto and A.D. Gordon, editors, Short Contributions from the Workshop on Algebraic Process Calculi: The First Twenty Five Years and Beyond, PA '05, Bertinoro, Italy, 2005, volume 162 of Electronic Notes in Theoretical Computer Science, pages 112-113. Elsevier, 2005. URL: https://doi.org/10.1016/j.entcs.2005.12.083.
  8. Robert J. van Glabbeek. On the expressiveness of higher dimensional automata. Theoretical Computer Science, 368(1-2):169-194, 2006. URL: https://doi.org/10.1016/j.tcs.2006.06.024.
  9. Robert J. van Glabbeek. Justness: A completeness criterion for capturing liveness properties. Technical report, Data61, CSIRO, 2019. Extended abstract in M. Bojańczyk & A. Simpson, editors: Proc. 22st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2019); held as part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2019), Prague, Czech Republic, 2019, LNCS 11425, Springer, pp. 505-522, https://doi.org/10.1007/978-3-030-17127-8_29. URL: http://arxiv.org/abs/1909.00286.
  10. Robert J. van Glabbeek. Reactive temporal logic. In O. Dardha and J. Rot, editors, Proceedings Combined 27th International Workshop on Expressiveness in Concurrency and 17th Workshop on Structural Operational Semantics, Online, 31 August 2020, volume 322 of Electronic Proceedings in Theoretical Computer Science, pages 51-68. Open Publishing Association, 2020. URL: https://doi.org/10.4204/EPTCS.322.6.
  11. Robert J. van Glabbeek and Peter Höfner. CCS: it’s not fair! Acta Informatica, 52(2-3):175-205, 2015. URL: https://doi.org/10.1007/s00236-015-0221-6.
  12. Robert J. van Glabbeek and Peter Höfner. Progress, fairness and justness in process algebra. Technical Report 8501, NICTA, 2015. URL: http://arxiv.org/abs/1501.03268.
  13. Robert J. van Glabbeek and Peter Höfner. Progress, justness, and fairness. ACM Computing Surveys, 52(4), 2019. URL: https://doi.org/10.1145/3329125.
  14. Robert J. van Glabbeek, Peter Höfner, Marius Portmann, and Wee Lum Tan. Modelling and verifying the AODV routing protocol. Distributed Computing, 29(4):279-315, 2016. URL: https://doi.org/10.1007/s00446-015-0262-7.
  15. Robert J. van Glabbeek, Peter Höfner, and Weiyou Wang. Enabling preserving bisimulation equivalence, full version of the present paper, 2021. URL: http://arxiv.org/abs/2108.00142.
  16. Eric Goubault and Thomas P. Jensen. Homology of higher dimensional automata. In W.R. Cleaveland, editor, Proceedings CONCUR 92, Stony Brook, NY, USA, volume 630 of LNCS, pages 254-268. Springer, 1992. URL: https://doi.org/10.1007/BFb0084796.
  17. Leslie Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering, 3(2):125-143, 1977. URL: https://doi.org/10.1109/TSE.1977.229904.
  18. 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.
  19. Gordon D. Plotkin. A structural approach to operational semantics. Journal of Logic and Algebraic Programming, 60-61:17-139, 2004. Originally appeared in 1981. URL: https://doi.org/10.1016/j.jlap.2004.05.001.
  20. K. V. S. Prasad. A calculus of broadcasting systems. In Samson Abramsky and T. S. E. Maibaum, editors, TAPSOFT'91: Proceedings of the International Joint Conference on Theory and Practice of Software Development, Volume 1: Colloquium on Trees in Algebra and Programming (CAAP'91), volume 493 of LNCS, pages 338-358. Springer, 1991. URL: https://doi.org/10.1007/3-540-53982-4_19.
  21. Vaughan R. Pratt. Modeling concurrency with geometry. In Principles of Programming Languages (PoPL'91), pages 311-322, 1991. URL: https://doi.org/10.1145/99583.99625.
  22. Wolfgang Reisig. Understanding Petri Nets - Modeling Techniques, Analysis Methods, Case Studies. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-33278-4.
  23. Robert de Simone. Higher-level synchronising devices in Meije-SCCS. Theoretical Comp. Science, 37:245-267, 1985. URL: https://doi.org/10.1016/0304-3975(85)90093-3.
  24. Eugine W. Stark. Concurrent transition systems. Theoretical Computer Science, 64:221-269, 1989. URL: https://doi.org/10.1016/0304-3975(89)90050-9.
  25. Glynn Winskel. Event structures. In W. Brauer, W. Reisig, and G. Rozenberg, editors, Petri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets 1986, Part II, volume 255 of LNCS, pages 325-392. Springer, 1987. URL: https://doi.org/10.1007/3-540-17906-2_31.
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 About DROPS Imprint Privacy Contact