A study on the expressive power of some fragments of the modal µ-calculus

Alessandro Facchini

Description

Sous la direction de Igor Walukiewicz, Jacques Duparc
Thèse soutenue le 03 décembre 2010: Université de Lausanne (Suisse), Bordeaux 1
Dans ce travail nous étudions la complexité de certains fragments du mu-calcul selon deux points de vue: l’un syntaxique et l’autre topologique. Dans la première partie nous adoptons le point de vue syntaxique afin d'étudier le comportement du mu-calcul sur des classes restreintes de modèles. Parmi d'autres résultats, nous montrons en particulier que sur les modèles transitifs toute propriété définissable par une formule du mu-calcul est définissable par une formule sans alternance de points fixes. Pour ce qui concerne la perspective topologique, nous montrons d'abord que sur les modèles transitifs la logique modale correspond au fragment borélien du mu-calcul. Ensuite nous donnons une description effective des hiérarchies de Borel et de Wadge d'un sous-fragment sans alternance de cette logique sur les arbres binaires et vérifions que pour ce fragment les points de vue topologique et syntaxique coïncident.
-Mu-calcul
-Hiérarchie de points fixes
-Hiérarchie de Wadge
In this work we study the complexity of some fragments of the modal mu-calculus from two points of view: the syntactical and the topological. In the first part of the dissertation we adopt the syntactical point of view in order to study the behavior of this formalism on some restricted classes of models. Among other results, we show that on transitive transition systems, every mu-formula is logically equivalent to an alternation free formula. For what concerns the topological point of view, we first prove that on transitive models, the modal logic is exactly the Borel fragment of the modal mu-calculus. Then we provide an effective description of the Borel and Wadge hierarchies of a sub-fragment of the alternation free fragment of the mu-calculus on binary trees. Finally we verify that for this fragment the syntactical point of view and topological point of view coincide.
-Mu-calculus
-Fixpoint alternation hierarchy
-Wadge hierarchy
Source: http://www.theses.fr/2010BOR14210/document

Informations

• Publié par: Thesee
• Nombre de lectures: 30
• Langue: English
• Poids de l'ouvrage: 3 Mo

Extrait

N° d’ordre : 4210





THÈSE

PRÉSENTÉE A

L’UNIVERSITÉ BORDEAUX 1

ÉCOLE DOCTORALE DE MATHÉMATIQUES ET INFORMATIQUE

Par Alessandro FACCHINI

POUR OBTENIR LE GRADE DE

DOCTEUR
SPÉCIALITÉ : Informatique

A STUDY ON THE EXPRESSIVE POWER OF SOME
FRAGMENTS OF THE MODAL µ-CALCULUS


Professeur: Jacques DUPARC
Directeur de recherche CNRS : Igor WALUKIEWICZ




Soutenue le : 3 Décembre 2010

Devant la commission d’examen formée de :

M. DUPARC, Jacques Professeur Université de Lausanne Co-directeur de thèse
M. GARBINATO, Benoît Professeur Université de Lausanne Examinateur
M. GRÄDEL, Erich Professeur Université d’Aix-la-Chapelle Examinateur
M. JÄGER, Gerhard Professeur Université de Bern Examinateur
M. NIWINSKI, Damian Professeur Université de Varsovie Rapporteur
M. PIGNEUR Yves Professeur Université de Lausanne Président du Jury
M. VAN BENTHEM, Johan Professeur Université d’Amsterdam Rapporteur
M. WALUKIEWICZ, Igor DR CNRS Université de Bordeaux I Directeur de thèse
M. ZEITOUN, Marc Professeur Université de Bordeaux I Examinateur
Université Bordeaux 1
Les Sciences et les Technologies au service de l’Homme et de l’environnement
R´esum´e
Dans ce travail nous ´etudions la complexit´e de certains fragmentsduµ-calcul
selon deux points de vue: l’un syntaxique et l’autre topologique. Dans la
premi`ere partie nous adoptons le point de vue syntaxique afin d’´etudier le com-
portement du µ-calcul sur des classes restreintes de mod`eles. Parmi d’autres
r´esultats, nous montrons en particulier que sur les mod`eles transitifs toute pro-
pri´et´e d´efinissable par une formule du µ-calcul est d´efinissable par une formule
sansalternancedepoints fixes. Pource quiconcernelaperspectivetopologique,
nous montrons d’abord que sur les mod`eles transitifs la logique modale corre-
spond au fragment bor´elien du µ-calcul. Ensuite nous donnons une description
e!ective des hi´erarchies de Borel et de Wadge d’un sous-fragment sans alter-
nance de cette logique sur les arbres binaires et v´erifions que pour ce fragment
les points de vue topologique et syntaxique co¨ıncident.
Mots-cl´es: µ-calcul, alternance de points fixes, automatesd’arbres, hi´erarchie
de Wadge, hi´erarchie de Borel.
Abstract
In this workwestudy the complexityof some fragmentsof the modalµ-calculus
from two points of view: the syntactical and the topological. In the first part
of the dissertation we adopt the syntactical point of view in order tostudy
the behavior of this formalism on some restricted classes of models. Among
other results, we show that on transitive transition systems, every µ-formula
is logically equivalent to an alternation free formula. For what concerns the
topological point of view, we first prove that on transitive models, the modal
logic is exactly the Borel fragment of the modal µ-calculus. Then we provide
an e!ective description of the Borel and Wadge hierarchies of a sub-fragment
of the alternation free fragment of the µ-calculus on binary trees. Finally we
verify that for this fragment the syntactical point of view and topological point
of view coincide.
Keywords : µ-calculus, fixpoint alternation, tree automata, Wadge hierarchy,
Borel hierarchy.
IIIBORDEAUX UNIVERSITY 1
Laboratoire Bordelais de Recherche en Informatique
UNIVERSITY OF LAUSANNE
Faculty of Business and Economics
ASTUDY ON THEEXPRESSIVEPOWER
OFSOMEFRAGMENTS OF THEMODAL
µ-CALCULUS
Alessandro Facchini
PhD DissertationIIContents
Long Abstract (in French) 1
Introduction 3
Outline of the dissertation . . . . . . . . . . . . . . . . . . . . . . . . . 7
Related works . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
Acknowledgements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
1Logics,GamesandAutomata 13
1.1 Trees and transition systems . . . . . . . . . . . . . . . . . . . . 13
1.1.1 Trees and their undressing . . . . . . . . . . . . . . . . . . 13
1.1.2 Transition systems . . . . . . . . . . . . . . . . . . . . . . 15
1.2 Topology . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
1.2.1 The Borel sets . . . . . . . . . . . . . . . . . . . . . . . . 16
1.2.2 The Wadge game . . . . . . . . . . . . . . . . . . . . . . . 18
1.3 Monadic second order logics . . . . . . . . . . . . . . . . . . . . . 20
1.3.1 Full MSO ........................... 20
1.3.2 Weak MSO .......................... 22
1.4 The modal µ-calculus . . . . . . . . . . . . . . . . . . . . . . . . 23
1.4.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
1.4.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
1.4.3 Another formalism for the binary tree . . . . . . . . . . . 28
1.4.4 MSO vs µ-calculus . . . . . . . . . . . . . . . . . . . . . . 29
1.5 The fixpoint alternation hierarchy . . . . . . . . . . . . . . . . . 30
1.6 Parity games . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
1.7 Evaluation games . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
1.8 Automata for the modal µ-calculus . . . . . . . . . . . . . . . . . 39
1.8.1 Automata on binary trees . . . . . . . . . . . . . . . . . . 39
1.8.2 Automata on transition systems . . . . . . . . . . . . . . 40
1.9 The Mostowski-Rabin index hierarchy . . . . . . . . . . . . . . . 41
1.10 Summarizing remarks . . . . . . . . . . . . . . . . . . . . . . . . 45
IThe µ-Calculus on Restricted Classes of Models 47
2TheFixpointHierarchyonReflexive,Transitive,andTransitive-
Symetric Models 49
2.1 Preliminary remarks . . . . . . . . . . . . . . . . . . . . . . . . . 49
2.2 Finite model theorems . . . . . . . . . . . . . . . . . . . . . . . . 50
IIIIV CONTENTS
2.2.1 Finite model theorem for reflexive transition systems . . . 50
2.2.2 Finite model theorem for transitive transition systems . . 51
2.3 The transitive and symmetric case . . . . . . . . . . . . . . . . . 52
2.4 The transitive case . . . . . . . . . . . . . . . . . . . . . . . . . . 54
2.4.1 Some technical preliminaries . . . . . . . . . . . . . . . . 54
2.4.2 A first reduction . . . . . . . . . . . . . . . . . . . . . . . 57
2.4.3 Normalizing the winning strategies . . . . . . . . . . . . . 59
2.4.4 Encoding normalized winning strategies . . . . . . . . . . 62
2.4.5 The collapse over transitive models . . . . . . . . . . . . . 67
2.5 The reflexive case . . . . . . . . . . . . . . . . . . . . . . . . . . . 70
2.6 Summarizing remarks . . . . . . . . . . . . . . . . . . . . . . . . 73
3Theµ-Calculus vs the G¨odel-L¨ob Logic 75
3.1 Preliminary remarks . . . . . . . . . . . . . . . . . . . . . . . . . 75
3.2 Go¨del-Lo¨b Logic GL ......................... 76
3.2.1 Syntax and Semantics . . . . . . . . . . . . . . . . . . . . 76
3.2.2 Embedding GL into the modal µ-calculus . . . . . . . . . 77
3.3 The modal µ-calculus over GL.................... 78
!3.4 The modal µ -calculus . . . . . . . . . . . . . . . . . . . . . . . . 79
3.4.1 Basic notions and results . . . . . . . . . . . . . . . . . . 79
3.4.2 The unicity of fixpoints . . . . . . . . . . . . . . . . . . . 82
!3.4.3 Collapsing the modal µ -calculus . . . . . . . . . . . . . . 85
3.5 Summarizing remarks . . . . . . . . . . . . . . . . . . . . . . . . 88
4CharacterizingtheModalFragmentonTransitiveModels 89
4.1 Preliminary remarks . . . . . . . . . . . . . . . . . . . . . . . . . 89
4.2 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91
4.2.1 The beauty of forests. . . . . . . . . . . . . . . . . . . . . 91
4.2.2 More on monadic second order logics . . . . . . . . . . . . 94
4.2.3 The logic EF and EF-bisimulation . . . . . . . . . . . . . 100
4.3 The complexity of conciliatory tree languages . . . . . . . . . . . 102
4.3.1 The set of well-founded trees is not Borel . . . . . . . . . 104
4.4 Characterizations of EF over infinite trees . . . . . . . . . . . . . 105
4.5 Modal=Borel, on transitive models . . . . . . . . . . . . . . . . . 107
4.6 Summarizing remarks . . . . . . . . . . . . . . . . . . . . . . . . 108
II HierarchicalQuestionsforTreeLanguagesDefinable
Without Alternation 111
5Preliminaries 113
5.1 Topological hierarchies . . . . . . . . . . . . . . . . . . . . . . . . 114
5.1.1 The topological complexity of regular tree languages . . . 114
5.1.2 The Wadge hierarchy of Borel sets of finite rank . . . . . 115
5.2 Weak alternating tree automata . . . . . . . . . . . . . . . . . . . 118
5.2.1 Paths and loops . . . . . . . . . . . . . . . . . . . . . . . 118
5.2.2 Weak index vs Borel rank . . . . . . . . . . . . . . . . . . 118
5.2.3 The Wadge hierarchy of weak alternating automata . . . 119
5.3 Summarizing remarks . . . . . . . . . . . . . . . . . . . . . . . . 122CONTENTS V
6DecidableHierarchiesforLinearGameAutomata 123
6.1 Preliminary remarks . . . . . . . . . . . . . . . . . . . . . . . . . 123
6.2 Linear game automata . . . . . . . . . . . . . . . . .