Unrolling LTL Specifications. LTL is a temporal logic that specifies properties over the future over paths, where the term temporal refers to a discrete notion of time. LTL does not in itself include the ability to reason about concrete, dense time, but rather considers timing as a sequence of computation steps. For instance, the logic itself provides the means to express that some property should hold after three computation steps, but not that it holds after three seconds, as opposed to more advanced logics such as timed computation tree logic (TCTL). Specifications in LTL are built from a finite set of atomic propositions, Boolean operators and the following temporal modalities: Globally ψ A property ψ shall hold globally, denoted Gψ. Finally ψ Eventually property ψ shall be satisfied, denoted Fψ. Next ψ In the successor state, ψ shall be satisfied, denoted Xψ. ψ1 Until ψ2 Property ψ1 shall hold until ψ2 holds, denoted ψ1Uψ2. These operators can be combined and nested to express complex properties. All LTL formulae are implicitly universally quantified, which means that the properties have to hold for all paths, as opposed to CTL which allows to specify properties over different possible futures by considering the branching structure of the computations1. 1At a first glance, CTL may thus appear to be more expressive than LTL. However, expressiveness of both logics is incomparable, and CTL has certain disadvantages when it comes to its application. See Sect. 2 for a discussion. The semantics of LTL is specified over infinite paths, which are naturally specified as ω-words π = s0s1 . . . over the alphabet 2AP where AP denotes the set of atomic properties. Let πi = sisi+1 . . . denote the suffix of π starting at position i. The satisfaction |= of an ω-word π is then specified as: • π |= p for p ∈ AP if and only iff p ∈ s0 • π |= ¬ψ iff π |= ψ • π |= ψ1 ∧ ψ2 iff π |= ψ1 and π |= ψ2 • π |= ψ1 ∨ ψ2 iff π |= ψ1 or π |= ψ2 • π |= X ψ iff π1 |= ψ. • π |= ψ1 U ψ2 iff there exists iN such that πi |= ψ and for all 0 ≤ k ≤ i, πk |= ψ1. The semantics of Gψ and Fψ follow directly from the following equiva- lences: • G ψ ≡ ¬F ¬ψ • F ψ ≡ true U ψ This semantics can naturally be unrolled until a fixed depth k, for exam- ple: F ψi = ψi ∨ ψi+1 ∨ . . . ∨ ψk G ψi = ψi ∧ ψi+1 ∧ . . . ∧ ψk 2 1 1 2 2 G ψi ∧ F ψi = (ψi ∨ ψi+1 ∨ . . . ∨ ψk) ∧ (ψi ∧ ψi+1 ∧ . . . ∧ ψk) This approach allows the specification to be passed directly to an SMT solver so that M can be checked for satisfiability.
