Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Mu-calcul
Résumé
En logique mathématique et en informatique théorique, le mu-calcul (ou logique du mu-calcul modal) est l'extension de la logique modale classique avec des opérateurs de points fixes. Selon Bradfield et Walukiewicz, le mu-calcul est une des logiques les plus importantes pour la vérification de modèles ; elle est expressive tout en ayant de bonnes propriétés algorithmiques.
Le mu-calcul (propositionnel et modal) a d'abord été introduit par Dana Scott et Jaco de Bakker puis a été étendu dans sa version moderne par Dexter Kozen. Cette logique permet de décrire les propriétés des systèmes de transition d'états et de les vérifier. De nombreuses logiques temporelles (telles que CTL* ou ses fragments très usités comme ou LTL) sont des fragments du mu-calcul.
Une manière algébrique de voir le mu-calcul est de le considérer comme une algèbre de fonctions monotones sur un treillis complet, les opérateurs étant une composition fonctionnelle plus des points fixes ; de ce point de vue, le mu-calcul agit sur le treillis de l'algèbre des ensembles. La sémantique des jeux du mu-calcul est liée aux jeux à deux joueurs à information parfaite, notamment les jeux de parité.
Soient deux ensembles de symbole P (les propositions) et A (les actions) et V un ensemble énumérable infini de variables. L'ensemble des formules du mu-calcul (propositionnel et modal) est défini inductivement de la façon suivante :
chaque proposition est une formule ;
chaque variable est une formule ;
si et sont des formules, alors est une formule ;
si est une formule, alors est une formule ;
si est une formule et est une action, alors est une formule (c'est la formule : « après , nécessairement ») ;
si est une formule et une variable, alors est une formule à supposer que chaque occurrence de dans apparaît positivement, c'est-à-dire qu'elle est niée un nombre pair de fois.
Les notions de variables liées ou libres sont définies comme d'ordinaire avec qui est le seul opérateur liant une variable.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.