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

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.

Original language | English |
---|---|

Title of host publication | Handbook of Model Checking |

Editors | Edmund Clarke, Thomas Henziger, Helmut Veith, Roderick Bloem |

Publisher | Springer International Publishing |

Pages | 871-919 |

Number of pages | 49 |

ISBN (Electronic) | 978-3-319-10575-8 |

ISBN (Print) | 978-3-319-10574-1 |

DOIs | |

Publication status | Published - Mar 2018 |

## Keywords

- model checking
- temporal logic
- mu-calculus