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 � (a) We encode a game graph ⟨V♦, V , E⟩ as a transition system ⟨S, E, P♦, P ⟩ where S =
V♦ ∪V , P♦ = V♦,and P = V . Write a µ-calculus formula stating that the given position is winning
for Player ♦.
(b) (hard)We encode a boolean circuit as a transition system ⟨S, E, P∧, P∨, P¬, P, P⟩ where P∧, P∨,
and P¬ label the three kinds of logic gates, P and P label the input gates with the corresponding input
values, and the output gate is the initial state. Write a µ-calculus formula saying that the output of the
circuit is .
�