Introduction to Modal and Temporal Mu-Calculi

@incollection{Bradfield01, abstract = {Modal mu-calculus is a logic obtained by adding fixpoint operators to ordinary modal logic, or Hennessy-Milner logic. The result is a very expressive logic, sufficient to subsume many other temporal logics such as CTL and CTL\&\#10033;. The modal mu-calculus is easy to model-check, and so makes a good ‘back-end’ logic for tools; it has an interesting theory, with some major problems still open; but it also has a certain reputation for being hard to read and write. This tutorial provides an introduction to the modal mu-calculus and related logics, suitable for those with some exposure to modal or temporal logic, but without prior knowledge of fixpoint logics. I start by reviewing the basic semantic setting of processes modelled as transition systems,and briefly review basic modal logic and temporal logics such as CTL. I then introduce the modal mu-calculus itself. I cover the formal syntax and semantics, and then give more informally the game-based intuition that is most useful in understanding formula of the logic. I next describe global and local model-checking techniques. Finally, I discuss the relationship between modal mu-calculus, automata and games, and some of the theoretical questions that have been and are now of interest. The tutorial is based around the handbook chapter [1],written with Colin Stirling,which forms the text for the tutorial.}, author = {Bradfield, Julian }, citeulike-article-id = {2776016}, doi = {10.1007/3-540-45694-5\_6}, journal = {CONCUR 2002 — Concurrency Theory}, pages = {221--231}, posted-at = {2008-05-09 15:37:27}, priority = {2}, title = {Introduction to Modal and Temporal Mu-Calculi}, url = {http://dx.doi.org/10.1007/3-540-45694-5\_6}, year = {2002} }

TY - CHAP ID - Bradfield01 TI - Introduction to Modal and Temporal Mu-Calculi JF - CONCUR 2002 — Concurrency Theory SP - 221 EP - 231 N2 - Modal mu-calculus is a logic obtained by adding fixpoint operators to ordinary modal logic, or Hennessy-Milner logic. The result is a very expressive logic, sufficient to subsume many other temporal logics such as CTL and CTL✱. The modal mu-calculus is easy to model-check, and so makes a good ‘back-end’ logic for tools; it has an interesting theory, with some major problems still open; but it also has a certain reputation for being hard to read and write. This tutorial provides an introduction to the modal mu-calculus and related logics, suitable for those with some exposure to modal or temporal logic, but without prior knowledge of fixpoint logics. I start by reviewing the basic semantic setting of processes modelled as transition systems,and briefly review basic modal logic and temporal logics such as CTL. I then introduce the modal mu-calculus itself. I cover the formal syntax and semantics, and then give more informally the game-based intuition that is most useful in understanding formula of the logic. I next describe global and local model-checking techniques. Finally, I discuss the relationship between modal mu-calculus, automata and games, and some of the theoretical questions that have been and are now of interest. The tutorial is based around the handbook chapter [1],written with Colin Stirling,which forms the text for the tutorial. AU - Bradfield, Julian PY - 2002/// UR - http://dx.doi.org/10.1007/3-540-45694-5_6 ER -