Formalization of mutual exclusion algorithms in N-labeled calculus

A family of formal systems called "labeled calculi" have been investigated lately for verification and analysis of time-concerned cooperating program systems. These calculi have high formality since they are based on the Peano arithmetic, one of the natural number theories. They are axiom- and proof-based approaches, i.e. properties of systems are verified by formal proofs. These approaches are more rigid and precise than that of model-checking. Among the labeled calculi, N-labeled calculus is the simplest and suited for usual time-concerned programs such as mutual exclusion. Mutual exclusion algorithms are indispensable for contemporary programs having parallel tasks/jobs/processes, and they offer typical examples of verification of such time-concerned cooperating programs. In this article, two mutual exclusion algorithms are formally represented in the calculus for verification.