September 2003
Intermediate to advanced
608 pages
14h 14m
English
“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 ...
Read now
Unlock full access