CTL * et mu-calcul

il est bien connu que le modal -calculus $\mu$ est l'une des logiques temporelles les plus expressives pour exprimer les propriétés des arbres / graphiques, et que CTL * est strictement moins expressif que le -calculus. $\mu$

Ici, je voudrais demander un exemple de formule -calculus, aussi simple que possible, qui ne soit pas exprimable dans CTL *, et j'espère une explication de sa signification (les formules à virgule fixe deviennent rapidement illisibles). Toute bonne référence pour un exemple simple "concret" serait aussi géniale! $\mu$

Merci d'avance

lo.logic model-checking temporal-logic mu-calculus LORE81
la source

Réponses:

Prenez une propriété de chemin qui n'est pas exprimable au premier ordre, par exemple qui dit qu'il existe un chemin où la proposition atomique tient à chaque position paire, et toute évaluation peut être utilisée sur des positions impaires.

ν x . p \land ◊ ◊ x

$\nu x.p\wedge\Diamond\Diamond x$

p

$p$

Sylvain
la source

merci beaucoup pour cette réponse simple. Pourriez-vous également suggérer une référence soutenant cet exemple? Merci encore

LORE81

Belle question et réponse (+2). Jetez un œil à cstheory.stackexchange.com/q/16186/6424 . J'ai également donné l'exemple de l'uniformité. Peut-être qu'une réponse fera également référence à la régularité.

DaveBall aka user750378

@ LORE81: l'exemple ``

aux positions paires '' est un classique, que vous pouvez retrouver par exemple dans l'article de Wolper pointé par @DaveBall dans sa question. Il n'est pas trop difficile de prouver directement par induction sur des formules LTL; alternativement, vous pouvez construire le monoïde de transition et voir qu'il n'est pas apériodique; enfin, vous pouvez essayer un argument Ehrenfeucht-Fraïssé, bien qu'il soit long à expliquer en détail.

p

$p$

Sylvain