Neue Frage

Conflict in Global Model Checking on Persistence and the definition

gefragt 2017-08-08 17:40:34 +0200

Dieser Post ist als Wiki-Post markiert

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

aktualisiert 2017-08-08 17:56:04 +0200

arsinux Gravatar-Bild

I gave this as an entry to Global Model Checking tool

vars a,b;
init 0,5,7;
labels 0:b; 1:; 2:a,b; 3:a; 4:b; 5:; 6:a,b; 7:a,b;
transitions 0->1; 1->3; 2->0; 2->1; 2->5; 3->4; 3->6; 4->6; 5->2; 5->6; 6->3; 6->7; 7->4;

and I wanted to check Persistence property(mu y.(nu x. (a & <>x) | <>y) ;) on it. The result says Property mu y:bool. (nu x:bool. (a & <> x) | <> y) holds in states {s0;s1;s2;s3;s4;s5;s6;s7} ⊇ {s0;s5;s7} = k.init. Hence, the structure satisfies the property., but it seems to me that the result is in a conflict with the definition of Persistence I know, which is "It is true in a state if, there is an infinite path from that state that phi sometimes holds and sometimes doesn't, but eventually it always holds". The conflict that I see is that it can go to a state like s4 which is outside of s3-s6 loop. So it doesn't seem to be "eventually it always holds".

bearbeiten retag Als beleidigend melden schließen löschen


Which model checking tool do you mean?

contradictioned ( 2017-08-08 19:49:06 +0200 )bearbeiten

The link Martin provided is correct but you have to omit the "html p tag" part from the url.

arsinux ( 2017-08-09 11:05:30 +0200 )bearbeiten

Ohlol. Askbot adds a p-tag to the URL if it is at the end of a comment. And I cannot edit the previous comment because someone already added a comment. Bug known but closed: mmh?!

Martin ( 2017-08-09 11:58:13 +0200 )bearbeiten

@Martin: Fixed it manually by addint a newline + fullstop. Maybe it is also already solved in a newer askbot version, however the Fachschaft currently doesn't invest energy in upgrading as there are discussions about a new platform that shall arrive soon^TM.

contradictioned ( 2017-08-09 15:04:05 +0200 )bearbeiten

2 Antworten


geantwortet 2017-08-09 11:30:16 +0200

PS Gravatar-Bild

aktualisiert 2017-08-09 12:06:22 +0200

The property that you consider is mu y. (nu x. (a & <>x) | <>y) that consists of two independent fixpoints. The inner one is nu x. (a & <>x) which is equivalent to EG a, i.e., it holds in all states that have an infinite path where always variable a holds. The outer fixpoint computes all states that can reach (EG a)-states by a finite path, so the entire formula is essentially the CTL formula EF EG a (ignoring the trouble with finite paths which is no problem in your example). It is also equivalent to EFGa and means that there is a persistent path, i.e., a path where from some time on always a holds.

Note that persistence is a path property and means that some property phi should hold after some finite time forever on a path. In LTL, this can be expressed as FGa. µ-calculus does not care about paths, but only expresses state properties. Here, we have to decide whether we want to state the existence of a persistent path or whether all paths are persistent.

The existence of a persistent path is expressed in CTL* as EFGphi which can be expressed in CTL als EF EG phi, and that is the formula you considered when replacing phi by a.

That all infinite paths are persistent is expressed in CTL* as AFG phi which cannot be expressed in CTL. Note that AF AG phi is different (see lecture slides). The negation of AFG phi is EGF¬phi that can be expressed in µ-calculus as nu y.(<> mu x.(y & !a | <>x)) with an alternation depth of two. Checking that formula is a bit harder, but again, none of the states of your transition system satisfy this one either.

You are wondering whether the states satisfying it really deserve to be called persistent in a. Note that the above formula only demands the existence of a persistent path, i.e., a path where from a certain point of time on, variable a always holds. That is indeed true in all states, since all states can reach the loop between s3 and s6 so that every state has such a persistent path.

To see the details of your example, look at the following computations:

Global model checking of EG a computes these states as follows:

step 0 : x = {s0;s1;s2;s3;s4;s5;s6;s7}
step 1 : x = {s2;s3;s6;s7}
step 2 : x = {s3;s6}
fixpoint reached!

Looking at the state transition system, this is true, since in all other states labeled with a, i.e., s2 and s7, even all of their successor states do not satisfy a.

If we call this formula phi, then the outer fixpoint of the given formula is now mu y.(phi|<>y) which holds in all states that have a possibly finite path leading to a phi-state, i.e., all states that can reach {s3;s6} with a finite path. Global model checking computes these states as follows:

step 0 : y = {}
step 1 : y = {s3;s6}
step 2 : y = {s1;s3;s4;s5;s6}
step 3 : y = {s0;s1;s2;s3;s4;s5;s6;s7}
fixpoint reached!

Hence, all states satisfy your formula.

Now consider AF AG a, where we compute AG a first. Since the structure has no deadend states, we clearly know that nu z.(<>z) holds in all states, so that we can consider the simplify formula nu y.(a & []y) instead of nu y. ((nu z.(<>z) -> a) & []y). These states are computed as follows

    step 0 : y = {s0;s1;s2;s3;s4;s5;s6;s7}
    step 1 : y = {s2;s3;s6;s7}
    step 2 : y = {s6}
    step 3 : y = {}
    fixpoint reached!

Since none of the states satisfy AG a (which we can easily see when looking at the transition system), we clearly conclude that also AF AG a holds in none of the states.

bearbeiten Als beleidigend melden löschen publish Link mehr

geantwortet 2017-08-09 11:48:10 +0200

As you quoted correctly, there persistence asks for the existence of an infinite path that has a step from which on a property is satisfied on all other steps. Where would persistence fail? It would fail states from where there is no such path. No such path means that on all infinite paths, the property is violated infinitely often.


Let's consider the Kripke structure you submitted. Let's find infinite paths satisfying the property $a$. The only adjacent states satisfying $a$ are $s_3, s_6, s_7$. The only infinite paths consisting entirely of states satisfying $a$ are made up from $s_3, s_6$ . This means that paths satisfying our persistence criterion have to stay infinitely long in this states. We are now looking for states from where there exists a path that does nonsense for a bit but then loops among those two until the end of time. This property is essentially just reachability: Whenever we can reach $s_3, s_6$, we can build a path to there and loop in $s_3, s_6$ forever.

Therefore, all states that from where $s_3, s_6$ is reachable are the ones from where there is a path that does whatever for an arbitrary finitely number of steps before looping in $s_3, s_6$ forever.

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-08 17:40:34 +0200

Gesehen: 73 mal

Letztes Update: Aug 09