The motivation for the research that I will discuss in my talk is a claim by van Glabbeek and Höfner that CCS-like process algebras are not powerful enough to establish correctness of Peterson’s algorithm, and, in particular, prove the required liveness property. The culprit, according to van Glabbeek and Höfner, is that for these process algebras it is not possible to express an appropriate notion of justness. In an attempt to shed more light on van Glabbeek and Höfner’s claim, we have reconsidered the analysis of Peterson’s algorithm using the mCRL2 toolset. Our conclusion is that it is possible to give a convincing argument that Peterson’s algorithm satisfies the required liveness property for all just paths through a verification in the mCRL2 toolset. The ACP-style communication mechanism of mCRL2 and the power of the mu-calculus turned out to be instrumental.

(Research was joint work with Mark Bouwman and Tim Willemse.)