Model Checking: Learn Linear Temporal Logic (LTL)

1. Introduction

While our previous blog post focused mainly on the different models used in Model Checking (Kripke structures, Labelled Transition Systems and Program Graphs), this blog focuses only on Kripke structures. One reason is that we can transform the other models into a Kripke structure as well. The transformations needed will, however, be discussed in detail in later posts. Our focus in this post is to study the properties of a system. For instance, how can one tell if a system does what it should actually do? For that, we first need to define what we mean by “the system should do so-and-so.” This definition of properties is in general easier to verify on Kripke structures. The automatic verification process will be reserved for a later blog. Our main focus in this post is one way fr defining the property’s syntax and semantics: The Linear Time Logic (LTL).

2. Why not typical Propositional or Predicate Logic?

The main reason is that these types of logics generally lack information that we want to express about our model. For instance, suppose we have the model of an elevator and we want to check the property “The elevator will eventually run out-of-service.” This is hard to define in propositional or predicate logic because of their lack of temporal information: they describe how the system is now, but not how it will eventually be in the future. This motivates the need for a more sophisticated type of logic that can express what will happen to our system over time. This is where Linear Temporal Logic (LTL) and Computational Tree Logic (CTL) come into the picture. Our focus in this blog will be Linear Temporal Logic, and we reserve the next blog to study CTL and its difference to LTL.

3. Linear Temproal Logic (LTL)

3.1. Definition of syntax

Every LTL formula over a set of atomic propositions AP is defined as one of the following expressions:

True (similar to propositional/predicate logic)
False (similar to propositional/predicate logic)
p ∈ AP: a propositional variable (similar to propositional logic)
ϕ ∨ ψ (the OR operator, similar to propositional logic), where ϕ and ψ are LTL formulas
¬ϕ (the NOT operator, similar to propositional logic), where ϕ is an LTL formula
Xϕ (sometimes written as ∘ϕ), where ϕ is an LTL formula. The X operator is called “next.”
ϕ U ψ, where ϕ and ψ are LTL formulas. The U operator is called “until.”

3.2. Definition of semantics

An LTL formula is evaluated (to True/False) over a single path of a Kripke structure. For a path P = $s_0 s_1 s_2 s_3 \dots$ we write P ⊨ ψ when the path P satisfies the LTL formula ψ. Satisfaction is defined recursively over the syntax of LTL formulas:

P ⊨ True always holds.
P ⊨ False never holds (also written as P ⊭ False).
P ⊨ p holds exactly when $p \in L(s_0)$, i.e. when p holds at the first state of the path.
P ⊨ ϕ ∨ ψ holds exactly when P ⊨ ϕ or P ⊨ ψ (at least one of the formulas holds).
P ⊨ ¬ϕ holds exactly when P ⊭ ϕ.
P ⊨ Xϕ holds exactly when the suffix path $s_1 s_2 s_3 \dots$ satisfies ϕ (i.e. the next operator checks the property starting at the next state).
P ⊨ ϕ U ψ holds exactly when there exists an $i \in \mathbb{N} \cup \{0\}$ such that:for all $0 \le k < i$: the suffix $s_k s_{k+1} s_{k+2} \dots ⊨ ϕ$, and at position $i$ we have the suffix $s_i s_{i+1} \dots ⊨ ψ$. In other words, ψ must eventually hold, and ϕ must hold at every state before the first time ψ holds. Informally, the path looks like $ϕϕϕ \dots ϕψ \text{True True True} \dots$. In particular, if ψ already holds at the beginning, then ϕ U ψ holds immediately.

We say that an LTL formula holds in a state of a Kripke structure if it holds on all possible paths starting at that state. We say it holds on the Kripke structure if it holds on all of its initial states.

3.3. Syntactic sugar

Other operators in LTL are derived from the basic syntax. The following table summarizes commonly used derived operators, their meaning, and their derivation from the original LTL syntax. Our focus, however, will be on F, G, X, and U.

Notation	Explanation	Derived from
ϕ ∧ ψ	And: both ϕ and ψ must hold now.	¬(¬ϕ ∨ ¬ψ)
ϕ → ψ	Implication: if ϕ holds now, then ψ holds now.	¬ϕ ∨ ψ
F ϕ	Finally: ϕ must hold eventually (at some future point).	True U ϕ
G ϕ	Globally: ϕ must hold on all states of the path.	¬(F ¬ϕ)
ψ W ϕ	Weak until: ψ must hold at least until ϕ; if ϕ never becomes true, ψ must remain true forever.	(G ϕ) ∨ (ψ U ϕ)
ψ M ϕ	Strong release: ϕ must be true until and including the point where ψ first becomes true, which must hold at the current or a future position.	¬(¬ψ W ¬ϕ)
ψ R ϕ	Release: ϕ must be true until and including the point where ψ first becomes true; if ψ never becomes true, ϕ must remain true forever.	ϕ W (ϕ ∧ ψ)

While combinations of these operators can get complex, two commonly used combinations are:

GF ψ: ψ holds infinitely many times. For example, GF idle expresses that an elevator always becomes idle infinitely often (it cannot stay moving forever).
FG ψ: ψ will hold forever from some point onward (not necessarily now). For example, FG oos expresses that the elevator will eventually become out-of-service and remain out-of-service forever.

3.4. Examples

We take the following Kripke structure and decide whether each of the following LTL formulae holds.

3.4.1. The Kripke structure:

$Kripke Structure Example for Linear Temporal Logic formulae. Graphviz notation: digraph G { n[label="", shape="point"]; s0[label="s0\n{p,q}"]; s1[label="s1\n{p}"]; s2[label="s2\n{q}"]; s3[label="s3\n{}"]; n-> s0; s0->s1; s0->s3; s1->s0; s1->s2; s2->s2; s2->s3; s3->s1; }$

3.4.2. The formulae:

$F_1 = Fp$
$F_2 = F(\neg p \land \neg q)$
$F_3 = Gp$
$F_4 = X \neg q$
$F_5 = XX(p \lor q)$
$F_6 = GFp$
$F_7 = XF(p \land q)$
$F_8 = GFq$
$F_9 = FG(p \lor q)$
$F_{10} = G(p \lor q) \to ((FG p) \lor (FG q))$
$F_{11} = (p \land q) U (\neg p \land \neg q)$
$F_{12} = XF(p U q)$

3.4.3. Solution and explanation

Formula	Truth value	Explanation
$F_1$	True	“Eventually, p will hold,” which is true because p holds in the initial state.
$F_2$	False	“Eventually neither p nor q will hold” is false for the path $s_0 s_1 s_0 s_1 s_0 s_1 \dots$ because p always holds on that path.
$F_3$	False	“p holds always” is false for any path visiting $s_3$; for example the path $s_0 s_3 s_1 s_2 s_2 s_2 \dots$ visits a state where p does not hold.
$F_4$	True	“q will not hold in the next state,” which is true because the next state is either $s_1$ or $s_3$, and q doesn’t hold in either.
$F_5$	True	“p or q will hold after two steps,” which is true because the state two steps ahead is either $s_0$, $s_1$, or $s_2$, each containing at least p or q.
$F_6$	False	“p holds infinitely many times” is false for the path $s_0 s_1 s_2 s_2 s_2 \dots$ because if we remain in $s_2$ forever, p does not hold there.
$F_7$	False	“Starting from the next state, p and q will eventually hold together” is false for the path $s_0 s_1 s_2 s_2 s_2 \dots$ because from $s_1$ onwards, $p \land q$ never holds.
$F_8$	True	“q holds infinitely many times” is true: from any state, q will hold within at most two steps (either immediately or after one or two transitions), so q recurs infinitely often on every path.
$F_9$	False	“At some point, $p \lor q$ will always hold” is false for the path $s_0 s_3 s_1 s_0 s_3 s_1 \dots$ because $s_3$ repeatedly breaks the property $p \lor q$.
$F_{10}$	True	If $p \lor q$ always holds, then either p or q will eventually hold forever. The condition $G(p \lor q)$ is true precisely for paths that do not contain $s_3$. Two cases arise: (1) If the path never reaches $s_2$ (e.g. $s_0 s_1 s_0 s_1 \dots$), then p holds in both $s_0$ and $s_1$, so p will eventually hold forever. (2) If the path reaches $s_2$, then from that point one can stay in $s_2$ forever and q holds in $s_2$; thus q will eventually hold forever. Hence the implication holds.
$F_{11}$	False	“Both p and q will always hold until the first time where neither p nor q holds” is false for the path $s_0 s_1 s_0 s_3 s_1 s_0 s_1 \dots$; before reaching $s_3$ (the only state satisfying $\neg p \land \neg q$), we visit $s_1$ where $p \land q$ does not hold.
$F_{12}$	True	“Starting from the next state, F(p U q) holds.” The next state is either $s_1$ or $s_3$. If at $s_1$, then q holds at the following state, and p holds at $s_1$, so $p U q$ holds at $s_1$. If at $s_3$, the next state is $s_1$, and as before $p U q$ will hold at that point. Thus $F(p U q)$ holds within at most one step in both cases, so $X F(p U q)$ is true.

4. Summary

This post focused on the syntax and semantics of Linear Temporal Logic (LTL) interpreted over paths of a Kripke structure. We explained the basic operators (X for next, U for until) and derived operators such as F (finally) and G (globally). We emphasized that LTL reasons about how properties evolve along paths (i.e., over time) rather than just the current state, which is why it is more suitable than plain propositional or predicate logic for expressing temporal properties (for example, eventualities and invariants). Finally, we walked through example formulae on a given Kripke structure and determined which formulae hold on which paths, illustrating typical uses of LTL in model checking.

5. Sources

“Linear temporal logic” — Wikipedia. Note: This page was used for the table of syntactic sugar (operators like F, G, W, R, M).
Baier, C. & Katoen, J.-P., Principles of Model Checking, Springer.Comprehensive textbook covering Kripke structures, LTL/CTL, semantics and model-checking algorithms.
“Temporal logic” — Wikipedia.Background on temporal logics and their classifications (linear vs. branching time).
“Introduction to Model Checking” — Lecture notes, RWTH Aachen.Readable lecture notes introducing Kripke structures, LTL semantics and examples.
Clarke, E., Grumberg, O., & Peled, D., “Model Checking” — in the Handbook of Model Checking.Survey chapter and reference material on model-checking techniques and temporal logics.
Baier & Katoen — “Principles of Model Checking” (PDF mirror).Direct PDF mirror of the textbook for quick access to chapters on LTL and Kripke structures.

0 0 votes

Article Rating

Formula	Truth value	Explanation
\(F_1\)	True	“Eventually, p will hold,” which is true because p holds in the initial state.
\(F_2\)	False	“Eventually neither p nor q will hold” is false for the path \(s_0 s_1 s_0 s_1 s_0 s_1 \dots\) because p always holds on that path.
\(F_3\)	False	“p holds always” is false for any path visiting \(s_3\); for example the path \(s_0 s_3 s_1 s_2 s_2 s_2 \dots\) visits a state where p does not hold.
\(F_4\)	True	“q will not hold in the next state,” which is true because the next state is either \(s_1\) or \(s_3\), and q doesn’t hold in either.
\(F_5\)	True	“p or q will hold after two steps,” which is true because the state two steps ahead is either \(s_0\), \(s_1\), or \(s_2\), each containing at least p or q.
\(F_6\)	False	“p holds infinitely many times” is false for the path \(s_0 s_1 s_2 s_2 s_2 \dots\) because if we remain in \(s_2\) forever, p does not hold there.
\(F_7\)	False	“Starting from the next state, p and q will eventually hold together” is false for the path \(s_0 s_1 s_2 s_2 s_2 \dots\) because from \(s_1\) onwards, \(p \land q\) never holds.
\(F_8\)	True	“q holds infinitely many times” is true: from any state, q will hold within at most two steps (either immediately or after one or two transitions), so q recurs infinitely often on every path.
\(F_9\)	False	“At some point, \(p \lor q\) will always hold” is false for the path \(s_0 s_3 s_1 s_0 s_3 s_1 \dots\) because \(s_3\) repeatedly breaks the property \(p \lor q\).
\(F_{10}\)	True	If \(p \lor q\) always holds, then either p or q will eventually hold forever. The condition \(G(p \lor q)\) is true precisely for paths that do not contain \(s_3\). Two cases arise: (1) If the path never reaches \(s_2\) (e.g. \(s_0 s_1 s_0 s_1 \dots\)), then p holds in both \(s_0\) and \(s_1\), so p will eventually hold forever. (2) If the path reaches \(s_2\), then from that point one can stay in \(s_2\) forever and q holds in \(s_2\); thus q will eventually hold forever. Hence the implication holds.
\(F_{11}\)	False	“Both p and q will always hold until the first time where neither p nor q holds” is false for the path \(s_0 s_1 s_0 s_3 s_1 s_0 s_1 \dots\); before reaching \(s_3\) (the only state satisfying \(\neg p \land \neg q\)), we visit \(s_1\) where \(p \land q\) does not hold.
\(F_{12}\)	True	“Starting from the next state, F(p U q) holds.” The next state is either \(s_1\) or \(s_3\). If at \(s_1\), then q holds at the following state, and p holds at \(s_1\), so \(p U q\) holds at \(s_1\). If at \(s_3\), the next state is \(s_1\), and as before \(p U q\) will hold at that point. Thus \(F(p U q)\) holds within at most one step in both cases, so \(X F(p U q)\) is true.