IA169: Model Checking
Seminar 5
Exercise 1 Recall the definition of simulation between two Kripke structures
M = (SM, →M, SM
0 , LM) and N = (SN, →N, SN
0 , LN). Simulation relation between M and N
is written as M ≤ N and is read “N
simulates M”Exercise 2 Given the following Kripke structures Mi, decide for each pair
(Mi, Mj) such that i ̸= j whether Mi ≤ Mj holds. If it does, find the
simulation relation. If not, explain why.
p p
¬p p
p
Figure 1: M1
p p
¬p
p
Figure 2: M2
p
p
p
¬p p
p
Figure 3: M3
p p ¬p p ¬p
Figure 4: M4
Exercise 3 Briefly explain what is a predicate abstraction Mmay of a
labeled transition system M given a set of predicates P.
Exercise 4 Consider the labeled transition system M defined by the following
description in guarded command language
V = {x, y},
E = {(a, x = 0, x := x + 1),
(b, y = 0, y := y + 1),
(c, x > 0, (x := x + 3, y := y + 3))
ia169: model checking 2
and a set of predicates
P = {x > 0, x = y, y > 2}.
Compute the system Mmay that is the result of predicate abstraction of the
system M.
Exercise 5 Consider the labeled transition system M and the set of predicates
P from Exercise 4. The system satisfies the property G(|x − y| ≤ 1)
but the abstract system Mmay does not. Find a spurious counterexample.
Try to find a refiniment of P that blocks the spurious counterexample.
Exercise 6 Consider the labeled transition system M defined by the following
description in guarded command language
V = {x, y},
E = {(a, ⊤, y := y + 10),
(b, x mod 3 = 0, (x := x + 1, y := y + 3)),
(c, x mod 3 = 1, (x := x + 1, y := y + 4)),
(d, x mod 3 = 2, (x := x + 1, y := y − 6))}.
The system satisfies the property G(y ≥ 0). Find a finite set of predicates
P that reduces the system M to a finite-state system Mmay that also satisfies
the property.
Try to find as small P as possible.