Translation between logic

Question

I have doubt regarding this following slide, 

AF( phi1 & Xphi2) is it a valid CTL? Since the Xphi2 is not starting with either A or E or just a variable or boolean values ?

AF(phi1 & AXphi2) is a valid CTL (using X= AX) . 

Could you please help on this?

Also another doubt,

Fa & b = b = b & Fa 

Fa | b = Fa  = b | Fa

Are they valid? 

Since , E(Fa & Fb) = E( [1 SU a] & [1 SU b]) = E(1&1 SU (a&[1 SU b] | b&[1 SU a])) =    E(1 SU (a&[1 SU b] | b&[1 SU a])) = E(1 SU (a&Fb | b&Fa)) = E(F((a&Fb | b&Fa)) = 

EF(a|b) , will it work?

Answer 1

AF(phi1 & Xphi2) is not a CTL formula (regardless whether valid or not), since CTL formulas are defined as those CTL* formulas where a temporal operator occurs right after a path quantifier and where after each path quantifier there is a temporal operator. There is however no path quantifier in front of the X operator since there is a conjunction, so it is not a CTL formula. Even worse: AF(phi1 & Xphi2) is not equivalent to any CTL formula!

AF(phi1 & AX phi2) is a CTL formula provided that phi1 and phi2 are CTL formulas.

However, X=AX is not correct, please remove this from your cheat sheet. 

The point is that AF(phi1 & AX phi2) and AF(phi1 & X phi2) are not equivalent. The formulas look very similar, but are not the same. If you continue reading the slides, you will find on page 38 a Kripke structure that satisfies one of the formulas, but not the other one.

Fa & b = b & Fa is certainly valid since conjunction is commutative, and since disjunction is also commutative, also Fa | b = b | Fa is valid.

However, Fa | b = Fa is not valid, and neither is Fa & b = b. You can find easily counterexamples with the LTL teaching tool.

Comments

Thanks, I will those stuffs from the cheat sheet.