Does AFa<->AFAFa hold?

Question

Hi, im having a hard time with the following AFa=AFAFa, does it hold ? I think it should hold because we can choose the future point to be the point where AFa holds.

Comments

I also sadly can not use the tools to check this.

Answer 1

AFa and AFAFa are equivalent. You can see that by looking at their fixpoint definition which yield AFa = µx.(a ⋁ []x)  and  AFAFa = µy.(µx.(a ⋁ []x) ⋁ []y)

It means that we start with the a states and a successively add universal predecessors until it stabilizes to get AFa, but then this set is closed with respect to universal predecessors, so adding some more with the other fixpoints will not change the set of states anymore.

Comments

Can we also eliminate nesting of the type EGEG to EG ? Or more generally things like AFGAFG to AFG ? I didn't see any rules of these types in the slides, and I find it very hard to reason about them.

---

Sure, since AFAFa = AFa implies by negating both sides EGEGb = EGb. For more general things, I would be more pessimistic since there must be some property of the fixpoint that we exploit here. What we do is increasing/decreasing same way in the two nested fixpoints, and as long as that is done, then yes, it should hold. Alternating fixpoints like EGFa are however not of that kind.

---

I see, thank you for your answer

---

Careful: AFG a and AFAG a are different.
(Same goes for already mentioned nested fixpoints like EGFa)

Answer 2

Treat it as two implications:

1. AF a → AFAF a? If the assumption holds, then on any path, we reach a after finite time. So AF a holds in the first step. Since the first step is on all paths that start from the first step, we satisfy AF AFa by definition.
2. AFAF a → AF a? If the assumption holds, then it just takes finite time on any path until we can pick any path from there on to satisfy a after finite time. Now we want to know whether AF a is satisfied. We answer that by uniting beginning of paths with infinite paths to new infinite paths. Sounds confusing but it isn't. In order to satisfy AF a, we need to only take finite time to see a on any path. Let's just take an arbitrary path. Let's call this path ro. From the assumption, we know that FAF a holds on this path. The outer F promised us that there is a place from which on AF a holds. So there is a place in the path ro from which on AF a is satisfied. One of the paths from this place on is the suffix of ro. We now know that this suffix satisfies F a. Hence, also ro satisfied F a.

Comments

Thank you, thinking of it this way helps.