O'Reilly logo

Spin Model Checker, The: Primer and Reference Manual by Gerard J. Holzmann

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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 ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required