Propriétés logiques du non-déterminisme
et
mu-calcul modal



Cette thèse traite de la spécification logique des comportements non déterministes. Plus précisément, on s'intéresse aux propriétés logiques des systèmes de transitions dont la sémantique est close par équivalence de bisimulation.

La logique modale paramétrée et son extension par points fixes : le mu-calcul modal, dont les formules satisfont cette propriété, s'imposent comme objets de notre étude.

On donne tout d'abord une caractérisation de la sémantique des mu-formules à l'aide d'une notion de tableau. Cette notion induit une forme originale d'automates appelés automates modaux alternants qui apparaissent comme des systèmes de plus petit et plus grand point fixe modaux.

On démontre alors un théorème de simulation analogue à celui de Muller et Schupp dans le cas des arbres binaires prouvant que tout automate modal alternant peut être simulé par un automate modal sans alternances. Ce théorème passe par la définition d'une forme normale disjonctive pour les formules du mu-calcul.

Pour conclure, on démontre que le mu-calcul modal est le plus grand ensemble de formules de logique monadique du second ordre dont la sémantique est close par équivalence de bisimulation.