# Safety property, induction rule September 6, 2022, question 3e

Hi,

I need help solving September 6, 2022, question 3e. I have a problem understanding safety property and induction rules.

Regards,

Pavithra

Well, this is a very broad question whose precise answer covers the entire chapter on induction which is chapter 9 of the course with more than 150 pages.

Anyway, to given some basics: On page 6, it is defined that a safety property phi is a property that holds (at least) on all reachable states of a transition system. We can prove safety properties by means of the fixpoint iteration nu x. (phi & []x)) which will compute all states that satisfy phi so that we need to check finally that the initial states are inside of this set. Another alternative is to use local model checking, where we have to prove that every initial state satisfies AG phi. This has however the same worst case complexity and is difficult to be implemented in a symbolic manner.

An alternative is the proof by induction. To this end, we have to that the initial states satisfy phi, and that all successor states of states that satisfy phi also satisfy phi. If we can prove both the induction base and the induction step, the safety property definitely holds on all reachable states. However, the induction base may not be provable even though the property holds on all reachable states. Such a case is called a counterexample to induction, and many techniques discussed in chapter 9 show how to eliminate those to obtain a complete induction proof procedure like the PDR method that can automatically compute suitable induction lemmata (that can be proven by induction and that imply phi).

In the exam problem, it is asked whether the property AG(p->q) can be proved by induction on the mentioned transition system. The example solution explains that there is a counterexample to induction so that the property cannot be proved by the mentioned induction rule and needs a stronger induction lemma.

Bytheway, why do you post the title pages of the exam paper? They don't help much to understand your question.
by (166k points) 1 flag