The mu-calculus and Model Checking

Julian Bradfield, Igor Walukiewicz

Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)peer-review

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.
Original languageEnglish
Title of host publicationHandbook of Model Checking
EditorsEdmund Clarke, Thomas Henziger, Helmut Veith, Roderick Bloem
PublisherSpringer International Publishing
Pages871-919
Number of pages49
ISBN (Electronic)978-3-319-10575-8
ISBN (Print)978-3-319-10574-1
DOIs
Publication statusPublished - Mar 2018

Keywords

  • model checking
  • temporal logic
  • mu-calculus

Fingerprint

Dive into the research topics of 'The mu-calculus and Model Checking'. Together they form a unique fingerprint.

Cite this