0 votes

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?
in * TF "Emb. Sys. and Rob." by (1.4k points)

2 Answers

+1 vote
 
Best answer

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 (93k 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 (24.7k points)
Thanks understood, Yes its WU its from exam 2015.07.28 Problem 9 phi 2.

Related questions

0 votes
2 answers
0 votes
1 answer
asked Jan 27, 2021 in * TF "Emb. Sys. and Rob." by dn (1.4k points)
0 votes
1 answer
asked Feb 14, 2021 in * TF "Emb. Sys. and Rob." by daodubasit (790 points)
0 votes
1 answer
asked Feb 12, 2021 in * TF "Emb. Sys. and Rob." by daodubasit (790 points)
Imprint | Privacy Policy
...