This book presents what in our opinion constitutes the basis of the theory of the mu-calculus, considered as an algebraic system rather than a logic. We have wished to present the subject in a unified way, and in a form as general as possible. Therefore, our emphasis is on the generality of the fixed-point notation, and on the connections between mu-calculus, games, and automata, which we also explain in an algebraic way. This book should be accessible for graduate or advanced undergraduate students both in mathematics and computer science. We have designed this book especially for researchers and students interested in logic in computer science, comuter aided verification, and general aspects of automata theory. We have aimed at gathering in a single place the fundamental results of the theory, that are currently very scattered in the literature, and often hardly accessible for interested readers. The presentation is self-contained, except for the proof of the Mc-Naughton's Determinization Theorem (see, e.g., [97]. However, we suppose that the reader is already familiar with some basic automata theory and universal algebra. The references, credits, and suggestions for further reading are given at the end of each chapter.
Author(s): André Arnold, Damian Niwiński
Series: Studies in Logic and the Foundations of Mathematics 146
Edition: 1
Publisher: Elsevier Science B.V.
Year: 2001
Language: English
Commentary: missing half-title, title page, dedication
Pages: 293
Cover......Page 1
Preface......Page 5
Table of Contents......Page 11
1.1.1 Least upper bounds and greatest lower bounds......Page 17
1.1.2 Complete lattices......Page 18
1.1.3 Some algebraic properties of lattices......Page 19
1.1.4 Symmetry in lattices......Page 20
1.1.6 Boolean algebras......Page 21
1.1.7 Products of lattices......Page 23
1.2.1 Monotonic and continuous mappings......Page 24
1.2.2 Fixed points of a function......Page 26
1.2.3 Nested fixed points......Page 30
1.2.4 Duality......Page 33
1.3 Some properties of fixed points......Page 35
1.4 Fixed points on product lattices......Page 40
1.4.1 The replacement lemma......Page 41
1.4.2 Bekič principle......Page 43
1.4.3 Gauss elimination......Page 46
1.4.4 Systems of equations......Page 47
1.6. Bibliographical notes and sources......Page 55
2. The μ-calculi: Syntax and semantics......Page 57
2.1 μ-calculi......Page 58
2.2 Functional μ-calculi......Page 60
2.3 Fixed-point terms......Page 62
2.3.2 The μ-calculus of fixed-point terms......Page 63
2.3.3 Semantics......Page 65
2.4 Quotient μ-calculi......Page 66
2.4.2 Variants of fixed-point terms......Page 67
2.5 Powerset interpretation......Page 69
2.6.2 A hierarchy of clones......Page 71
2.6.4 The Emerson-Lei hierarchy......Page 72
2.7.1 Vectorial extension of a μ-calculus......Page 74
2.7.2 Interpretations of vectorial fixed-point terms......Page 76
2.7.3 The vectorial hierarchy......Page 78
2.7.4 Vectorial fixed-point terms in normal form......Page 79
2.8 Bibliographic notes and sources......Page 85
3.1 Monotone Boolean functions......Page 87
3.2 Powerset interpretations and the Boolean μ-calculus......Page 88
3.3.1 Finite vectorial fixed-point terms......Page 91
3.3.2 Infinite vectors of fixed-point terms......Page 94
3.3.3 Infinite vectors of infinite fixed-point terms......Page 98
3.4 Bibliographic notes and sources......Page 99
4. Parity games......Page 101
4.1 Games and strategies......Page 102
4.2 Positional strategies......Page 103
4.3.1 Boolean terms for games......Page 104
4.3.2 Game terms......Page 109
4.4.1 Games for Boolean terms......Page 111
4.4.2 Games for powerset interpretations......Page 113
4.5 Weak parity games......Page 115
4.6 Bibliographic notes and sources......Page 117
5.1.1 Preliminary definitions......Page 121
5.1.3 Arden's lemma......Page 123
5.1.4 The μ-calculus of extended languages......Page 126
5.2.1 Automata on finite words......Page 131
5.2.2 Automata on infinite words......Page 133
5.2.3 Parity automata......Page 134
5.2.4 Recognizable languages......Page 138
5.2.5 McNaughton's determinization theorem......Page 141
5.3 Terms with intersection......Page 142
5.3.1 The μ-calculus of constrained languages......Page 144
5.3.2 Duality......Page 149
5.3.3 Interpretation of terms by constrained languages......Page 151
5.3.4 Recognizable constrained languages......Page 152
5.4 Bibliographic notes and sources......Page 154
6.1.1 Semi-algebras......Page 157
6.1.2 Powerset algebras......Page 159
6.1.3 Logical operations......Page 160
6.2 Modal μ-calculus......Page 161
6.3 Homomorphisms, μ-homomorphisms, and bisimulations......Page 164
6.4 Bibliographic notes and sources......Page 169
7.1 Automata over semi-algebras......Page 171
7.1.2 Basic definitions......Page 172
7.1.3 Hierarchy of indices......Page 175
7.1.4 Dual automata......Page 176
7.1.5 Relation to classical automata......Page 178
7.2.1 The μ-calculus of automata......Page 187
7.2.2 The interpretation as homomorphism......Page 193
7.3.1 From fixed-point terms to automata......Page 196
7.3.2 From automata to fixed-point terms......Page 199
7.3.3 Conclusion......Page 202
7.4 Bibliographic notes and sources......Page 203
8.1 Introduction......Page 207
8.2.1 Games on the binary tree......Page 208
8.2.2 Alternating automata on trees......Page 211
8.2.4 The hierarchy of Mostowski indices for tree languages......Page 214
8.2.5 Universal languages......Page 215
8.3 Weak alternating automata......Page 217
8.4 Bibliographic notes and sources......Page 219
9.1 The propositional μ-calculus......Page 221
9.2.2 Guarded terms......Page 224
9.3.2 A syntactic notion of intersection......Page 227
9.4 The powerset construction......Page 232
9.5 The νμ case......Page 233
9.6.1 McNaughton's Theorem revisited......Page 237
9.6.2 The simulation theorem......Page 238
9.6.3 The Rabin complementation lemma......Page 244
9.7 Bibliographic notes and sources......Page 245
10. Decision problems......Page 249
10.1 Disjunctive mappings......Page 250
10.2.1 Compact lattices......Page 251
10.2.2 Disjunctiveness of fixed-points......Page 252
10.2.3 Emptiness of nondeterministic tree automata......Page 255
10.3.1 Quotients of trees......Page 256
10.3.2 The regularity theorem......Page 257
10.4.1 Bounded decomposition......Page 258
10.4.2 Tree models......Page 260
10.4.3 Finite models and decidability......Page 264
10.5 Bibliographic notes and sources......Page 266
11.1 Evaluation of vectorial fixed-point terms......Page 269
11.1.1 A naive algorithm......Page 273
11.1.2 Improved algorithms......Page 274
11.2.1 Computations of winning positions......Page 281
11.2.2 Computations of winning strategies......Page 282
11.3 Bibliographic notes and sources......Page 283
Bibliography......Page 285
Index......Page 291
