Translation between logics

Question

Hi,

I have doubt regarding translation between logics, 

[2023.02.15. VRS] 

E((Fa) ^ (Fb)) to CTL. What is the () bracket means here?

 E((Fa) ^ (Fb)) =  EF(b ^ EFa) | EF(a ^ EFb) is given as a solution. 

Can we convert Fa= !G!a and Fb= !G!b , then 

E((Fa) ^ (Fb)) = E((!G!a)^(!G!b)) = E(!G(!a&!b)) = E(F(a|b))= EF(a|b) . Will it work? If not could you please help me?  

Answer 1

If we write E((Fa) ^ (Fb)) without the outermost brackets, it will be E(Fa) ^ (Fb) which is just EFa ^ Fb and since that is another formula, we need to write the brackets.

Your solution is incorrect. It is true that you can use Fa=!G!a and Fb=!G!b, but you cannot reduce (!G!a)^(!G!b) to !G(!a&!b) while you could reduce (G!a)^(G!b) to G(!a&!b) but that is another formula.

Comments

Yeah..got it..so if I do E( Fa& Fb) to EFa &EFb which will be a right solution. Do we need to get exact same solution given in the paper or other solutions are taken in account?

---

No, that is not correct: E(Fa& Fb) is *NOT* equivalent to EFa &EFb. E(Fa& Fb) is  equivalent to EF(b ^ EFa) | EF(a ^ EFb). There may also be alternative solutions, of course.

---

E((Fa & Fb))  =
                      = EF(Fa & Fb)     used E = EF
                      = EF(EFa & EFb)  used E = EF,
I think this can be a valid CTL for this question. I have seen that we can use EF = E/F/EFE. Now as per my understanding , formula is starting from E then a temporal operator, which is again should mapped to a boolean formula which is started by State formula.

---

E is not equivalent to EF, please remove this from your cheat sheet. However EFEphi is equivalent to EF phi  so you can keep EFE = EF on your cheat sheet. Also, EF is not equivalent to F, so please remove that also. For CTL, you have to ensure that after each path quantifier, next comes a temporal operator, and right before a temporal operator, there is a path quantifier. Not every CTL* formula can be translated to CTL.

---

thanks for the clarification, i will remove from the cheat sheet