Linear Temporal Logic

Table of Contents

• Motivation
• Temporal Operators
• Model Checking

Motivation

Linear temporal logic is a framework for expressing logical statements in time. Suppose a Boolean proposition $p$ is true if the robot’s battery is low. A propositional logical statement, such as $\neg p$, is either true or false at a given point in time. However, given an infinite expanse of discrete points in time, we might be interested in:

• Will $p$ be true at the next point in time?
• Will $p$ remain true until some other proposition, $q$, is satisfied?
• Will $p$ eventually be true?
• Is $p$ always true? (Is $p$ true at every point in time?)

These are questions of satisfiability in time. We can express these questions using temporal operators.

Temporal Operators

• $Xp$ is true if $p$ is true at the neXt time step.
• $pUq$ is true if $p$ is true at least Until $q$ is true. $q$ must be true at some time point.

$X$ and $U$ can be combined to create two additional linear temporal logical operators:

• $\Diamond p$ is equivalent to $\text{True} Up$, and is true if $p$ is eventually true. (Also denoted as $Fp$, for Future.)
• $\square p$ is equivalent to $\neg (\Diamond \neg p)$, and is true if $p$ is true at every point in time. (Also denoted as $Gp$, for Globally.)

Model Checking

A trace is an infinite sequence of states. Temporal logic can be used to specify properties of traces. To efficiently check that a property is always satisfied, represent as Büchi Automata.