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

if it's like without negation (G!a)^(G!b) to G(!a&!b) , will it work? I think we have a formula for Gphi1 & Gphi2 = G(phi1&phi2), if that's the case then will it work?

Also E((Fa) ^ (Fb)) means = EFa ^ EFb right ?

---

Yes, as I wrote, we have (G!a)^(G!b) = G(!a&!b), and you can add a single negation on both sides to obtain !((G!a)^(G!b)) = !(G(!a&!b)) but that is not what you want.

EFa & EFb means (EFa) & (EFb) which is not E(Fa & Fb), i.e., E((Fa)&(Fb))

---

EFa & EFb is already in CTL form I guess. Since starting from a path like E then followed by temporal operators. But the solution is given as
E((Fa) ^ (Fb)) =  EF(b ^ EFa) | EF(a ^ EFb) . Does that make any difference.?

---

Also EF(b ^ EFa) | EF(a ^ EFb) is a CTL formula, but E((Fa) ^ (Fb)) is not a CTL formula (even though it is equivalent).

---

But if I put E inside the brackets it will be EFa & EFb . Which is a CTL I guess?
EF(b ^ EFa) | EF(a ^ EFb) this one also E followed by F then expression..which is equivalent to EFa & EFb this Solution I guess ? Is it correct?

---

EFa & EFb is a CTL formuła, but this is not equivalent to E(Fa&Fb). The former would be satisfied by a structure that has a path where at some time a holds, and another path where at some time b holds, while the latter requires a path where both a and b must hold at some some (maybe not at the same point of time). Also EF(b ^ EFa) | EF(a ^ EFb) is not equivalent to  EFa & EFb, but it is equivalent to E(Fa&Fb). The formula EF(b ^ EFa) | EF(a ^ EFb) is satisfied in two ways: (1) there is a path where first b and later a holds, or (2) there is a path where first a and later b holds.

---

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