ABSTRACT
This chapter is concerned with language and models (structures) which are interrelated concepts that play a central role in logic and in this book. It introduces some of the elementary notions from model theory that are needed, such as structure, first-order language, and the satisfaction relation. The chapter defines the notions of (first-order) language and satisfaction to a degree required for reading this book, but without giving a full exposition. It also analyses Peterson’s well known critical section protocol and proves that the mutual exclusion property holds. The main aim in presenting the protocol is to give an example of the assertional method of proof which is the standard approach to concurrency using global states and transitions.
