Abstract
Recent work by van Glabbeek and coauthors suggests that the liveness property for Peterson’s mutual exclusion algorithm, which states that any process wanting to enter the critical section will eventually enter it, cannot be analysed in CCS and related formalisms. In our article, we explore the formal underpinning of this suggestion and its ramifications. In particular, we show that the liveness property for Peterson’s algorithm can be established convincingly with the mCRL2 toolset, which has a conventional ACP-style process-algebra based specification formalism.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
The mCRL2 sources can be found in the academic example directory of the mCRL2 repository, see https://github.com/mCRL2org/mCRL2, revision b45856d9a.
References
Bouwman, M., Luttik, B., Willemse, T.: Off-the-shelf automated analysis of liveness properties for just paths. Acta Informatica 57, 551–590 (2020). https://doi.org/10.1007/s00236-020-00371-w
Bunte, O., et al.: The mCRL2 toolset for analysing concurrent systems. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 21–39. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17465-1_2
Cranen, S., Luttik, B., Willemse, T.A.C.: Evidence for fixpoint logic. In: CSL. Volume 41 of LIPIcs, pp. 78–93. Schloß Dagstuhl - Leibniz-Zentrum für Informatik (2015)
Dyseryn, V., van Glabbeek, R.J., Höfner, P.: Analysing mutual exclusion using process algebra with signals. In: Peters, K., Tini, S. (eds.) Proceedings of EXPRESS/SOS 2017. Volume 255 of EPTCS, pp. 18–34 (2017)
Glabbeek, R.: Justness. In: Bojańczyk, M., Simpson, A. (eds.) FoSSaCS 2019. LNCS, vol. 11425, pp. 505–522. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17127-8_29
van Glabbeek, R.J., Höfner, P.: 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). https://doi.org/10.1007/s00236-015-0221-6
van Glabbeek, R.J., Höfner, P.: Progress, justness, and fairness. ACM Comput. Surv. 52(4), 69:1–69:38 (2019)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 IFIP International Federation for Information Processing
About this paper
Cite this paper
Bouwman, M., Luttik, B., Willemse, T. (2021). Off-the-Shelf Automated Analysis of Liveness Properties for Just Paths. In: Peters, K., Willemse, T.A.C. (eds) Formal Techniques for Distributed Objects, Components, and Systems. FORTE 2021. Lecture Notes in Computer Science(), vol 12719. Springer, Cham. https://doi.org/10.1007/978-3-030-78089-0_11
Download citation
DOI: https://doi.org/10.1007/978-3-030-78089-0_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-78088-3
Online ISBN: 978-3-030-78089-0
eBook Packages: Computer ScienceComputer Science (R0)
