IA169: Model Checking
Seminar 4
Exercise 1 Recall the definition of symbolic transition system (symbolically
represented Kripke structure) from the lecture.
Exercise 2 Let P be a safety property. Explain bounded model checking
algorithm for the property P and write the corresponding formula that needs
to be checked.
Exercise 3 Write a symbolic transition system and a property P that is Feel free to use fish in your transition
system.violated for bound k = 4, but is satisfied for all bounds k < 4. Check your
answers in nuXmv.
Exercise 4 Let P be a safety property. Explain k-induction algorithm for
the property P and write the corresponding formulas that need to be checked.
Exercise 5 Write a symbolic transition system S and a property P such
that
• S satisfies the property P, and
• P is inductive (1-inductive).
Check your answers in nuXmv.
Exercise 6 Write a symbolic transition system S and a property P such
that
• S satisfies the property P, but
• P is not inductive (1-inductive).
Check your answers in nuXmv.
Exercise 7 Write a symbolic transition system S and a property P such
that
• S satisfies the property P,
• P is 4-inductive, but
• P is not k-inductive for any k < 4.
Check your answers in nuXmv.
Exercise 8 Write a symbolic transition system S and a property P such
that
• S satisfies the property P,
• P is not k-inductive for any k.
You can check your answer in nuXmv, but you will probably fail. The
k-induction algorithm nuXmv uses simple path constraints and is thus
complete for finite systems.