Neue Frage

CTL to mu-calulus conversion

gefragt 2017-08-14 09:57:06 +0200

Dieser Post ist als Wiki-Post markiert

Das ist ein Wiki-Beitrag. Jeder mit Karma >75 darf diesen Beitrag verbessern.

aktualisiert 2017-08-14 11:02:21 +0200

How to know when to use mu.x and when to use nu.x while converting CTL to mu-calculus. I know that for mu.x we start with empty set and for nu.x we start with all the sets but still things are not that clear for me.

bearbeiten retag Als beleidigend melden schließen löschen

2 Antworten


geantwortet 2017-08-14 12:04:47 +0200

PS Gravatar-Bild

There is a simple rule that should help to remember in which cases you have to use $\mu$ or $\nu$ for the CTL operators: Use $\mu$ for the strong operators like strong-until etc. and use $\nu$ for the weak versions. Remember that the strong version implies the weak one (hence, is a subset of the satisfying behaviors) and that the least fixpoint specified by $\mu$ is a subset of the greatest fixpoint specified by $\nu$.

The strong temporal operators demand that some event will become true after finite time, and the least fixpoint operators also demand that the recursion has to terminate after finitey many steps. This essentially connects them and allows one to express the strong and weak CTL operators by least and greatest fixpoints, respectively.

For ALWAYS and EVENTUAL it is a bit more difficult since there is essentially only one version. Here, you may remember that you can express ALWAYS by a weak-until and EVENTUAL by a strong-until, and this should then also clarify which fixpoint operator to use in these cases ($\mu$ for EVENTUAL and $\nu$ for ALWAYS).

bearbeiten Als beleidigend melden löschen publish Link mehr

geantwortet 2017-08-14 11:42:44 +0200

Both $\mu x. f(x)$ and $\nu x. f(x)$ determined fixed points of $f$. These are values for $x$ with $f(x) = x$. There is a semantic difference between $\mu x$ and $\nu x$ once there are multiple fixed points: $\mu x. f(x)$ is the least fixed point and and $\nu x$ the greatest fixed point.

An example:

  • $\mu x. \phi \vee \diamond x$ liveness We start with the empty set, immediately get the states satisfying $\phi$ and add states from where $\phi$ is reachable in one steps, two steps … arbitrary many steps.
  • $\nu x. \phi \wedge \diamond x$ safety The first iteration yields the predecessors of any state (i.e. non-deadends) that satisfy $\phi$. Then, we look at predecessors for one step, two steps …infinitely many steps so that $\phi$ is still satisfied on every of these steps.
bearbeiten Als beleidigend melden löschen publish Link mehr

Ihre Antwort

Du kannst deinen Eintrag bereits als Gast verfassen. Deine Antwort wird zwischengespeichert, bis du dich eingeloggt oder registriert hast.
Bitte nur konstruktive Antworten auf diese konkrete Frage posten.
Falls du eine Frage stellen willst, dann stelle eine neue Frage.
Für kurze Diskussionen und Nachfragen benutze bitte die Kommentar-Funktion.
Deine Fragen und Antworten kannst du jederzeit nachbearbeiten und verbessern.
Gute Fragen und Antworten kannst du mit einem Upvote oder Downvote bewerten.

Schreibe deine Antwort auf diese Frage

[Vorschau ausblenden]


1 Follower


Gefragt: 2017-08-14 09:57:06 +0200

Gesehen: 93 mal

Letztes Update: Apr 06