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. 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):

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.

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 = 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