# Linear Temporal Logic
**Introduction**: Temporal logic - can refer to infinite behavior of a reactive system. Express properties about the rel. bw state labels in executions. [Amir Pnueli](https://en.wikipedia.org/wiki/Amir_Pnueli). Temporal logic can be linear (LTL) or branching (CTL). "*Temporal*" - modalities in temporal logic are *time-abstract*. Underlying time domain is *discrete* (Timed CTL = *continuous-time* domain).
**Syntax**: LTL formulae over the set AP of atomic propositions are formed according to the following grammar φ :== true | a | φ1 ∧ φ2 | ¬ φ | ○ φ | φ1 U φ2 where a ∈ AP. Unary bind stronger than binary. ○ ("next") and ¬ bind equally. U ("until") precedes over ∧, ∨, and → and is right-associative. The other operators can b e derived as follows: φ1 ∨ φ2 = ¬(¬φ1 ∧ ¬φ2); φ1 → φ2 = ¬φ1 ∨ φ2; φ1 ↔ φ2 = (φ1 → φ2) ∧ (φ2 → φ1); φ1 ⊕ φ2 = (φ1 ∧ ¬φ2) ∨ (φ2 ∧ ¬φ1). Can also combine temporal modalities: ◇ ("eventually") = true U φ; □ ("always") = ¬◇¬φ. □◇a ("always eventually a"); □◇φ (“infinitely often φ”); ◇□φ (“eventually forever φ”).
**Semantics**:
**Interpretation over Words**: of LTL formula φ is defined as a language Words(φ) that contains all infinite words over the alphabet 2^AP that satisfy φ. Let φ be an LTL formula over AP. The LT property induced by φ is Words(φ) = {σ ∈ (2^AP)^ω | σ ⊨ φ} where the satisfaction relation ⊨ ⊆ (2^AP)^ω × LTL is the smallest relation with the following. properties (LTL semantics (satisfaction relation ⊨) for infinite workds over 2^AP):
- σ ⊨ true
- σ ⊨ a iff a ∈ A_0 (i.e. A_0 ⊨ a)
- σ ⊨ φ1 ∧ φ2 iff σ ⊨ φ1 and σ ⊨ φ2
- σ ⊨ ¬φ iff σ ¬⊨ φ
- σ ⊨ ○φ iff φ[1...] = A1 A2 A3 ... ⊨ φ
- σ ⊨ φ1 U φ2 iff ∃j >= 0. σ[j ...] ⊨ φ2 and σ[i...] ⊨ φ1 for all 0 <= i < j.
Semantics for derived operators: φ ⊨ ◇φ iff ∃.j >- 0. φ[...] ⊨ φ; φ ⊨ □φ iff ∀j >= 0. φ[j...] ⊨ φ; φ ⊨ □φ = ¬◇¬φ ↔ ¬∃j >= 0. σ[j...] ⊨ ¬φ ↔ ¬∃j >= 0. σ[j...] ¬⊨ φ ↔ ∀j >= 0. σ[j...] ⊨ φ.
**over Paths and States**: Let TS = (S, Act, →, I, AP, L) be a transition system without terminal states, and let φ be an LTL-formula over AP.
- For infinite path fragment π of TS, the satisfaction relation is defined by π ⊨ φ iff trace(π) ⊨ φ
- For state s ∈ S, the satisfaction relation |= is defined bys ⊨ φ iff (∀π ∈ Paths(s). π ⊨ φ).
- TS ⊨ φ if Traces(TS) ⊆ Words(φ).
**LT Property**: A linear-time property over the set of atomic propositions AP is a subset of (2^AP)^ω (i.e. the set of words that arise from the infinite concatenation of words in 2^AP). LT is the *language* of infinite words over the alphabet 2^AP.
**Satisfaction Relation for LT Properties**: Let P be an LT property over AP and TS = (S, Act, →, I, AP, L) a transition system without terminal states. TS ⊨ P, iff Traces(TS) ⊆ P . State s ∈ S satisfies P, notation s ⊨ P, whenever Traces(s) ⊆ P .
**State Graph**: The state graph of TS, notation G(TS), is the digraph (V,E) with vertices V = S and edgesE={(s,s')∈ S×S |s' ∈Post(s)}.
**Path Fragment**: A finite path fragment π-hat of TS is a finite state sequence s_0 s_1 ... s_n such that s_i ∈ Post(s_i−1) for all 0 < i a <= n, where n >= 0. An infinite path fragment π is an infinite state sequence s0 s1 s2 ... such that si ∈ Post(s_(i−1)) for all i>0.
**Maximal and Initial Path Fragment**: A maximal path fragment is either a finite path fragment that ends in a terminal state, or an infinite path fragment. A path fragment is called initial if it starts in an initial state, i.e., if s0 ∈ I.
**Path**: A path of transition system TS is an initial, maximal path fragment. Paths(TS) is the set of all paths in TS. Paths_fin(TS) is the set of all initial, finite path fragments of TS.
**Trace and Trace Fragment**: Let TS = (S, Act, →, I, AP, L) be a transition system without terminal states. The trace of the infinite path fragment π = s0 s1 ... is defined as trace(π) = L(s0) L(s1) . . .. The trace of the finite path fragment π = s0 s1 ... sn is defined as trace(π) = L(s0) L(s1) ... L(sn). The set of traces of a set Π of paths: trace(Π) = {trace(π)|π ∈ Π}. Let Traces(s) denote the set of traces of s, and Traces(TS) the set of traces of the initial states of transition system TS: Traces(s) = trace(Paths(s)) and Traces(TS) = U_(s∈I) Traces(s).
**Transition System (TS)**: A transition system TS is a tuple (S, Act, →, I , AP, L) where. S is a set of states, Act is a set of actions, → ⊆ S × Act × S is a transition relation, I ⊆ S is a set of initial states, AP is a set of atomic propositions, and L : S → 2^AP is a labeling function. TS is called finite if S, Act, and AP are finite. The labeling function L(s) stand for a ∈ AP which are satisfied by state s. (note: 2^AP denotes the power set of AP);
**Reference**: Principles of Model Checking by Christel Baier and Joost-Pieter Katoen