Mu-calcul

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 Modèle:Lien 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é.

Syntaxe

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 $\varphi$ et $\psi$ sont des formules, alors $(\varphi \wedge \psi )$ est une formule ;

• si $\varphi$ est une formule, alors $\mathrm{\neg }\varphi$ est une formule ;

• si $\varphi$ est une formule et $a$ est une action, alors $[a]\varphi$ est une formule (c'est la formule : « après $a$, nécessairement $\varphi$ ») ;

• si $\varphi$ est une formule et $Z$ une variable, alors $\nu Z.\varphi$ est une formule à supposer que chaque occurrence de $Z$ dans $\varphi$ 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 $\nu$ qui est le seul opérateur liant une variable.

Avec les définitions ci-dessus, on peut rajouter comme sucre syntaxique :

• $\varphi \vee \psi$ signifiant $\mathrm{\neg }(\mathrm{\neg }\varphi \wedge \mathrm{\neg }\psi )$ ;

• $⟨a⟩\varphi$ signifiant $\mathrm{\neg }[a]\mathrm{\neg }\varphi$ (après $a$ il est possible que $\varphi$) ;

• $\mu Z.\varphi$ signifiant $\mathrm{\neg }\nu Z.\mathrm{\neg }\varphi [Z:=\mathrm{\neg }Z]$, où $\varphi [Z:=\mathrm{\neg }Z]$ signifie qu'on remplace $Z$ par $\mathrm{\neg }Z$ pour chaque occurrence libre de $Z$ dans $\varphi$.

Les deux premières formules sont familières du calcul des propositions et de la logique multimodale K.

La notation $\mu Z.\varphi$ (et respectivement son dual $\nu Z.\varphi$) est inspirée du lambda-calcul ; l'objectif est de noter le plus petit (respectivement le plus grand) point fixe en la variable Z de l'expression $\varphi$ tout comme en lambda-calcul $\lambda Z.\varphi$ est une fonction de la formule $\varphi$ en la variable liée Z ; voir la sémantique dénotationnelle plus bas pour plus de détails.

Sémantique dénotationnelle

Les modèles d'une formule mu-calcul (propositionnelle, modale) sont donnés comme des systèmes de transition d'états $(S,R,V)$ où :

• $S$ est un ensemble d'états ;

• $R$ associe à chaque label $a$ une relation binaire sur $S$ ;

• $V:P\to 2^S$ associe à chaque proposition $p\in P$ l'ensemble des états où la proposition est vraie.

Étant donné un système de transition $(S,R,V)$, une interprétation $i$ associe à toute variable $Z$ un sous-ensemble d'états $i(Z)$. On définit le sous-ensemble d'états $[[\underset{\_}{\varphi }]{]}_i$ par induction structurelle sur la formule $\varphi$ :

• $[[p]{]}_i=V(p)$ ;
• $[[Z]{]}_i=i(Z)$ ;
• $[[\varphi \wedge \psi ]{]}_i=[[\varphi ]{]}_i\cap [[\psi ]{]}_i$ ;
• $[[\mathrm{\neg }\varphi ]{]}_i=S\setminus [[\varphi ]{]}_i$;
• $[[[a]\varphi ]{]}_i=\{s\in S\mid \mathrm{\forall }t\in S,(s,t)\in R_a\to t\in [[\varphi ]{]}_i\}$ ;
• $[[\nu Z.\varphi ]{]}_i=\bigcup \{T\subseteq S\mid T\subseteq [[\varphi ]{]}_{i[Z:=T]}\}$, où $i[Z:=T]$ associe $Z$ à $T$ tout en préservant les associations de $i$ partout ailleurs.

Par dualité, l'interprétation des autres formules basiques est :

• $[[\varphi \vee \psi ]{]}_i=[[\varphi ]{]}_i\cup [[\psi ]{]}_i$ ;
• $[[⟨a⟩\varphi ]{]}_i=\{s\in S\mid \mathrm{\exists }t\in S,(s,t)\in R_a\wedge t\in [[\varphi ]{]}_i\}$ ;
• $[[\mu Z.\varphi ]{]}_i=\bigcap \{T\subseteq S\mid [[\varphi ]{]}_{i[Z:=T]}\subseteq T\}$.

De manière informelle, pour un système de transition $(S,R,V)$ :

• $p$ est vraie pour les états $V(p)$ ;

• $\varphi \wedge \psi$ est vraie si $\varphi$ et $\psi$ sont vraies ;

• $\mathrm{\neg }\varphi$ est vraie si $\varphi$ n'est pas vraie ;

• $[a]\varphi$ est vraie dans l'état $s$ si toutes les transitions $a$ sortants de $s$ mènent à un état où $\varphi$ est vraie ;

• $⟨a⟩\varphi$ est vraie dans un état $s$ s'il existe au moins une transition $a$ sortant de $s$ qui mène à un état où $\varphi$ est vraie ;

• $\nu Z.\varphi$ est vraie dans n'importe quel état de n'importe quel ensemble $T$ tel que, si la variable $Z$ est remplacée par $T$, alors $\varphi$ est vraie pour tout $T$ (du théorème de Knaster-Tarski, on déduit que $[[\nu Z.\varphi ]{]}_i$ est le plus grand point fixe de $[[\varphi ]{]}_{i[Z:=T]}$, et $[[\mu Z.\varphi ]{]}_i$ en est le plus petit).

L'interprétation de $[a]\varphi$ et $⟨a⟩\varphi$ est l'interprétation « classique » de la logique dynamique. De surcroît, $\mu$ peut être vu comme une propriété de vivacité (« quelque chose de bon intervient à un moment ») tandis que $\nu$ est vu comme une propriété de sûreté (« quelque chose de mauvais n'arrive jamais ») dans la classification informelle de Leslie Lamport.

Exemples

• $\nu Z.\varphi \wedge [a]Z$ est interprétée comme « $\varphi$ est vraie pour chaque chemin de a ».

• $\mu Z.\varphi \vee ⟨a⟩Z$ est interprétée comme l'existence d'un chemin de transitions a vers un état dans lequel $\varphi$ est vraie.

• La propriété d'un système d'être non bloquant, c'est-à-dire que de tout état accessible, il existe une transition sortante, peut être exprimée par la formule $\nu Z.(\underset{a\in A}{\bigvee }⟨a⟩\mathrm{\top }\wedge \underset{a\in A}{\bigwedge }[a]Z)$ .
• $\mu Z.[a]Z$ : tout chemin composé de a-transitions est fini.
• $\nu Z.⟨a⟩Z$ : il existe un chemin infini composé de a-transitions.
• $\nu Z.\varphi \wedge ⟨a⟩Z$ : il existe un chemin infini composé de a-transitions le long duquel $\varphi$ est vraie tout le temps.

Alternation

L'alternation de plus petits et plus grands points fixes s'appelle la profondeur d'alternation. On peut compter le nombre d'alternations mais généralement, on utilise une définition plus sophistiquée introduite par Damian Niwiński qui regarde aussi l'utilisation des variables. La hiérarchie d'alternation est stricte.

Problèmes algorithmiques

Le problème de model checking du mu-calcul est dans NP inter co-NP et est P-dur. Un algorithme pour le model checking du mu-calcul est le suivant :

• Construire un jeu de parité à partir du système de transitions et de la formule du mu-calcul à vérifier ;
• Résoudre le jeu de parité.

Le problème de satisfiabilité du mu-calcul est EXPTIME-complet.

Comme pour la logique temporelle linéaire (LTL), le problème de la vérification de modèles, de la satisfiabilité et de la validité du mu-calcul linéaire est PSPACE-complet.

Discussions

La syntaxe originale du mu-calcul était vectorielle. L'avantage de cette notation est qu'elle permet de partager les variables sur plusieurs sous-formules. Il existe une version linéaire (non branchée) du mu-calculModèle:,.

Bibliographie

• Modèle:Ouvrage, chapter 7, Model checking for the μ-calculus, pp. 97–108
• Modèle:Ouvrage, chapter 5, Modal μ-calculus, pp. 103–128
• Modèle:Ouvrage, chapter 6, The μ-calculus over powerset algebras, pp. 141–153 concerne le μ-calcul.
• Yde Venema (2008) Lectures on the Modal μ-calculus; a été présenté à la 18th European Summer School in Logic, Language and Information.
• Modèle:Ouvrage
• Modèle:Lien conférence
• Modèle:Article

Liens externes

• Sophie Pinchinat, Logic, Automata & Games video recording of a lecture at ANU Logic Summer School '09