Une transformation de structures relationnelles qui développe un modèle en une forme arborescente en dupliquant des nœuds le long des chemins, de sorte que les relations locales deviennent des branches d'arbre, utilisée pour simplifier les arguments sémantiques et les analyses de décidabilité.

Principe

Conserver la satisfaction pour le fragment visé (souvent modal, gardé ou invariant par bisimulation) tout en convertissant des structures relationnelles arbitraires en formes arborescentes plus maniables.

Démonstration

Pour un cadre de Kripke avec des cycles, construire son dépliage en arbre en prenant pour nœuds tous les chemins finis ancrés et en reliant un chemin p à p·a lorsque a est un successeur ; l'arbre obtenu satisfait les mêmes formules modales invariantes par bisimulation que le cadre d'origine.

Mauvaise application

Appliquer sans précaution la technique à des logiques non invariantes par bisimulation ou à des langages exigeant des contraintes globales de cardinalité peut rompre l'équivalence de vérité et conduire à de fausses affirmations de décidabilité.

Conséquence

Donne la propriété de modèle en arbre, simplifie les arguments par bisimulation et ouvre souvent la voie à la décidabilité ou à des bornes de complexité en réduisant à des automates sur arbres ou à des constructions d'arbres infinis.

Inversion

En repliant l'arbre déplié en identifiant les nœuds correspondant au même élément original on reconstruit la structure relationnelle initiale, mais on peut réintroduire des cycles et des caractéristiques globales perdues dans la forme arborescente.

Limite

S'applique aux structures relationnelles et aux fragments respectant la localité et la bisimulation (modal, fragments gardés) ; elle ne préserve généralement pas les propriétés du second ordre, les contraintes globales de comptage ni les théories dépendant des groupes d'automorphismes.

Tension sémantique

Tension entre l'obtention de localité et la perte de structure globale : le dépliage facilite la vérification locale des modèles mais peut masquer ou détruire des invariants globaux comme la cardinalité finie ou la symétrie.

Synthèse

La Technique de Dépliage transforme systématiquement des modèles relationnels complexes en modèles arborescents qui conservent la vérité locale et invariante par bisimulation, permettant des preuves sémantiques et des analyses algorithmiques plus simples tout en excluant les phénomènes nécessitant une identification globale.