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

I am getting confused. For showing property phi is inductive, 

we first take all the states that satisfy phi. Example here, {{p,a}, {p},{p,q,a},{p,q}}

then find universal predecessor of phi ({p,a}, {p},{p,q,a},{p,q}, {q,a})

then check if phi is subset of universal predecessor of phi. if yes then property is inductive else not.

But I don't understand why we are looking here for successors? I know the lemma where exsitential successors of Q1 is subset of Q2 (lecture 9- slide 12), but I really don't understand what is Q1 and Q2 referring to in this example. 

in * TF "Vis. and Sci. Comp." by (870 points)

1 Answer

0 votes
To prove the induction step, we have to show that all successor states of those states that satisfy Phi do also satisfy Phi. Hence, we have to prove that suc∃(Phi)⊂Phi. By the inductiveness lemma on slide 12 of the Induction Chapter, this is equivalent to Phi ⊂ pre∀(Phi) and that in turn is equivalent to Phi -> []Phi by the semantics of the modal operator [].

I know that this is not that straightforward and it confused me also a lot. Finally, I have proven those lemmata at the beginning of the Induction chapter, and that clarified these things for me. Otherwise, it is really confusing about predecessors and successors. At the end, it is not that difficult, once these lemmata are seen. The lemmata are however a bit more general than needed, but I wanted to see all what holds.
by (170k points)

Related questions

Imprint | Privacy Policy
...