Conversion to CTL

Question

Is this the correct conversion to CTL?

Answer 1

I think a solution is as follows

    !A(G X F b & F X b)
    = !A(X G F b & X F b)
    = !A X(G F b & F b)
    = !A X G F b
    = !A X A G A F b
    =  E X E F E G !b

Note that (G a) & a is equivalent to G a, and hence, GFb & Fb is equivalent to GFb.

    

Comments

I got your solution but I just want to know whether my approach is correct or not.

---

Your approach is also fine, sorry, I forgot to write that. The solution I wrote above is very similar to yours (in fact it is just the dual). You made use of the fact that (F a) | a is equivalent to a.

---

Hello @KS. I had a small doubt regarding how we consider (Fa) | a, looking at how the author used it to solve the translation.

1. Based on the problem, is it okay to either consider (Fa) | a = Fa or (Fa) | a = a?.

2. If it does work, would the same rule hold for (Ga) | a?. Kindly request some help to clarify this.

---

(Fa) | a is NOT equivalent to a, just consider the case where a does not hold at t=0, but at t=1, then Fa holds at t=0, but a does not. However, (Fa) | a is equivalent to Fa.

(Ga)|a is equivalent to a, but not equivalent to Ga, just consider the case where a holds at t=0 and is false for t>0.

---

Thank you for the explanation. The concept is now clear in terms of Fa with a. However, you quoted to the author's solution, i.e., "You made use of the fact that (F a) | a is equivalent to a.".

I'm a bit confused again. Are there any exceptions that exist in the author's solution, where (F a) | a is equivalent to a?

I humbly request you to clarify this, as it would help discard the contradiction in my understanding.

---

Sorry, I see that I wrote in a comment above that (F a) | a is equivalent to a, which is not true. It is as I wrote later that (F a) | a is equivalent to Fa. You can also quickly check this using https://es.cs.uni-kl.de/tools/teaching/TemporalLogicProver.html.

---

Thankyou. The clarification helps a lot.