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


543 users

0 votes

Exam : 15.02.2017 : Q 10 b and c : (

Q1. For computing deadend states I thought computing universal predecessor of the transition relation with false (state set) once is enough. But here this is in iteration with putting previous result as new state set and ORing the previous state set.  Does it mean that it is calculating the finally deadend states as well iteratively ?

Q2. Also same thing with reachable states. So what I understood is that it is calculating from initial states which other states are reachable. Is it right ?

Thanks in advance.

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

1 Answer

+1 vote
Best answer
The definition of deadend states is not clear in the literature. That's why in the VRS course, we distinguish between deadend and finally deadend states to make precise what we mean. However, that distinction has been only recently introduced, and was not there some years ago. At that time, "deadend state" has been derived from the context, i.e., temporal logics have trouble with finally deadend states, and also induction hast that problem. The computation shown above computes the finally deadend states, since the states that have no outgoing transition are clearly those that satisfy []false while the finally deadend states are those that satisfy A false.
by (166k points)
selected by
I got your point.
Thanks a lot for this explanation.
Imprint | Privacy Policy