Exercise  We consider words over the alphabet {a, b} as transition systems ⟨S, Es, Er, Pa, Pb⟩ where
the states S are the positions,the two predicates Pa and Pb label each position with the corresponding
letter, and the two edge relations are
Es = {⟨i, i + ⟩ i < n − } ,
Er = {⟨i, k⟩ i ≤ k < n } .
(where n = S is the length of the word). Define the following languages in modal logic.
(a) All words starting with the letter a.
(b) All words consisting only of letters a.
(c) All words ending with the letter a.
(d) a∗
b∗
(e) All words containing the factor bb.
(f) All words containing at least two letters b.
(g) All words containing exactly two letters b.
(h) (ab)∗
Exercise  Translate the following formulae into first-order logic.
(a) [a]P → P
(b) P → ⟨a⟩Q
(c) [a](P ∧ ⟨b⟩Q) → (⟨a⟩P ∨ ⟨b⟩Q)
Exercise  Prove the following modal formulae using tableaux.
(a) ¬ P → ♦♦¬P
(b) (P ∧ ¬P) → Q
(c) ¬♦P → (P → Q)
(d) (P ↔ (Q ∧ R)) → ( P ↔ ( Q ∧ R))
Prove the following entailment relationships using tableaux.
(a) φ → φ ⊧ φ → φ
(b) ∀xφ ⊧ ∀x φ

Exercise  Find CTL*-formulae defining the following properties of trees with a single predicate P.
Which of these statements can be expressed in CTL?
(a) There is at least one label P.
(b) Every path contains some P.
(c) Every path contains at least two P.
(d) All paths contain infinitely many P.
(e) Some path contains infinitely many P.
Exercise  Express the properties from Exercise  in the modal µ-calculus.
Exercise  We model an elevator in a building with  stories.
(a) Describe the elevator as a transition system.
(b) Write a specification for the elevator in modal logic and in LTL. Start with the following two
statements, then add your own.
(i) The elevator never moves when the door is open.
(ii) If the button on floor  is pressed, the elevator will eventually stop at that floor and open
the door.
Check that your system from (a) satisfies these formulae.
