Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.3k answers

1.7k comments

556 users

0 votes
If we are asked to perform a local model checking on a state transition diagram and it has more than 1 initial state and in the paper, an initial state is not specified. are we supposed to perform local model checking for ALL initial states?

Does that mean we will have as many trees as the number of initial states and all my satisfy to prove local model checking holds?
in * TF "Emb. Sys. and Rob." by (200 points)

1 Answer

0 votes
Yes, that is the case. For checking whether a structure satisfies a property, we need to make sure that ALL initial states satisfy the property. However, the proof trees of the initial states may have significant overlaps, but we need one proof tree per initial state.
by (170k points)
Imprint | Privacy Policy
...