Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.
In local model checking, we have to check for every s belongs to Initial states set.
So If there is two initial state in a Kripke structure namely s0 and s5, then lets say I start checking from s0 and it didn't satisfy, then we need to check again for s5 from starting as well.
Is there any strategy to choose initial state ? or we have to choose randomly and then check ?