The mu-calculus and Model Checking

Julian Bradfield; Igor Walukiewicz

doi:10.1007/978-3-319-10575-8_26

The mu-calculus and Model Checking

Research output: Chapter in Book/Report/Conference proceeding › Chapter (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 language	English
Title of host publication	Handbook of Model Checking
Editors	Edmund Clarke, Thomas Henziger, Helmut Veith, Roderick Bloem
Publisher	Springer
Pages	871-919
Number of pages	49
ISBN (Electronic)	978-3-319-10575-8
ISBN (Print)	978-3-319-10574-1
DOIs	https://doi.org/10.1007/978-3-319-10575-8_26
Publication status	Published - Mar 2018

Keywords / Materials (for Non-textual outputs)

model checking
temporal logic
mu-calculus

Access to Document

10.1007/978-3-319-10575-8_26

https://link.springer.com/chapter/10.1007/978-3-319-10575-8_26

Cite this

@inbook{54921aed0616436f87f183e6bfa4b5a1,

title = "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.",

keywords = "model checking, temporal logic, mu-calculus",

author = "Julian Bradfield and Igor Walukiewicz",

year = "2018",

month = mar,

doi = "10.1007/978-3-319-10575-8\_26",

language = "English",

isbn = "978-3-319-10574-1",

pages = "871--919",

editor = "Edmund Clarke and Thomas Henziger and Helmut Veith and Roderick Bloem",

booktitle = "Handbook of Model Checking",

publisher = "Springer",

address = "United Kingdom",

}

TY - CHAP

T1 - The mu-calculus and Model Checking

AU - Bradfield, Julian

AU - Walukiewicz, Igor

PY - 2018/3

Y1 - 2018/3

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

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

KW - model checking

KW - temporal logic

KW - mu-calculus

U2 - 10.1007/978-3-319-10575-8_26

DO - 10.1007/978-3-319-10575-8_26

M3 - Chapter (peer-reviewed)

SN - 978-3-319-10574-1

SP - 871

EP - 919

BT - Handbook of Model Checking

A2 - Clarke, Edmund

A2 - Henziger, Thomas

A2 - Veith, Helmut

A2 - Bloem, Roderick

PB - Springer

ER -

The mu-calculus and Model Checking

Abstract

Keywords / Materials (for Non-textual outputs)

Access to Document

Fingerprint

Cite this