×

Rudiments of \(\mu\)-calculus. (English) Zbl 0968.03002

Studies in Logic and the Foundations of Mathematics. 146. Amsterdam: Elsevier. xvii, 277 p. (2001).
\(\mu\)-calculus deals with computation of least fixed points of monotonic operators over a powerset, or, more generally, over a complete lattice. A distinctive feature of the book, the first published one entirely devoted to this subject, is its algebraic treatment: \(\mu\)-calculus is introduced in a very general form, as an abstract algebraic structure, a particular case of which is the ‘functional \(\mu\)-calculus’ mentioned above. In my opinion, the generality of the proposed framework is well-justified in the book, at least from the mathematical viewpoint. Still, the first chapter of the book provides the proper traditional background to the topic, viz. complete lattices and the theory of least and greatest fixed points in them, as well as some less-known facts about fixed points of systems of recursive equations. The formal treatment of syntax and semantics of \(\mu\)-calculus is presented in Chapter 2, while Chapter 3 presents the particular case of the Boolean (i.e. essentially powerset-based) \(\mu\)-calculus.
Chapter 4 discusses the relationship between \(\mu\)-calculus and games, more specifically two-player parity games of perfect information: on the one hand the existence of winning strategies in such games is naturally expressible in \(\mu\)-calculus, which on the other hand is provided with an alternative, ‘dynamic’ semantics in terms of winning sets of states in parity games.
Another important aspect of \(\mu\)-calculus, presented in Chapter 5, is its link with automata on finite and infinite words and trees, going back to the classical work of Büchi and of Rabin [see, e.g., M. O. Rabin, Trans. Am. Math. Soc. 141, 1-35 (1969; Zbl 0221.02031)]. This link is developed further in Chapter 7 where an equivalence is established between \(\mu\)-calculus and generalized automata (incorporating non-deterministic and alternating automata), the semantics of which is given in powerset algebras by means of parity games. These automata are organized into an abstract \(\mu\)-calculus, and here the abstract algebraic approach pays off.
Chapter 6 presents D. Kozen’s modal \(\mu\)-calculus [Theor. Comput. Sci. 27, 333-354 (1983; Zbl 0553.03007)] in the framework of powerset algebras and notes the link between bisimulations and homomorphisms of \(\mu\)-calculi. In Chapter 8 the alternation hierarchy is treated and shown to be strict in the powerset algebra of trees. Chapter 9 interprets the simulation theorem of alternating automata by non-deterministic ones (a strengthening of Rabin’s complementation lemma) in the framework of the abstract \(\mu\)-calculus as eliminability of the intersection operator in closed fixpoint terms. Chapter 10 discusses decidability problems of \(\mu\)-calculus and the last Chapter 11 presents some related algorithms.
Despite the absence of some important topics of \(\mu\)-calculus (such as deductive systems, the fixpoint extension of first-order logic, and some important related results in descriptive complexity and finite model theory) the book is a solid, conceptually and mathematically profound, modern treatment of the subject, worth reading for an audience ranging from graduate students to working mathematicians and computer scientists.

MSC:

03-02 Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations
03-01 Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations
03B70 Logic in computer science
03G10 Logical aspects of lattices and related structures
68Q70 Algebraic theory of languages and automata
08A70 Applications of universal algebra in computer science
03D05 Automata and formal grammars in connection with logical questions
06B23 Complete lattices, completions
03B45 Modal logic (including the logic of norms)
68Q45 Formal languages and automata
91A99 Game theory
PDFBibTeX XMLCite