@inproceedings{84801334155946b08a6c79ab08588422,
title = "Off-the-Shelf Automated Analysis of Liveness Properties for Just Paths: (Extended Abstract)",
abstract = "Recent work by van Glabbeek and coauthors suggests that the liveness property for Peterson{\textquoteright}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{\textquoteright}s algorithm can be established convincingly with the mCRL2 toolset, which has a conventional ACP-style process-algebra based specification formalism.",
author = "Mark Bouwman and Bas Luttik and Tim Willemse",
year = "2021",
month = jun,
day = "8",
doi = "10.1007/978-3-030-78089-0\_11",
language = "English",
isbn = "978-3-030-78088-3",
series = "Lecture Notes in Computer Science (LNCS)",
publisher = "Springer",
pages = "182--187",
editor = "Kirstin Peters and Willemse, \{Tim A.\}",
booktitle = "Formal Techniques for Distributed Objects, Components, and Systems",
address = "Germany",
note = "41st IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2021 held as part of 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021 ; Conference date: 14-06-2021 Through 18-06-2021",
}