Logique MSO de Presburger (PMSO)

Table des matières

Introduction
1 Définitions de base
1.1 Multiensembles
1.2 Arithmétique de Presburger
1.3 Modèle d’arbres et représentations des arbres
2 Automates
2.1 Automates de Presburger
2.2 Automates à contraintes numériques
2.2.1 Exécution d’un automate et calcul d’une exécution
2.2.2 Automate déterministe et automate complet
2.2.3 Sous classes d’automates à contraintes numériques
2.3 Propriétés des automates à contraintes numériques
2.3.1 Déterminisation
2.3.2 Clôture par les opérations booléennes
2.3.3 Clôture par homomorphisme
2.3.4 Test du vide
2.3.5 Test d’appartenance
2.4 Propriétés des automates à contraintes numériques sans étoile et semilinéaires
2.4.1 Déterminisation
2.4.2 Clôture par les opérations booléennes
2.4.3 Clôture par homomorphisme
2.4.4 Test du vide
2.4.5 Test d’appartenance
3 Logiques
3.1 Logique monadique du second ordre et extension
3.1.1 Logique monadique du second ordre (MSO)
3.1.2 Logique MSO de Presburger (PMSO)
3.1.3 Logiques monadiques du second ordre et automates à contraintes numériques
3.2 Logique spatiale (LS)
3.2.1 Syntaxe
3.2.2 Sémantique
3.2.3 Opérateurs dérivés
3.2.4 Propriétés de la satisfiabilité
3.2.5 Fragments et variantes de la logique
3.2.6 Exemples
Conclusion