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

1.6k comments

531 users

0 votes

I do not get why the answer for <:> is {}. Because S1 and S5 have already {} predecessor satisfying phi. (last line)

in * TF "Emb. Sys. and Rob." by (200 points)
retagged by
Please use the tag VRS.

1 Answer

0 votes
In general, <:> phi holds in a state if that state has a predecessor state which satisfies phi. Having computed the states S where phi holds, you can compute the states that satisfy <:>phi as suc∃(S).

Hence, if S={} holds, we have to compute suc∃({}) which means the set of states having at least one successor which is in {}. Since no state could be in {}, this is {}.
by (166k points)

Related questions

0 votes
2 answers
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
asked Aug 14, 2020 in * TF "Emb. Sys. and Rob." by maherin (370 points)
Imprint | Privacy Policy
...