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


538 users

0 votes
related to an answer for: compute R' from the following FSM
in * TF "Emb. Sys. and Rob." by (300 points)

1 Answer

+1 vote
s2 is a reachable state in the Kripke structure, the the state s2 in the FSM is not reachable.
by (166k points)
Is that so? s3 is {q,a} an initial state, and the self-loop of the FSM-state s1 {q} induces a transition to s2 {q}. As s2 {q} is a deadend, we delete it from the initial states. On the final graph, transition s3→s2 is no more
Yes, finally the transition s3->s2 is gone. But first, the state s2 exists and as an initial state, it is reachable by definition (since reachable states are mu x. (Init or <:>x) which includes the initial states). Hence, s2 of the Kripke structure is reachable. But we want to clean up the structure by removing all finite paths, and because of this, the state s2 is removed. It is a (reachable) deadend state.
Imprint | Privacy Policy