Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.2k answers


546 users

0 votes

For 1) doesn't b need to be satisfied in s0 also?
For 2) Can you explain, how to interpret these two formulas(How they differ from each other)?
For 3) Will the solution drawn satisfy S1?
For 4) Does the solution satisfy S1?  

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

1 Answer

0 votes
(1) EFa holds in states s0,s1 due to the path s0->s1->s1->...; thus, label these states with a new variable "c" and consider E[c SU b] which holds in states s0,s2 due to the path s0->s2->s2->.... It is therefore not necessary that b should also hold in s0. If it would, then S1 would also hold in S0.

(2) AF(p|q) holds in a state if all infinite paths leaving that state reach a state where p|q holds. AFp holds in a state if all infinite paths leaving that state reach a state where p holds. Now, if you have a state that reaches states where p holds, but not q, and the other paths reach states where q holds, then you have AF(p|q), but you don't have (AFp)|(AFq).

(3) There is only one path where p&q holds at all even points of time, hence, GF(p&q) holds on that path, even in every position of that path. However, on that path, we also have GFp and GFq, so that the structure does not distinguish between the two formulas.

(4) There is only one path where always b holds. Since b implies [phi SU b], we also always have [a SU b], and therefore also G[a SU b] holds on that path. On the other hand, Ga does not hold, so that the solution is fine.
by (166k points)
Imprint | Privacy Policy