Théorème de Rabin sur les arbres

En informatique théorique, le théorème de Rabin sur les arbres énonce la décidabilité de la théorie monadique du second ordre de l'arbre binaire infini complet, mais aussi des arbres infinis d'arité finie fixée, et de l'arbre infini d'arité dénombrable. Ce théorème a été démontré par Michael Rabin en 1969[1],[2].

Démonstrations

Il existe plusieurs démonstrations de ce théorème dans la littérature[réf. nécessaire]. L'article original de Rabin utilise des automates d'arbres non déterministes avec des conditions dites de Rabin[1].

Donnons à présent la démonstration issue de[réf. nécessaire]. Sans perte de généralité, on suppose qu'il n'y a pas de variables du premier ordre dans la formule. La démonstration ressemble beaucoup à la démonstration de Büchi pour S1S. On construit par induction sur les formules un automate d'arbres alternants. L'automate d'arbres pour une sous-formule donnée reconnaît exactement les arbres binaires infinis étiquettés par les prédicats (c.-à-d. les variables du second ordre) qui satisfont cette sous-formule. On teste si la formule est vraie sur l'arbre binaire infini complet ssi le langage de l'automate construit est non vide.

Applications

Le théorème de Rabin sur les arbres permet de démontrer que[2] :

  • la logique modale S4 est décidable ;
  • la logique modale KvB est décidable ;
  • la logique du mu-calcul, la logique temporelle CTL* sont décidables.

Notes et références
  1. (en) Michael O. Rabin, « Decidability of second-order theories and automata on infinite trees », Bull. Amer. Math. Soc., vol. 74, no 5,‎ , p. 1025-1029 (lire en ligne, consulté le )
  2. (en) S. Steinert-Threlkeld, « Rabin's Tree Theorem and Applications », .
  • Portail de l'informatique théorique
  • Portail des mathématiques
Cet article est issu de Wikipedia. Le texte est sous licence Creative Commons - Attribution - Partage dans les Mêmes. Des conditions supplémentaires peuvent s'appliquer aux fichiers multimédias.