Doubt Regarding CTL* to CTL Conversion

Question

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?

Answer 1

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)

Comments

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!

Answer 2

• 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

Comments

Thanks understood, Yes its WU its from exam 2015.07.28 Problem 9 phi 2.