Automata, logic and games for the λ-calculus - Ong, C (Springer, 2016)
Automata, logic and games provide the mathematical theory that underpins the model checking of reactive systems: - automata on infinite words and trees as models of computation for statebased systems, - logical systems such as temporal and modal logics for specifying correctness properties, and - two-person games as a mathematical model of the interactions between a system and its environment.