Mu-calcul

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

• si ${\displaystyle \phi }$ est une formule, alors ${\displaystyle \neg \phi }$ est une formule ;

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

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

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

• ${\displaystyle \phi \lor \psi }$ signifiant ${\displaystyle \neg (\neg \phi \land \neg \psi )}$ ;

• ${\displaystyle \langle a\rangle \phi }$ signifiant ${\displaystyle \neg [a]\neg \phi }$ (après ${\displaystyle a}$ il est possible que ${\displaystyle \phi }$) ;

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

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

La notation ${\displaystyle \mu Z.\phi }$ (et respectivement son dual ${\displaystyle \nu Z.\phi }$) 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 ${\displaystyle \phi }$ tout comme en lambda-calcul ${\displaystyle \lambda Z.\phi }$ est une fonction de la formule ${\displaystyle \phi }$ en la variable liée Z[4] ; voir la sémantique dénotationnelle plus bas pour plus de détails.

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

• ${\displaystyle S}$ est un ensemble d'états ;

• ${\displaystyle R}$ associe à chaque label ${\displaystyle a}$ une relation binaire sur ${\displaystyle S}$ ;

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

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

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

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

• ${\displaystyle [\![\phi \vee \psi ]\!]_{i}=[\![\phi ]\!]_{i}\cup [\![\psi ]\!]_{i}}$ ;
• ${\displaystyle [\![\langle a\rangle \phi ]\!]_{i}=\{s\in S\mid \exists t\in S,(s,t)\in R_{a}\wedge t\in [\![\phi ]\!]_{i}\}}$ ;
• ${\displaystyle [\![\mu Z.\phi ]\!]_{i}=\bigcap \{T\subseteq S\mid [\![\phi ]\!]_{i[Z:=T]}\subseteq T\}}$.

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

• ${\displaystyle p}$ est vraie pour les états ${\displaystyle V(p)}$ ;

• ${\displaystyle \phi \wedge \psi }$ est vraie si ${\displaystyle \phi }$ et ${\displaystyle \psi }$ sont vraies ;

• ${\displaystyle \neg \phi }$ est vraie si ${\displaystyle \phi }$ n'est pas vraie ;

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

• ${\displaystyle \langle a\rangle \phi }$ est vraie dans un état ${\displaystyle s}$ s'il existe au moins une transition ${\displaystyle a}$ sortant de ${\displaystyle s}$ qui mène à un état où ${\displaystyle \phi }$ est vraie ;

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

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

• ${\displaystyle \nu Z.\phi \wedge [a]Z}$ est interprétée comme « ${\displaystyle \phi }$ est vraie pour chaque chemin de a »[5].

• ${\displaystyle \mu Z.\phi \vee \langle a\rangle Z}$ est interprétée comme l'existence d'un chemin de transitions a vers un état dans lequel ${\displaystyle \phi }$ est vraie[6].

• 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 ${\displaystyle \nu Z.(\bigvee _{a\in A}\langle a\rangle \top \wedge \bigwedge _{a\in A}[a]Z)}$ [6].
• ${\displaystyle \mu Z.[a]Z}$ : tout chemin composé de a-transitions est fini[7].
• ${\displaystyle \nu Z.\langle a\rangle Z}$ : il existe un chemin infini composé de a-transitions[7].
• ${\displaystyle \nu Z.\phi \land \langle a\rangle Z}$ : il existe un chemin infini composé de a-transitions le long duquel ${\displaystyle \phi }$ est vraie tout le temps[7].

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[8] qui regarde aussi l'utilisation des variables. La hiérarchie d'alternation est stricte[9].

Le problème de model checking du mu-calcul est dans NP inter co-NP[1] 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[10].

Comme pour la logique temporelle linéaire (LTL)[11], 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[12].

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[13]. Il existe une version linéaire (non branchée) du mu-calcul[14] - [12].

• (en) Edmund M. Clarke, Jr., Orna Grumberg et Doron A. Peled, Model Checking, Cambridge, Massachusetts, USA, MIT press, 1999 (ISBN 0-262-03270-8), chapter 7, Model checking for the μ-calculus, pp. 97–108
• (en) Colin Stirling, Modal and Temporal Properties of Processes, New York, Berlin, Heidelberg, Springer Verlag, 2001, 191 p. (ISBN 0-387-98717-7, lire en ligne), chapter 5, Modal μ-calculus, pp. 103–128
• (en) André Arnold et Damian Niwiński, Rudiments of μ-Calculus, Elsevier,‎ 2001, 277 p. (ISBN 978-0-444-50620-7), 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.
• (en) Julian Bradfield et Colin Stirling, The Handbook of Modal Logic, Elsevier, 2006, 721–756 p. (lire en ligne), « Modal mu-calculi »
• (en) E. Allen Emerson « Model Checking and the Mu-calculus » (1996)
  — « (ibid.) », dans Descriptive Complexity and Finite Models, American Mathematical Society (ISBN 0-8218-0517-7), p. 185–214
• (en) Kozen, Dexter, « Results on the Propositional μ-Calculus », Theoretical Computer Science, vol. 27, n^o 3,‎ 1983, p. 333–354 (DOI 10.1016/0304-3975(82)90125-6)

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

• (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Modal μ-calculus » (voir la liste des auteurs).