When talking about mutual exclusion, many textbooks start by introducing Peterson’s algorithm for two processes. The algorithm looks very simple, but upon closer inspection its behaviour is deceptively subtle. Less commonly known are extensions of Peterson’s algorithm to n processes. In this talk, I will look at such generalisations. I will also describe how these processes can be modelled and verified using mCRL2.