Spin Model Checker, The: Primer and Reference Manual

Chapter 6. Automata and Logic

	“Obstacles are those frightful things you see when you take your eyes off your goal.”
	--(Henry Ford, 1863–1947)

The model checking method that we will describe in the next few chapters is based on a variation of the classic theory of finite automata. This variation is known as the theory of ω-automata. The main difference with standard finite automata theory is that the acceptance conditions for ω-automata cover not just finite but also infinite executions.

Logical correctness properties are formalized in this theory as ω-regular properties. We will see shortly that ω-automata have just the right type of expressive power to model both process behavior in distributed systems and a broad range of correctness properties ...