# Doubt Regarding CTL* to CTL Conversion

Hi,

I have two questions,

• When is E[phi and Si] = E phi and E Si ? is it always the case?
• We want to convert !EF(!E[1 WU a] & Fa)  to a CTL, Steps are follows
•  A!F(!E[1 WU a] & Fa)
• AG(E[1 WU a] | !Fa)
• AGE[1 WU a] | AG !a
• AGE[1 WU a] | AG !a Now here we can see that both cannot be true at the same because we can further simplify it to AGEFa | AG !a. What should we do in such case? How do we choose what can be dropped from the solution?

+1 vote

For general path formulas p and q, E(p∧q) is not equivalent to Ep∧Eq. For example, if p=Fa and q=Fb, then E(Fa∧Fb) means that we have to have one path where a holds at some time ta and b holds at some time tb. However, EFa∧EFb means that we have a path where a holds at some time ta, and we have to have a path where b holds at some time tb. The two paths in the latter case may however be two different paths which is not allowed in the former case.

If q is a state formula, however, then it holds on a path iff it holds on the first state of the path. This first state is the same first state for all paths leaving the state. Hence, we have E(p∧q) in some state s if there is path leaving where p∧q holds on that path and that means that p holds on that path and q holds in s. That is the same as (Ep)∧q  and therefore E(p∧q) is equivalent in this case to (Ep)∧q.

Analogously, A(p∨q) is equivalent in this case to (Ap)∨q if q is a state formula.

Concerning your above transformation, the following are equivalent

• A!F(!E[1 WU a] & Fa)
• AG(E[1 WU a] | !Fa)
• AGA(E[1 WU a] | !Fa)
• AG(E[1 WU a] | A!Fa) (note here that E[1 WU a] is a state formula)
by (117k points)
selected by
Thanks I understood your first regarding transformation , the solution states that answer is AG(E[1 WU a]), is it equivalent to AG(E[1 WU a] | A!Fa) ?
The computation above does not yet end with a CTL formula. I stopped at the point where I wanted to show you the use of the special rule A(p∨q)=(Ap)∨q if q is a state formula. To finish, note Martin's hint that [1 WU a] is valid so that the entire formula is just true. The original problem in the exam was however not ¬EF(¬E[1 WU a] ∧ Fa), but ¬EF¬E([1 WU a] ∧ Fa), thus the second E was applied to the conjunction and not only to [1 WU a].
Understood! Thank you very much!
+1 vote
• In most cases, you can't distribute E over a conjunction. One formula is seeking for one path with two properties. The other formula is seeking for two paths satisfying two different properties.
• Are you sure its a WU? [1 WU a] is a tautology. [1 SU a] = [1 WU a]  Fa = Fa
by (25.2k points)
Thanks understood, Yes its WU its from exam 2015.07.28 Problem 9 phi 2.