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



In the above solution, why didn't we solve for initial state s1 as well. For local model checking, we need to solve for all the initial states right?

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

1 Answer

0 votes
Yes, a property holds on a Kripke structure if the property holds on all initial states of that structure. As it does not hold on the one state used in the local model checking tree, we already know that it does not hold for the structure and there is no need to check for the other initial states.
by (166k points)
Imprint | Privacy Policy
...