The mu-calculus and model checking

Abstract

This chapter presents that part of the theory of the μ-calculus that is relevant to the model-checking problem as broadly understood. The μ-calculus is one of the most important logics in model checking. It is a logic with an exceptional balance between expressiveness and algorithmic properties. The chapter describes at length the game characterization of the semantics of the μ-calculus. It discusses the theory of the μ-calculus starting with the tree-model property, and bisimulation invariance. Then it develops the notion of modal automaton: an automaton-based model behind the μ-calculus. It gives a quite detailed explanation of the satisfiability algorithm, followed by results on alternation hierarchy, proof systems, and interpolation. Finally, the chapter discusses the relation of the μ- calculus to monadic second-order logic as well as to some program and temporal logics. It also presents two extensions of the μ-calculus that allow us to address issues such as inverse modalities.