µ-Kalkül (Model Checking)

[Gast]

Hallo.

Die Fairness-Eigenschaft ("eine gewünschte Zustandsmenge wird unendlich oft erreicht") lässt sich mit dem µ-Kalkül wie folgt notieren

$\nu y.\diamond ( \mu x.(y \wedge \phi) \vee \diamond x )$

Dabei beschreibt Phi die gewünschte Zustandsmenge.
Die Interpretation dieser Formel über einer Kripke-Struktur K beinhaltet damit alle Zustände, auf denen ein unendlicher Pfad p (Abbildung von Natürlichen Zahlen in Zustandsmenge) startet mit
\forall t\_1. \exists t\_2. p(t\_1 + t\_2) \in [ \phi ]_K

Nun, ich habe allgemein Probleme, Formeln des µ-Kalküls schnell zu verstehen, ohne mir den Sinn irgendwie über die unanschauliche Definition (Fixpunktgleichung) erschließen zu müssen. Wenn mehrere Fixpunktoperatoren geschachtelt sind, verstehe ich es intuitiv kaum noch. Kann also nicht ganz nachvollziehen, warum obiger Ausdruck die Fairness-Eigenschaft beschreibt.

Wie geht man da am besten ran?
Ohne das zu verstehen, kann ich kaum selbst Formeln für bestimmte Eigenschaften aufstellen.

Die Formeln für persistence, safety und liveness habe ich verstanden. Die sind aber nicht derart verschachtelt wie Obige.

Gruss, space