0 votes

Hi,

I think the below solution is wrong or perhaps my understanding is not correct. All of the formulae is same except EGa and Ga, EGa, as far as I know, means that there must be one path which satisfies Ga. In the solution, there is a statement saying path looping in s2 satisfies S1. The path is a ,G b how does this satisfy E(Fb and EGa)? 

in * TF "Emb. Sys. and Rob." by (1.4k points)

1 Answer

+1 vote
 
Best answer

The solution is correct. 

Look, the formula E((F b) & EGa) can be rewritten to the equivalent formula (E F b)&(E G a) which is possible since EGa is a state formula and has to hold in the first state of the path that should satisfy (F b) & EGa for the entire formula E((F b) & EGa). However, the path that satisfies (F b) & EGa, and the path that satisfies Ga in EGa may not be the same. 

In the example, we have

    s0 |= E(F b & E G a)
    since s0s1 |= F b & E G a
    since s0s1 |= F b and s0s1 |= E G a
    since s0s1 |= F b and s0 |= E G a
    since s0s1 |= F b and s0s2 |= G a

However, 

    s0 |/= E(F b & G a)
    since neither s0s1 |= F b & G a nor s0s2 |= F b & G a
    since neither s0s1 |= F b  nor s0s2 |= G a

Clearly, I may continue to explain why the latter is the case, but I guess that you can agree from here. 

by (96.2k points)
selected by
Thanks Professor, why does a has to hold in s0? Isnt s0 already satisfies Fb and EGa ? Does EG a means that first state has to satisfy a?
We need "a" to hold in s0 to have s0 |= E G a, since the latter means that "a" always holds on a path starting (and including) s0.
Understood thanks alot

Related questions

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