# Exercise 11 PDR Method

Hello,

For exercise 11, I am using the tool to get the answer.

Consider the Kripke structure K={V,φI,φR}K={V,φI,φR}, where V=V={a,b,c}, φI=φI= !a&!c, and the following state transition diagram:

Check the safety properties S=S= b|c|!a holds or not by the Property Directed Reachability (PDR) method.
In the tool I am giving the following input

variables : a,b,c

Initial States : !a&!c

Transition Relation : !a&!b&!c|

a&!b&!c&!next(a)&!next(b)&next(c)|

!a&!b&c&next(a)&!next(b)&!next(c)|

b&!a&!c & next(a)&next(b)&!next(c)|

a&b&!c & next(a)&!next(b)&next(c)|

a&!b&c & !next(a)&next(b)&next(c)|

!a&b&c & next(a)&next(b)&next(c)|

a&b&c & !next(a)&next(b)&!next(c)

Safety Property Φ: b|c|!a

After checking, the tool computes the following

## INITIAL SETUP

• Checking Safety of Initial States (x) ➞ Φ(x):
All initial states satisfy the safety property, so there is no counterexample of length 1.
• Checking Safety of Successors of Initial States (x) ⋀ (x,x') ➞ Φ(x'):
State !a & !b & !c which is a successor state of initial state a & !b & !c violates Φ, so Φ is not valid.
• Checking Inductiveness of Initial States (x) ⋀ (x,x') ➞ (x'):
There are initial states have successor states that are not initial states. Hence, the reachable states have to be approximated by a sequence of assertions ψ[...].
• Checking Inductiveness of the Safety Property Φ(x) ⋀ (x,x') ➞ Φ(x'):
There safety property Φ is not inductive, so that we have to find inductive assertions ψ[...] proving Φ.

Summary: Initial checks were conclusive: there is no need to start the PDR loop.

Can some one tell how to interpret the output?

Thanks

Well, you must first read the chapter on induction, i.e. VRS-09-Induction before you are ready for this kind of exercise. In particular, you will find the PDR method on pages 98-100, but to understand that, you need the really many slides before (depending in which detail you want to understand it). It is impossible to summarize those 100 slides here in a few lines.

Looking at the exercise, the first thing I notice is that your transition relation is not correct. The generated transition system does not look like yours. Instead, the transition relation should be as follows:

     a&!b&!c & !next(a)&!next(b)& next(c) |
!a&!b& c &  next(a)&!next(b)&!next(c) |
!a& b&!c &  next(a)& next(b)&!next(c) |
a& b&!c &  next(a)&!next(b)& next(c) |
a&!b& c & !next(a)& next(b)& next(c) |
!a& b& c &  next(a)& next(b)& next(c) |
a& b& c & !next(a)& next(b)&!next(c)


and will give you the following Kripke structure:

Initial states are !a&!c, so that the reachable states are s0,s2,s3,s5,s6,s7, i.e., all states but s1 and s4. The safety property phi to be checked is b|c|!a which holds in all states except for s4 (these are the green states).

Hence, the property is not inductive, since there are states (namely s1) where phi holds but where some successor state does not satisfy phi.

Hence, we cannot prove this property by applying the simple induction rule even though all reachable states satisfy phi, and therefore AGphi holds on all initial states. Instead, we have to strengthen the induction property until we find a stronger property that is inductive. PDR does this automatically.

To this end, PDR starts as follows with the following initial checks:

(1) Check the Safety of Initial States I(x) ➞ Φ(x), i.e., check whether all initial states are included in the safety property. In our case, all initial states satisfy the safety property, so there is no counterexample of length 1.

(2) Check the Safety of the Successors of Initial States I(x) ⋀ R(x,x') ➞ Φ(x'), i.e., check whether all successor states of all initial states satisfy the safety property. In our case, all successors of initial states satisfy the safety property, so there is no counterexample of length 2.

(3) Check the Inductiveness of Initial States I(x) ⋀ R(x,x') ➞ I(x'), i.e., check whether all successor states of all initial states are also initial states. If that would be true, the initial states would be the reachable states. However, in our case that is not true, since we have a transition s2->s6 from the initial state s2 to a non-initial state s6.

(4) Check the Inductiveness of the Safety Property Φ(x) ⋀ R(x,x') ➞ Φ(x'), i.e., whether all successors of green states are green states. In our example, this is not the case, since we have for example, s1->s4 and while s1 satisfies the safety property, s4 does not. Hence, we don't get a cheap proof this way.

Hence, the initial checks were not conclusive, we can neither prove nor disprove the safety property with the simple checks (1)-(4) and therefore PDR has to start its work.

PDR will therefore check the counterexample to the induction step which is only the transition s1->s4. PDR will then find out that s1 is not reachable and will remove s1 from the green states. Checking inductiveness again will then work, and a proof is found with the stronger safety property {s0,s2,s3,s5,s6,s7} which can be expressed as ¬a&¬c ∨ b ∨ a∧c. This is inductive and it implies the given property.

For more details, you really have to study the chapter on induction, it is quite involved and cannot be summarized here in a few lines of text.

by (170k points)
Hello, thank you.
I went through the slides, and in order to check the answer I used the tool, because the answer which I got was incorrect.
I will go through the slides again and hopefully this time I understand better, and there is no mistake from my end.
Thank you again for the brief explanation.