Pourquoi utiliser

9

On sait que les logiques temporelles LTL, CTL, CTL * peuvent être traduites / intégrées dans le μ-calcul. En d'autres termes, le (modal)μ-calculus subsume ces logiques, (c'est-à-dire qu'il est plus expressif.)

Pourriez-vous s'il vous plaît m'expliquer / pointer vers des articles / livres qui développent cette question. En particulier, y a-t-il des propriétés concrètes d'équité, de vivacité, etc. non exprimables dans les logiques temporelles mais dans lesμ-calcul?

Dimiter
la source

Réponses:

8

Quant à un μformule -calcul non exprimable en CTL *, voir cet article .

En ce qui concerne les textes sur le sujet, vous êtes susceptible d'aller plus loin en lisant des articles, car ces sujets ne sont pas abordés dans de nombreux livres. Pourtant, le Manuel de la logique modale peut être un bon début.

Quant aux papiers, essayez:

Puissance expressive de la logique temporelle

Cette thèse de doctorat

Vérification du modèle d'Emerson et calcul Mu

Et il y en a bien d'autres. Juste des termes google comme "puissance expressive", "calcul mu" et "logiques temporelles".

Shaull
la source
Merci pour l'exemple et les suggestions. Pourriez-vous s'il vous plaît suggérer des articles pertinents? Je me souviens en avoir vu dans le passé mais j'ai du mal à les localiser maintenant ...
Dimiter
Ajout de documents à la réponse.
Shaull
Il existe maintenant un livre sur la modélisation avec mCRL2 (pour une idée approximative de son contenu, voir l'annonce du livre ).
reinierpost
4

le μ-calcul est strictement plus expressif que LTL, CTL et CTL *. Ceci est la conséquence de quelques résultats différents.

La première étape consiste à montrer que μ-calcul est aussi expressif que les logiques temporelles. L'idée principale pour coder ces logiques vient de la reconnaissance des propriétés temporelles comme des points fixes. À un niveau très informel, les points les moins fixes vous permettent d'exprimer des propriétés de nature finitaire et les plus grands points fixes s'appliquent aux propriétés infinitaires. Par exemple, finalementφ en LTL définit qu'il y a un instant dans un avenir fini où φest vrai, bien que toujoursφ stipule que φest vrai à un nombre infini de futurs pas de temps. En termes de points fixes, la propriété finale serait exprimée en utilisant un point le moins fixe et la propriété toujours en utilisant un point fixe le plus grand. Suivant une telle intuition, les opérateurs temporels peuvent être encodés en opérateurs à point fixe.

L'étape suivante consiste à montrer que le μ-calcul est plus expressif. L'idée principale est la profondeur d'alternance. Les points fixes alternent si un point le moins fixe influence le plus grand point fixe, et vice-versa. La profondeur d'alternance d'unμ-la formule de calcul compte le nombre d'alternances qui s'y produisent. Les opérateurs dans CTL peuvent être codés parμ-calculus avec profondeur d'alternance 1. Les opérateurs dans CTL * et LTL peuvent être codés parμ-calculus avec profondeur d'alternance au maximum 2. Cependant, la hiérarchie d'alternance desμ-calcul est strict, ce qui signifie que l'augmentation de la profondeur d'alternance dans une formule vous permet d'exprimer strictement plus de propriétés. C’est pourquoi les gens disent queμ-calcul est plus expressif que ces logiques temporelles.

Quelques références:

  1. Les arguments initiaux que le μ-calculus subsume plusieurs logiques apparaît dans Modality for Model Checking: Branching Time Logic Strikes Back , Emerson et Lei, 1985.
  2. La traduction de CTL dans le μ-calcul est simple. Vous pouvez le trouver dans le livre sur la vérification des modèles de Clarke, Grumberg et Peled. Vous pouvez également le trouver dans Model Checking et lemu-calculus par Emerson ou dans la thèse de Ken McMillan.
  3. La traduction de CTL * dans le μ-calcul est impliqué. Plutôt que la traduction originale et indirecte, je suggère l'article de Mads Dam sur la traduction de CTL * dans le mu-calcul modal .
  4. Il y a une traduction plus simple de LTL dans ce qu'on appelle le temps linéaire μ-calcul, dans lequel les modalités opèrent sur des traces et non des états. Voir Axiomatising Linear Time Mu-calcul de Roope Kaivola.
  5. La hiérarchie d'alternance est étudiée dans La hiérarchie d'alternance mu-calcul modal est stricte par Julian Bradfield et dans Un théorème de hiérarchie pour leμ-calcul de Giacomo Lenzi.

Tout cela concerne l'expressivité et non l'utilité. En pratique, les gens ne spécifient généralement pas les propriétés commeμ-expressions de calcul car elles pourraient trouver les logiques temporelles plus faciles à utiliser. Les langages de spécification industrielle diffèrent à la fois des logiques temporelles et desμ-calcul dans leur syntaxe et leur pouvoir expressif.

Vijay D
la source
Merci pour une excellente réponse! En ce qui concerne votre commentaire sur l'utilité: supposons que je veuille utiliser un vérificateur de modèle μ-calcul, mais spécifiez les choses dans des logiques temporelles, ce qui est plus facile. Existe-t-il une technique (encore mieux, un outil) qui traduit automatiquement les formules de l'une de ces logiques (CTL, CTL * ou LTL) en μ-calcul? Merci!
Dimiter
SMV traduit en interne CTL en μ-calcul. Je ne sais pas quel outil le fait explicitement.
Vijay D
2

Il est bien connu que μ-calculi peut exprimer des propriétés qui "comptent modulo une constante", par exemple, " toutes les étapes paires visitent unUNE-state "qui est capturé par quelque chose commeμX.UNEX. De telles propriétés ne peuvent pas être déclarées avec les modalités TL standard Jusqu'à et Suivant car ces modalités sont définissables au premier ordre. Voir l'article de DC Kozen en 1983 .

phs
la source