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

538 users

0 votes


In the above question, initial state satisfies the property p->q, then how does it not hold on the Kripke structure?
Are there any generalized steps to see the induction base and induction step?

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

1 Answer

0 votes
Well, a state formula phi holds on a Kripke structure if and only it holds on all of its initial states. When we check whether a safety property AG phi holds on a Kripke structure, we therefore need to check whether AG phi holds in all of its initial states. This means that phi always holds on all infinite paths that start in one of the initial states.

To do this, we may check whether phi holds on all initial states, if not, then AG phi does also not hold in all initial states. If phi holds on all initial states, it may still be the case that AG phi does not hold in all initial states. Just think of a successor state of an initial state that violates phi. So, you were confused with the question whether phi or AG phi holds on all initial states.
by (166k points)

Related questions

0 votes
1 answer
0 votes
1 answer
asked Jan 25 in * TF "Emb. Sys. and Rob." by A (360 points)
0 votes
1 answer
asked Jan 25 in * TF "Emb. Sys. and Rob." by A (360 points)
0 votes
1 answer
0 votes
1 answer
Imprint | Privacy Policy
...