Modal Fixpoint Logic: Some model theoretic questions [PhD Thesis]

1 Introduction 1
2 Preliminaries 11
2.1 Syntax of the -calculus . . . . . . . . . . . . . . . . . . . . . . . 11
2.2 Semantics for the -calculus . . . . . . . . . . . . . . . . . . . . . 15
2.3 Game terminology and the evaluation game . . . . . . . . . . . . 21
2.4 -Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
2.4.1 !-Automata . . . . . . . . . . . . . . . . . . . . . . . . . . 26
2.4.2 -automata . . . . . . . . . . . . . . . . . . . . . . . . . . 26
2.4.3 Disjunctive formulas . . . . . . . . . . . . . . . . . . . . . 31
2.5 Axiomatization of the -calculus . . . . . . . . . . . . . . . . . . . 32
2.6 Expressivity of the -calculus . . . . . . . . . . . . . . . . . . . . 33
2.6.1 Bisimulation . . . . . . . . . . . . . . . . . . . . . . . . . . 33
2.6.2 Expressivity results . . . . . . . . . . . . . . . . . . . . . . 35
2.6.3 Expressivity results for -programs . . . . . . . . . . . . . 39
2.7 Graded -calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
3 Completeness for the -calculus on nite trees 45
3.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
3.2 Rank of a formula . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
3.3 Completeness for generalized models . . . . . . . . . . . . . . . . 50
3.4 Completeness for nite trees . . . . . . . . . . . . . . . . . . . . . 55
3.5 Adding shallow axioms to K + x:2x . . . . . . . . . . . . . . . 58
3.6 Graded -calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
3.7 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
4 The -calculus and frame denability on trees 67
4.1 MLF-denability on trees . . . . . . . . . . . . . . . . . . . . . . 69
4.2 Graded -calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
4.3 Preservation under p-morphic images . . . . . . . . . . . . . . . . 84
4.4 Local denability . . . . . . . . . . . . . . . . . . . . . . . . . . . 92
4.5 Negative and projective denability . . . . . . . . . . . . . . . . . 108
4.5.1 Negative denability . . . . . . . . . . . . . . . . . . . . . 108
4.5.2 Projective denability . . . . . . . . . . . . . . . . . . . . 110
4.6 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113
5 Characterizations of fragments of the -calculus 115
5.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 117
5.1.1 Structures and games . . . . . . . . . . . . . . . . . . . . . 117
5.1.2 Guarded and disjunctive formulas . . . . . . . . . . . . . . 118
5.1.3 Expansion of a formula . . . . . . . . . . . . . . . . . . . . 119
5.1.4 Monotonicity and positivity . . . . . . . . . . . . . . . . . 120
5.2 Finite path property . . . . . . . . . . . . . . . . . . . . . . . . . 122
5.3 Finite width property . . . . . . . . . . . . . . . . . . . . . . . . . 129
5.4 Continuity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 139
5.4.1 Link with Scott continuity . . . . . . . . . . . . . . . . . . 139
5.4.2 Constructivity . . . . . . . . . . . . . . . . . . . . . . . . . 140
5.4.3 Semantic characterization of continuity . . . . . . . . . . . 141
5.5 Complete additivity . . . . . . . . . . . . . . . . . . . . . . . . . . 144
5.6 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 163
6 CoreXPath restricted to the descendant relation 165
6.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 167
6.1.1 XML trees . . . . . . . . . . . . . . . . . . . . . . . . . . . 167
6.1.2 CoreXPath, the navigational core of XPath 1.0 . . . . . . 167
6.1.3 Connections with modal logic . . . . . . . . . . . . . . . . 169
6.2 CoreXPath(#+) node expressions . . . . . . . . . . . . . . . . . . 171
6.3 CoreXPath(#+) path expressions . . . . . . . . . . . . . . . . . . 179
6.4 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 187
7 Automata for coalgebras: an approach using predicate liftings 189
7.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 191
7.1.1 Coalgebras . . . . . . . . . . . . . . . . . . . . . . . . . . . 191
7.1.2 Graph games . . . . . . . . . . . . . . . . . . . . . . . . . 194
7.2 Automata for the coalgebraic -calculus . . . . . . . . . . . . . . 197
7.3 Finite model property . . . . . . . . . . . . . . . . . . . . . . . . 203
7.4 One-step tableau completeness . . . . . . . . . . . . . . . . . . . . 214
7.5 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 222
8 Conclusion 223
Bibliography 227
Index 237
List of symbols 241
Samenvatting 243
Abstract 245