[DOUBT] Translation of Logic to CTL

Question

Hello!. I am trying to solve this logic translation to CTL, as given in the solutions of the paper, dated 2021.02.17. 

In the 2nd step, F[d U b] was converted to FGd | Fb. But in the next step, AGd is written with a note at the bottom. Could anyone please explain how the reduction took place from step 2 to 3.?.

Answer 1

The claim is that (Gd & (FGd | Fb)) is equivalent to Gd. To see this, note first that Gd implies FGd since Gd demands that always d holds, and hence, it then holds also after any other point of time forever. Now, abbreviate p:=Gd, q:=FGd and r:=Fb and note finally that the following propositional logic formula is valid:

(p->q) -> (p & (q | r) <-> p)

Comments

Thank you for the explanation. I get the idea now.

Just to confirm my understanding, would it be true if there is a formula in the given format: Gd & (FGd | <any path formula or state formula>), for example:

Gd & (FGd | GFa) or Gd & (FGd | [d U b])

The rule of (p->q) -> (p & (q | r) <-> p) would still apply?

---

Yes, it does still apply. As you wrote above the second formula in the disjunction can be any formula.

---

Thanks for the clarification.