Show description

Temporal structures for LTL can be understood as a special case of Kripke structures where K = N and, for i, j ∈ N, i ✁◦ j ⇔ i + 1 = j , i ✁✷ j ⇔ i ≤ j . Taking these definitions in clause 4 above (with ✁◦ and ✁✷ , respectively) we indeed get back the LTL definitions for Ki ( ❝A) and Ki (✷A). As long as no restrictions are put on the relation ✁ ⊆ K × K , modal logic can be axiomatized by a sound and complete formal system with the axioms • • all tautologically valid formulas (defined as in LTL), ✷(A → B ) → (✷A → ✷B ) and the rules • • A, A → B A ✷A.

Let us illustrate this idea with a little example. Suppose A ≡ (v1 → v2 ) → ✷v3 , B ≡ v3 → ❡v2 (with v1 , v2 , v3 ∈ V), and P = ({A}, {B }). One possible completion of P is P ∗ = ({A, v1 → v2 , ✷v3 , v2 , v3 }, {B , v1 , ❡v2 }). If all the (proper) parts of A and B in pos(P ∗ ) evaluate to tt and those in neg(P ∗ ) to ff then A becomes tt and B becomes ff and, moreover, such a valuation is in fact possible because of the consistency of P ∗ . However, some of this information focussed on one state may also have implications for other states.

Example. , ¬ ❡A and equivalent. To prove this we have to show that Ki (¬ ❡A) = Ki ( and i ∈ N: K (¬ ❡A) = tt ⇔ K ( ❡A) = ff i ❡¬A are logically ❡¬A) for every K i ⇔ Ki+1 (A) = ff ⇔ Ki+1 (¬A) = tt ⇔ K ( ❡¬A) = tt. i We now collect some facts about the semantical notions. 1. Let K = (η0 , η1 , η2 , . ) be some temporal structure and i ∈ N. If Ki (A) = tt and Ki (A → B ) = tt then Ki (B ) = tt. Proof. Ki (A → B ) means Ki (A) = ff or Ki (B ) = tt, and together with the assumption Ki (A) = tt it must be the case that Ki (B ) = tt.