Sat, 05 Jul 2008 11:58:26 BST CiteULike: di rob_quill Bradfield http://www.citeulike.org/user/rob_quill/author/Bradfield CiteULike.org en-gb Copyright © 2004-2008 citeulike.org http://www.citeulike.org/user/rob_quill/article/2776016 <i>CONCUR 2002 — Concurrency Theory (2002), pp. 221-231.</i><br /><br />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. Introduction to Modal and Temporal Mu-Calculi Julian Bradfield doi:10.1007/3-540-45694-5_6 CONCUR 2002 — Concurrency Theory (2002), pp. 221-231. 2008-05-09T14:36:32-00:00 2002 CONCUR 2002 — Concurrency Theory 221 231 no-tag