Accueil🇫🇷Chercher

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. L'article original de Rabin utilise des automates d'arbres non déterministes avec des conditions dites de Rabin[1].

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 théorie monadique des ordres linéaires dénombrables 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 », .
Cet article est issu de wikipedia. Text licence: CC BY-SA 4.0, Des conditions supplémentaires peuvent s’appliquer aux fichiers multimédias.