IA169: Model Checking
Seminar 3
Exercise 1 Consider the following Kripke structure S with atomic propositions
p, q, r, s.
p
q
q
r
s
Which of the following CTL properties φ are satisfied by the system S, i.e.,
S |= φ.
1. EFq
2. AFq
3. AG(r → AFr)
4. AG(s → AFs)
5. AG(q → EXr)
6. AG(q → EXs)
7. AG(q → AXr)
8. AG(q → AXs)
9. AG(s → AX(A(¬qUs)))
10. AG(r → AX(A(¬qUr)))
Try to come up with some additional non-trivial properties that are satisfied
by the system S.
Exercise 2 CTL can be also used to specify properties of infinite trees with
labeled vertices. Write CTL formulas for the following properties of infinite
trees. Can all of them be expressed in CTL?
1. There is at least one vertex labeled by p.
2. Every path contains a vertex labeled by p.
3. There is a subtree whose all vertices are labeled by p.
4. Every path contains at least two vertices labeled by p.
5. All paths contain infinitely many vertices labeled by p.
ia169: model checking 2
6. At least one path contains infinitely many vertices labeled by p.
7. There is no path with a vertex labeled by q that is between two vertices
labeled by p. (Not necessarily neighboring.)
Exercise 3 If any of the previous properties is not expressible in CTL,
express it in CTL*.
Exercise 4 For each of the following CTL formulas φ, find a Kripke structure
S that satisfies it or explain why it does not exist.
1. AFp ∧ AG(p → AX¬p)
2. AFp ∧ AG(p → EX¬p)
3. AFp ∧ AG(p → (EXp ∧ EX¬p))
4. AFp ∧ AG(p → (AXp ∧ EX¬p))
5. EF¬p ∧ EF(AGp)
Exercise 5 Construct Binary Decision Diagrams (BDD) for the following
propositional formulas.
1. (A ∧ B) → C
2. (A ∧ B) ↔ C
3. (A ↔ C) ∧ (B ↔ D)