Reading the book on Principles of Model Checking by Christel Baier and Joost-Pieter Katoen, on page 43-45, I was reminded about a particular property of Peterson's mutual exclusion algorithm that I forgot from my undergraduate operating systems class, and therefore, I had pondered till I read the book. In particular, I was wondering why the need for the turn variable. Peterson's mutual exclusion algorithm is special in the way that it has the inclusion of a scheduling strategy to ensure the progress of the competing processes. Ha, I really forgot the obvious!