IA169: Model Checking
Seminar 1
Exercise 1 Let AP be a set of atomic propositions such that p, q, r ∈ AP.
For each of the following LTL formulas over the set of atomic propositions
AP, find at least two words w1, w2 ∈ (2AP(φ))ω that satisfy the formula and
at least two words w3, w4 ∈ (2AP(φ))ω that do not satisfy it. What is the
intuitive meaning of the formulas?
1. Gp ∧ Fq
2. F(p ∧ Xq)
3. G(p → Xq)
4. G(p → Fq)
5. G(p → Gq)
6. (¬p → Xq)Ur
Exercise 2 Write LTL formulas for the following properties
1. every state of the run that satisfies p also satisfies q
2. the run contains at least two states that satisfy p
3. the run contains infinitely many states that satisfy p
4. the run contains exactly two states that satisfy p
Exercise 3 Let us have two fish, Alice (A) and Bob (B). There is an aquarium
divided into two parts: left (L) and right (R). Both fish start on the
right side of the aquarium and repeat the following sequence of steps (at the
beginning they start moving independently): They move left, eat, and move
back right.
Write (or draw) a Kripke structure that corresponds to this system. What
are the atomic propositions?
Then formulate the following properties using LTL and decide whether
the system satisfies each property.
1. Whenever Alice eats, she is on the left.
2. Whenever Alice is on the left, she will eat eventually.
3. Whenever Alice eats, she will immediately go to the left.
4. Alice will not eat before Bob.
5. If Alice does not eat before Bob, she will never eat.
6. Alice and Bob will never be on the same side from some point.
ia169: model checking 2
7. Bob chases Alice until they both eat together.
Exercise 4 Design non-deterministic Buchi automata for languages of
words over alphabet Σ = {a, b, c} that:
1. contain infinitely many letters a
2. contain infinitely many letters a and b
3. contain finitely many letters a and b
4. each a is immediately followed by b
5. each a is (possibly not immediately) followed by b
Exercise 5 Consider again the model from Exercise 3, but now with only
one fish. Draw the Kripke structure and convert it to the corresponding
Buchi automaton.