Modal logics and mu-calculi: An introduction (Q2760241)

At the beginning a brief survey of modal logics, such as Hennessy-Milner logic, PDL and CTL, is given. Then mu-calculus is introduced, which includes fixpoints as recursion, approximating fixpoints, calculus syntax and semantics. Next, the theory of modal mu-calculus is presented, which includes fixpoint regeneration and the fundamental semantics theorem, the finite model property and decidability, axiomatization, and the approximant approach to model-checking of finite systems. Also other model-checking techniques as local model-checking and model-checking for infinite systems are discussed. The relationship of modal mu-calculus to other formalisms, in particular automata and games, is briefly mentioned.NEWLINENEWLINEFor the entire collection see [Zbl 0971.00006].