%0 Conference Proceedings
%T Off-the-Shelf Automated Analysis of Liveness Properties for Just Paths
%+ Eindhoven University of Technology [Eindhoven] (TU/e)
%A Bouwman, Mark
%A Luttik, Bas
%A Willemse, Tim, A.C.
%Z Part 2: Short and Journal-First Papers
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 41th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)
%C Valletta, Malta
%Y Kirstin Peters
%Y Tim A.C. Willemse
%I Springer International Publishing
%3 Formal Techniques for Distributed Objects, Components, and Systems
%V LNCS-12719
%P 182-187
%8 2021-06-14
%D 2021
%R 10.1007/978-3-030-78089-0_11
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X 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.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-03740262/document
%2 https://inria.hal.science/hal-03740262/file/509782_1_En_11_Chapter.pdf
%L hal-03740262
%U https://inria.hal.science/hal-03740262
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-LNCS-12719