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,.
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.
Applications
Le théorème de Rabin sur les arbres permet de démontrer que :
- 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
- Portail de l'informatique théorique
- Portail des mathématiques
