Semantics of LTL

Logical Paradigms in Computing Practical patterns of specifications: • It is impossible to get to a state where started holds, but ready does not hold: G¬(started ∧¬ready) • For any state, if a request (of some resource) occurs, then it will eventually be acknowledged: G(requested → F acknowledged). • A certain process is enabled infinitely often on every computation path: GF enabled. • Whatever happens, a certain process will eventually be permanently deadlocked: FG deadlock. • If the process is enabled infinitely often, then it runs infinitely often. GF enabled → GF running. • An upwards travelling lift at the second floor does not change its direction when it has passengers wishing to go to the fifth floor: G(floor2 ∧ directionup ∧ ButtonPressed5 → (directionup U floor5)). Here, our atomic descriptions are boolean expressions built from system variables, e.g., floor2. Important equivalences between LTL formulas: Definition: We say that two LTL formulas φ and ψ are semantically equivalent, or simply equivalent, writing φ ≡ ψ, if for all models M and all paths π in M: π ⊨ φ iff π ⊨ ψ. F and G are duals of each other, and X is dual with itself: Also U and R are duals of each other: It’s also the case that F distributes over ∨ and G over ∧, i.e. Example: Prove the equivalence of φ U ψ ≡ φ W ψ ∧ F ψ. Suppose first that a path satisfies φ U ψ. Then, from clause 11, we have i ≥ 1such that πi ⊨ ψ and for all j =1,...,i – 1 we have πj⊨ φ. From clause 12, this proves φ W ψ, and from clause 10 it proves F ψ. Thus for all paths π, if π ⊨ φ U ψ then π ⊨ φ W ψ ∧ F ψ. Adequate sets of connectives for LTL: Small adequate sets of connectives also exist in LTL. Here is a summary of the situation. • X is completely orthogonal to the other connectives. That is to say, its presence doesn’t help in defining any of the other ones in terms of each other. Moreover, X cannot be derived from any combination of the others. • Each of the sets {U,X}, {R,X}, {W,X} is adequate. To see this, we note that 1. R and W may be defined from U, by the duality φ R ψ ≡¬(¬φ U ¬ψ) 2. U and W may be defined from R, by the duality φ U ψ ≡¬(¬φ R ¬ψ) 3. Rand U may be defined from W, by equivalence and the duality φ U ψ ≡¬(¬φ R ¬ψ) Example: Prove that equivalence φ U ψ ≡¬(¬ψ U(¬φ ∧¬ψ)) ∧ F ψ holds for all LTL formulas φ and ψ. Proof: Take any path s0 → s1 → s2 → ... in any model. Exercise 1. Prove the equivalences: φ U ψ ≡ φ W ψ ∧ F ψ. For each equivalence there are two directions to prove. 2. Prove that φ U ψ ≡ ψ R(φ ∨ ψ) ∧ F ψ.