Document Open Access Logo

Reactive Bisimulation Semantics for a Process Algebra with Time-Outs

Author Rob van Glabbeek

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2020.6.pdf
  • Filesize: 0.53 MB
  • 23 pages

Document Identifiers

Author Details

Rob van Glabbeek
  • Data61, CSIRO, Sydney, Australia
  • UNSW, Sydney, Australia

Acknowledgements

My thanks to the referees for helpful feedback.

Cite As Get BibTex

Rob van Glabbeek. Reactive Bisimulation Semantics for a Process Algebra with Time-Outs. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 6:1-6:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.CONCUR.2020.6

Abstract

This paper introduces the counterpart of strong bisimilarity for labelled transition systems extended with time-out transitions. It supports this concept through a modal characterisation, congruence results for a standard process algebra with recursion, and a complete axiomatisation.

Subject Classification

ACM Subject Classification
  • Theory of computation → Process calculi
Keywords
  • Process algebra
  • time-outs
  • labelled transition systems
  • reactive bisimulation semantics
  • Hennessy-Milner logic
  • modal characterisations
  • recursion
  • complete axiomatisations

Metrics

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

Related Versions

References

  1. J.C.M. Baeten and W.P. Weijland. Process Algebra. Cambridge Tracts in Theoretical Computer Science 18. Cambridge University Press, 1990. URL: https://doi.org/10.1017/CBO9780511624193.
  2. M.S. Bouwman. Liveness analysis in process algebra: simpler techniques to model mutex algorithms. Technical report, Eindhoven University of Technology, 2018. URL: http://www.win.tue.nl/~timw/downloads/bouwman_seminar.pdf.
  3. M.S. Bouwman, B. Luttik, and T.A.C. Willemse. Off-the-shelf automated analysis of liveness properties for just paths. Acta Informatica, 57(3-5):551-590, 2020. URL: https://doi.org/10.1007/s00236-020-00371-w.
  4. S.D. Brookes, C.A.R. Hoare, and 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.
  5. J. Davies and S. Schneider. Recursion induction for real-time processes. Formal Aspects of Computing, 5(6):530-553, 1993. URL: https://doi.org/10.1007/BF01211248.
  6. R. De Nicola and M. Hennessy. Testing equivalences for processes. Theoretical Computer Science, 34:83-133, 1984. URL: https://doi.org/10.1016/0304-3975(84)90113-0.
  7. V. Dyseryn, R.J. van Glabbeek, and P. Höfner. Analysing mutual exclusion using process algebra with signals. In K. Peters and S. Tini, editors, Proceedings Combined 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics, Berlin, Germany, 4th September 2017, 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.
  8. W. 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.
  9. R.J. van Glabbeek. A complete axiomatization for branching bisimulation congruence of finite-state behaviours. In A.M. Borzyszkowski and S. Sokołowski, editors, Proceedings 18^th International Symposium on Mathematical Foundations of Computer Science, MFCS '93, Gdansk, Poland, August/September 1993, volume 711 of LNCS, pages 473-484. Springer, 1993. URL: https://doi.org/10.1007/3-540-57182-5_39.
  10. R.J. van Glabbeek. The linear time - branching time spectrum II; the semantics of sequential systems with silent moves. 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.
  11. R.J. van Glabbeek. On the expressiveness of ACP (extended abstract). In A. Ponse, C. Verhoef, and S.F.M. van Vlijmen, editors, Proceedings First Workshop on the Algebra of Communicating Processes, ACP'94, Utrecht, The Netherlands, May 1994, Workshops in Computing, pages 188-217. Springer, 1994. URL: https://doi.org/10.1007/978-1-4471-2120-6_8.
  12. R.J. van Glabbeek. The linear time - branching time spectrum I; the semantics of concrete, sequential processes. In J.A. Bergstra, A. Ponse, and S.A. Smolka, editors, Handbook of Process Algebra, chapter 1, pages 3-99. Elsevier, 2001. URL: https://doi.org/10.1016/B978-044482830-9/50019-9.
  13. R.J. van Glabbeek. The meaning of negative premises in transition system specifications II. Journal of Logic and Algebraic Programming, 60-61:229-258, 2004. URL: https://doi.org/10.1016/j.jlap.2004.03.007.
  14. R.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.
  15. R.J. van Glabbeek. Ensuring liveness properties of distributed systems: Open problems. Journal of Logical and Algebraic Methods in Programming, 109, 2019. URL: https://doi.org/10.1016/j.jlamp.2019.100480.
  16. R.J. van Glabbeek. Failure trace semantics for a process algebra with time-outs, 2020. URL: http://arxiv.org/abs/2002.10814.
  17. R.J. van Glabbeek and P. Höfner. CCS: it’s not fair! Fair schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions. Acta Informatica, 52(2-3):175-205, 2015. URL: https://doi.org/10.1007/s00236-015-0221-6.
  18. R.J. van Glabbeek and P. Höfner. Progress, justness and fairness. ACM Computing Surveys, 52(4), August 2019. URL: https://doi.org/10.1145/3329125.
  19. R.J. van Glabbeek and C.A. Middelburg. On infinite guarded recursive specifications in process algebra, 2020. URL: http://arxiv.org/abs/2005.00746.
  20. R.J. van Glabbeek and W.P. 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.
  21. J.F. Groote. Transition system specifications with negative premises. Theoretical Computer Science, 118:263-299, 1993. URL: https://doi.org/10.1016/0304-3975(93)90111-6.
  22. J.F. Groote and F.W. Vaandrager. Structured operational semantics and bisimulation as a congruence. Information and Computation, 100(2):202-260, October 1992. URL: https://doi.org/10.1016/0890-5401(92)90013-6.
  23. M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137-161, 1985. URL: https://doi.org/10.1145/2455.2460.
  24. C.A.R. Hoare. Communicating Sequential Processes. Prentice Hall, Englewood Cliffs, 1985. Google Scholar
  25. X. Liu and T.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), Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. To appear. Google Scholar
  26. M. Lohrey, P.R. D'Argenio, and H. Hermanns. Axiomatising divergence. Information and Computation, 203(2):115-144, 2005. URL: https://doi.org/10.1016/j.ic.2005.05.007.
  27. R. Milner. A complete inference system for a class of regular behaviours. Journal of Computer and System Sciences, 28:439-466, 1984. URL: https://doi.org/10.1016/0022-0000(84)90023-0.
  28. R. Milner. A complete axiomatisation for observational congruence of finite-state behaviors. Information and Computation, 81(2):227-247, 1989. URL: https://doi.org/10.1016/0890-5401(89)90070-9.
  29. R. 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.
  30. E.-R. Olderog. Operational Petri net semantics for CCSP. In G. Rozenberg, editor, Advances in Petri Nets 1987, volume 266 of LNCS, pages 196-223. Springer, 1987. URL: https://doi.org/10.1007/3-540-18086-9_27.
  31. E.-R. Olderog and C.A.R. Hoare. Specification-oriented semantics for communicating processes. Acta Informatica, 23:9-66, 1986. URL: https://doi.org/10.1007/BF00268075.
  32. J. Parrow and P. Sjödin. Multiway synchronization verified with coupled simulation. In W.R. Cleaveland, editor, Proceedings CONCUR 92, Stony Brook, NY, USA, volume 630 of LNCS, pages 518-533. Springer, 1992. URL: https://doi.org/10.1007/BFb0084813.
  33. G.M. Reed and A.W. Roscoe. A timed model for communicating sequential processes. Theoretical Computer Science, 58:249-261, 1988. URL: https://doi.org/10.1016/0304-3975(88)90030-8.
  34. F.W. Vaandrager. Expressiveness results for process algebras. In J.W. de Bakker, W.P. de Roever, and G. Rozenberg, editors, Proceedings REX Workshop on Semantics: Foundations and Applications, Beekbergen, The Netherlands, June 1992, volume 666 of LNCS, pages 609-638. Springer, 1993. URL: https://doi.org/10.1007/3-540-56596-5_49.
  35. D.J. Walker. Bisimulation and divergence. Information and Computation, 85(2):202-241, 1990. URL: https://doi.org/10.1016/0890-5401(90)90048-M.
  36. Ernst Zermelo. Untersuchungen über die Grundlagen der Mengenlehre I. Mathematische Annalen, 65(2):261-281, 1908. URL: https://doi.org/10.1007/bf01449999.
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