Translation between different logics

Question

Hello,

I have a doubt in converting the below formula in CTL.

¬AXX(GF(¬E[1 U (E¬a)]))

= ¬AXX(GF(¬E[1 U (¬a)]))

can we write [1 U (¬a)]  as F(!a) and then F(!a) as !a?

Thanks in advance.

Answer 1

Well, it depends: If the U is a strong-until, let's write SU for that, then we have [1 SU q] = (F q) since (F q) demands that at some point of time on a path, q holds, and [1 SU q] asks for the same (since the additional demand that 1 must hold until that point of time is trivially true).

However, you cannot write F(!a) as !a: The formula !a means that !a holds at the first point of time (and nothing is stated about any other point of time), and F(!a) means that !a holds at some point of time, which may be the first point of time, but also any other one. Hence, we have (!a) -> F(!a), but not the converse.

Comments

Okay got it, thank you so much.
One more question: So, if we have G(!a) then can we write as (!a)?.

Thanks in advance.

---

No, you cannot. G(!a) means that a is always false, i.e., false at all points of time while !a just means that a is false at the initial point of time.

---

Thank You very much!