¬ ∧ ∨ ⊃ ≡ □ ◇ K_a E D C [α] ⟨α⟩ ; ∪ * ? ( ) [] is □, <> is ◇, K_a is agent a’s knowledge, [a;p?;b] is a program. Every modality binds tighter than ∧ ∨ ⊃ ≡