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

1.1k questions

1.3k answers

1.7k comments

556 users

0 votes
In the task we are given S2 = EF(q & EG(p & !q)).

1.) Can this even be true at any time? And if so, how would a corresponding Kripke structure look like?

2.) Is there a difference to the formula EF(q & G(p & !q))? This formula cannot be satisfied, right? Because q & G (!q) would need to hold at the same time?
in * TF "Emb. Sys. and Rob." by (800 points)

1 Answer

+1 vote
 
Best answer

S2 = EF(q & EG(p & !q)) is indeed equivalent to S2 = EF(q & G(p & !q)) and these formulas cannot be satisfied, since as you wrote q contradicts G!q. 

by (170k points)
selected by
The example solution is correct, but it only explains that S2 does not hold on the discussed structure. Maybe you would like to read also that it does even not hold anywhere else and that therefore it is sufficient to construct a model for S1. Right, that is the case!

Related questions

0 votes
1 answer
asked Aug 21, 2020 in * TF "Emb. Sys. and Rob." by Nicola (800 points)
0 votes
1 answer
asked Feb 8, 2021 in * TF "Emb. Sys. and Rob." by dn (1.4k points)
0 votes
1 answer
asked Jan 26, 2021 in * TF "Emb. Sys. and Rob." by dn (1.4k points)
0 votes
1 answer
asked Jan 24, 2021 in * TF "Emb. Sys. and Rob." by dn (1.4k points)
0 votes
1 answer
asked Feb 6, 2021 in * TF "Emb. Sys. and Rob." by dn (1.4k points)
Imprint | Privacy Policy
...