# Doubt in mu-calculus

In Feb 2022 exam, for problem 8e (Translate the following formula to an equivalent µ-calculus formula), is the above solution correct?

Your computation is almost fine! The difficult parts are fine, but there is a flaw in your computation.

First of all, consider G[a WB b] which holds if at any point of time t, "a" holds before "b" or G!b holds at time t. If G!b should not hold at time t, then !G!b holds, i.e., F b holds at time t, and therefore there is a point of time t+d where b holds. At that point of time t+d, it is however not possible that [a WB b] holds, and therefore, it is not possible that G!b does not hold at some time t. Thus, G!b must always hold so that G[a WB b] is equivalent to G!b.

In particular, G[a WB F X b] is therefore equivalent to G !F X b. Good that you have seen this, since this simplifies matters. Because of this, we then get

```    A G[a WB F X b]
= A G !F X b
= A G !X F b
= A G !F X b
= A G G X !b
= A G X !b
= A G A X !b
```

and since that is CTL, it is not difficult to get a µ-calculus formula from here.

However, G !X F b is not equivalent to G !F b. Note that G !X F b is equivalent to GX!b (as explained above), while  G !F b is equivalent to GG!b which is equivalent in turn to G!b. However, GX!b holds if b is initially true and then always false, which does not satisfy G!b.

by (170k points)