Semantics of LTL

A transition system M=(S,→,L) is a set of states S endowed with a transition relation → (a binary relation), such that every s ∈ S has some s’∈ S with s → s’, and a labeling function L: S →P(Atoms). Transition systems are also simply called models. a model has a collection of states S, a relation →,saying how the system can move from state to state, and, associated with each state s, one has the set of atomic propositions L(s)which are true at that particular state. L is that it is just an assignment of truth values to all the propositional atoms. A transition system has more than one state, so this assignment depends on which state s the system is in: L(s) contains all atoms which are true in state s. All the information about a (finite) transition system M always be figured by using directed graphs whose nodes (which we call states) contain all propositional atoms that are true in that state. For example, if our system has only three states s0, s1 and s2; if the only possible transitions between states are s0 → s1, s0 → s2, s1 → s0, s1 → s2 and s2 → s2; and if L(s0)= {p, q}, L(s1)= {q, r} and L(s2)= {r}, then we can condense all this information into Figure given below: Note: A path in a model M=(S,→,L)is an infinite sequence of states s1,s2,s3,... in S such that, for each i ≥ 1, si → si+1.We write the path as s1 → s2 → ... . Definition: Let M=(S,→,L) be a model and π = s1 → ... be a path in M. Whether π satisfies an LTL formula is defined by the satisfaction relation ⊨ as follows: Clauses 1 and 2 reflect the facts that T is always true, and ⊥ is always false. Clause 8 removes the first state from the path, in order to create a path starting at the ‘next’ (second) state. Clauses 11–13, which deal with the binary temporal connectives. The formula φ1 U φ2 holds on a path if it is the case that φ1 holds continuously until φ2 holds. Moreover, φ1 U φ2 actually demands that φ2 does hold in some future state. The other binary connectives are W, standing for ‘Weak-until,’ and R, standing for ‘Release.’ Weak-until is just like U, except that φ W ψ does not require that ψ is eventually satisfied along the path in question, which is required by φ U ψ. Release R is the dual of U; that is, φ R ψ is equivalent to ¬(¬φ U ¬ψ). It is a fact that when we say ‘in all future states,’ we are including the present state as a future state. It is a matter of convention whether we do this, or not. A consequence of adopting the convention that the future shall include the present is that the formulas Gp → p, p → q U p and p → F p are true in every state of every model. So far we have defined a satisfaction relation between paths and LTL formulas. However, to verify systems, we would like to say that a model as a whole satisfies an LTL formula. This is defined to hold whenever every possible execution path of the model satisfies the formula. Suppose M=(S,→,L)is a model, s ∈ S,and φ an LTL formula. We write M,s ⊨ φ if, for every execution path π of M starting at s, we have π ⊨ φ. Exercise 1. List all sub formulas of the LTL formula ¬p U(F r ∨ G¬q → q W ¬r). 2. Consider the system of Figure. For each of the formulas φ: (b) a U b (e) X(a ∧ b) ∧ F(¬a ∧¬b) (i) Find a path from the initial state q3 which satisfies φ. (ii) Determine whether M,q3 ⊨ φ. (Detailed solution) a U b (i) Choose path ρ = (q3, q4, q3….) whenever we reach to a true “b” “a” is remains true. In all other paths a turns to false. M,q3 ⊨ φ does not hold because for all the other paths b U a does not hold. (Detailed solution) X(a ∧ b) ∧ F(¬a ∧ ¬b) (i) We can find a path q3, q4, q3,q1,.... where the next state from q3 satisfies a ∧ b and at some point in the future along that path, neither a or b are satisfied in q1. (ii) M,q3 ⊨ φ does not hold because for all the other paths X(a ∧ b) ∧ F(¬a ∧ ¬b) does not hold.