Une extension à points fixes de la logique modale qui ajoute des opérateurs de point fixe le plus petit (μ) et le plus grand (ν) pour exprimer des propriétés inductives et coinductives des systèmes de transition, permettant de spécifier des comportements récursifs et des propriétés régulières de trajectoires.

Principe

Utiliser μ pour définir des propriétés par induction en nombre fini d'étapes (points fixes minimaux) et ν pour définir des invariants coinductifs (points fixes maximaux) ; l'alternance de μ et ν contrôle l'expressivité et correspond à la complexité en vérification de modèles et aux traductions en automates.

Démonstration

Exprimer «sur chaque chemin, finalement toujours p» ou l'ensemble des états pouvant atteindre un état p via un motif répétitif au moyen d'une formule μ/ν sur une structure de Kripke ; la profondeur d'alternance se corrèle avec la complexité de l'automate de parité correspondant.

Mauvaise application

Encoder des propriétés non bien-fondées ou d'ordre supérieur sans respecter la sémantique des points fixes, ou ignorer la profondeur d'alternance et sous-estimer ainsi la complexité de la vérification de modèles et les contraintes de décidabilité.

Conséquence

Fournit un langage de spécification très expressif mais bien compris pour la vérification de programmes et la vérification de modèles : de nombreuses propriétés régulières des systèmes de transition sont définissables, et satisfiabilité et model-checking disposent de procédures décisionnelles liées à la théorie des automates.

Inversion

La logique modale ordinaire, sans opérateurs de point fixe, ne peut pas exprimer de nombreuses propriétés récursives ou de clôture transitive ; l'inversion supprime l'expressivité inductive/coinductive et simplifie la complexité mais perd la capacité à définir de nombreuses propriétés temporelles.

Limite

S'applique aux systèmes de transition étiquetés, structures de Kripke et modèles d'états similaires ; sa sémantique standard présuppose des constructions syntaxiques de points fixes bien fondées et ne capture pas directement des propriétés d'ordre supérieur arbitraire ou de pleine logique du premier ordre sans encodage.

Tension sémantique

Tension entre expressivité (capacité à définir des propriétés récursives complexes) et coût algorithmique (profondeur d'alternance, explosion d'états, taille de l'automate de parité) ; également entre localité modale et effets globaux des points fixes sur les modèles.

Synthèse

Le calcul μ modal intègre modalités et points fixes minimaux/maximaux pour former un cadre compact et expressif de spécification et vérification de comportements récursifs sur systèmes de transition, dont l'expressivité et la complexité sont governées par l'alternance des points fixes.