geantwortet
**
2017-08-09 11:30:16 +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.

Which model checking tool do you mean?

contradictioned ( 2017-08-08 19:49:06 +0200 )bearbeitenThis one: https://es.informatik.uni-kl.de/tools/teaching/ModelChecking.html .

Martin ( 2017-08-09 10:25:34 +0200 )bearbeitenThe 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 )bearbeitenOhlol. Askbot adds a p-tag to the URL if it is at the end of a comment. https://es.informatik.uni-kl.de/tools/teaching/ModelChecking.html And I cannot edit the previous comment because someone already added a comment. Bug known but closed: https://github.com/ASKBOT/askbot-devel/issues/190 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