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 CTL (en) 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 $ϕ$ et $ψ$ sont des formules, alors $(ϕ \land ψ)$ est une formule ;

si $ϕ$ est une formule, alors $\neg ϕ$ est une formule ;

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

si $ϕ$ est une formule et $Z$ une variable, alors $ν Z . ϕ$ est une formule à supposer que chaque occurrence de $Z$ 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.

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

$ϕ \lor ψ$ signifiant $\neg (\neg ϕ \land \neg ψ)$ ;

$⟨ a ⟩ ϕ$ signifiant $\neg [a] \neg ϕ$ (après $a$ il est possible que $ϕ$ ) ;

$μ Z . ϕ$ signifiant $\neg ν Z . \neg ϕ [Z := \neg Z]$ , où $ϕ [Z := \neg Z]$ signifie qu'on remplace $Z$ par $\neg Z$ pour chaque occurrence libre de $Z$ dans $ϕ$ .

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

La notation $μ Z . ϕ$ (et respectivement son dual $ν Z . ϕ$ ) 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 $ϕ$ tout comme en lambda-calcul $λ Z . ϕ$ est une fonction de la formule $ϕ$ 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 $[[\underline{ϕ}]]_{i}$ par induction structurelle sur la formule $ϕ$ :

$[[p]]_{i} = V (p)$ ;
$[[Z]]_{i} = i (Z)$ ;
$[[ϕ \land ψ]]_{i} = [[ϕ]]_{i} \cap [[ψ]]_{i}$ ;
$[[\neg ϕ]]_{i} = S ∖ [[ϕ]]_{i}$ ;
$[[[a] ϕ]]_{i} = {s \in S ∣ \forall t \in S, (s, t) \in R_{a} \to t \in [[ϕ]]_{i}}$ ;
$[[ν Z . ϕ]]_{i} = ⋃ {T \subseteq S ∣ T \subseteq [[ϕ]]_{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 :

$[[ϕ \lor ψ]]_{i} = [[ϕ]]_{i} \cup [[ψ]]_{i}$ ;
$[[⟨ a ⟩ ϕ]]_{i} = {s \in S ∣ \exists t \in S, (s, t) \in R_{a} \land t \in [[ϕ]]_{i}}$ ;
$[[μ Z . ϕ]]_{i} = ⋂ {T \subseteq S ∣ [[ϕ]]_{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)$ ;

$ϕ \land ψ$ est vraie si $ϕ$ et $ψ$ sont vraies ;

$\neg ϕ$ est vraie si $ϕ$ n'est pas vraie ;

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

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

$ν Z . ϕ$ 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 $ϕ$ est vraie pour tout $T$ (du théorème de Knaster-Tarski, on déduit que $[[ν Z . ϕ]]_{i}$ est le plus grand point fixe de $[[ϕ]]_{i [Z := T]}$ , et $[[μ Z . ϕ]]_{i}$ en est le plus petit).

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

Exemples

$ν Z . ϕ \land [a] Z$ est interprétée comme « $ϕ$ est vraie pour chaque chemin de a ».

$μ Z . ϕ \lor ⟨ a ⟩ Z$ est interprétée comme l'existence d'un chemin de transitions a vers un état dans lequel $ϕ$ 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 $ν Z . (\underset{a \in A}{⋁} ⟨ a ⟩ ⊤ \land \underset{a \in A}{⋀} [a] Z)$ .
$μ Z . [a] Z$ : tout chemin composé de a-transitions est fini.
$ν Z . ⟨ a ⟩ Z$ : il existe un chemin infini composé de a-transitions.
$ν Z . ϕ \land ⟨ a ⟩ Z$ : il existe un chemin infini composé de a-transitions le long duquel $ϕ$ 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-calcul^,.

Bibliographie

(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)

Liens externes

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

Notes et références

1 2 (en) Julian Bradfield et Igor Walukiewicz, « The mu-calculus and Model Checking », dans Handbook of Model Checking, Springer International Publishing, 2018 (ISBN 9783319105741, DOI 10.1007/978-3-319-10575-8_26, lire en ligne), p. 871–919
↑ André Arnold et Damian Niwiński, Rudiments of μ-Calculus, pp. viii-x et chapitre 6.
↑ André Arnold et Damian Niwiński, Rudiments of μ-Calculus, pp. viii-x et chapitre 4.
↑ André Arnold et Damian Niwiński, Rudiments of μ-Calculus, p. 14.
1 2 Julian Bradfield et Colin Stirling, The Handbook of Modal Logic, p. 731.
1 2 (en) Erich Grädel, Phokion G. Kolaitis, Leonid Libkin, Maarten Marx, Joel Spencer, Moshe Y. Vardi, Yde Venema et Scott Weinstein, Finite Model Theory and Its Applications, Springer, 2007, 437 p. (ISBN 978-3-540-00428-8, lire en ligne), p. 159.
1 2 3 « Cours sur le mu calcul au Labri ».
↑ (en) Damian Niwiński, « On fixed-point clones », Automata, Languages and Programming, Springer, Berlin, Heidelberg, lecture Notes in Computer Science,‎ 15 juillet 1986, p. 464–473 (ISBN 3540167617, DOI 10.1007/3-540-16761-7_96, lire en ligne, consulté le 12 mars 2018)
↑ (en) J. C. Bradfield, « The modal mu-calculus alternation hierarchy is strict », CONCUR '96: Concurrency Theory, Springer, Berlin, Heidelberg, lecture Notes in Computer Science,‎ 26 août 1996, p. 233–246 (ISBN 3540616047, DOI 10.1007/3-540-61604-7_58, lire en ligne, consulté le 12 mars 2018)
↑ (en) Klaus Schneider, Verification of reactive systems : formal methods and algorithms, Springer, 2004, 602 p. (ISBN 978-3-540-00296-3, lire en ligne), p. 521.
↑ (en) A. P. Sistla et E. M. Clarke, « The Complexity of Propositional Linear Temporal Logics », J. ACM, vol. 32, n^o 3,‎ 1^er juillet 1985, p. 733–749 (ISSN 0004-5411, DOI 10.1145/3828.3837, lire en ligne).
1 2 (en) M. Y. Vardi, « A Temporal Fixpoint Calculus », ACM, New York, NY, USA,‎ 1^er janvier 1988, p. 250–259 (ISBN 0897912527, DOI 10.1145/73560.73582, lire en ligne).
↑ Julian Bradfield et Igor Walukiewicz, The mu-calculus and model-checking (lire en ligne)
↑ Howard Barringer, Ruurd Kuiper et Amir Pnueli, « A really abstract concurrent model and its temporal logic », POPL 'x86 Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, ACM,‎ 1986, p. 173–183 (DOI 10.1145/512644.512660, lire en ligne, consulté le 12 mars 2018)

(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).

Portail de l'informatique théorique

[:2-1] 1 2 (en) Julian Bradfield et Igor Walukiewicz, « The mu-calculus and Model Checking », dans Handbook of Model Checking, Springer International Publishing, 2018 (ISBN 9783319105741, DOI 10.1007/978-3-319-10575-8_26, lire en ligne), p. 871–919

[2] André Arnold et Damian Niwiński, Rudiments of μ-Calculus, pp. viii-x et chapitre 6.

[3] André Arnold et Damian Niwiński, Rudiments of μ-Calculus, pp. viii-x et chapitre 4.

[4] André Arnold et Damian Niwiński, Rudiments of μ-Calculus, p. 14.

[Bradfield_and_Stirling,_p._731-5] 1 2 Julian Bradfield et Colin Stirling, The Handbook of Modal Logic, p. 731.

[GrädelKolaitis2007-6] 1 2 (en) Erich Grädel, Phokion G. Kolaitis, Leonid Libkin, Maarten Marx, Joel Spencer, Moshe Y. Vardi, Yde Venema et Scott Weinstein, Finite Model Theory and Its Applications, Springer, 2007, 437 p. (ISBN 978-3-540-00428-8, lire en ligne), p. 159.

[:0-7] 1 2 3 « Cours sur le mu calcul au Labri ».

[8] (en) Damian Niwiński, « On fixed-point clones », Automata, Languages and Programming, Springer, Berlin, Heidelberg, lecture Notes in Computer Science,‎ 15 juillet 1986, p. 464–473 (ISBN 3540167617, DOI 10.1007/3-540-16761-7_96, lire en ligne, consulté le 12 mars 2018)

[9] (en) J. C. Bradfield, « The modal mu-calculus alternation hierarchy is strict », CONCUR '96: Concurrency Theory, Springer, Berlin, Heidelberg, lecture Notes in Computer Science,‎ 26 août 1996, p. 233–246 (ISBN 3540616047, DOI 10.1007/3-540-61604-7_58, lire en ligne, consulté le 12 mars 2018)

[Schneider2004-10] (en) Klaus Schneider, Verification of reactive systems : formal methods and algorithms, Springer, 2004, 602 p. (ISBN 978-3-540-00296-3, lire en ligne), p. 521.

[11] (en) A. P. Sistla et E. M. Clarke, « The Complexity of Propositional Linear Temporal Logics », J. ACM, vol. 32, n^o 3,‎ 1^er juillet 1985, p. 733–749 (ISSN 0004-5411, DOI 10.1145/3828.3837, lire en ligne).

[:1-12] 1 2 (en) M. Y. Vardi, « A Temporal Fixpoint Calculus », ACM, New York, NY, USA,‎ 1^er janvier 1988, p. 250–259 (ISBN 0897912527, DOI 10.1145/73560.73582, lire en ligne).

[13] Julian Bradfield et Igor Walukiewicz, The mu-calculus and model-checking (lire en ligne)

[14] Howard Barringer, Ruurd Kuiper et Amir Pnueli, « A really abstract concurrent model and its temporal logic », POPL 'x86 Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, ACM,‎ 1986, p. 173–183 (DOI 10.1145/512644.512660, lire en ligne, consulté le 12 mars 2018)