Temporal Logic and Interval Reasoning

"Every model in this book guessed at numbers. I do not guess. I assert. I say that something good will eventually happen, and I will keep saying it, calmly, at every timestep, until either the something good happens or the universe ends. So far the universe has not ended, so my track record is excellent."

A Logic Formula That Insists Something Good Eventually Happens

Chapter 30 opens Part VII, where the statistical machinery of Parts I through VI is assembled into intelligent temporal systems, and it opens with reasoning and causality because those are the two faculties a forecaster or an agent still lacks. The previous parts gave us models that predict and act; this chapter gives us models that can say what they require and say why things happen. This first section handles the saying-what-they-require half: temporal logic, a symbolic complement to every learned model so far. Section 30.2 turns to the why with causal discovery for time series (Granger causality, PCMCI, and causal networks), and the remaining sections of the chapter, Section 30.3 and Section 30.4, build on both. We use the unified notation of Appendix A: a signal $s$ with value $s(t)$ at time $t$, a predicate $\mu$ over signal values, and $\varphi$, $\psi$ for temporal formulas.

Why does a book about forecasting and decision making need formal logic at all? Because a learned model is mute about its own obligations. A load forecaster outputs a number; it cannot tell you "this forecast violates the requirement that reserve margin stays above ten percent for the next six hours", because that requirement was never written down in a language the system can check. Temporal logic is that language. Once a requirement is a formula, a monitor can check it continuously against a live signal and raise an alarm the instant it is breached, an agent can be rewarded for satisfying it, and a learner can be pushed, by gradient, toward signals that satisfy it more robustly. The same formula serves all three roles: specification, monitoring, and training signal. That reuse is the reason this material sits at the head of the "building intelligent systems" part rather than in an appendix.

The competencies this section installs are four. First, to read and write LTL formulas over discrete propositions and STL formulas over real signals, with their temporal operators. Second, to compute STL quantitative robustness, the real-valued margin of satisfaction, by hand and in code. Third, to place two intervals in Allen's algebra and use the relations for qualitative temporal reasoning. Fourth, to deploy a robustness monitor as a runtime check and to see why its differentiability makes it a learning objective. These are the load-bearing skills for the temporal agents of Chapter 31 and for any deployed system that must respect temporal requirements.

1. Reasoning About Time Symbolically: LTL and STL Intermediate

A statistical model answers "what will the value be?" A temporal logic answers a different kind of question: "does the trajectory satisfy this property over time?" The property is something like "the system is always safe", "a fault is eventually cleared", or "the door stays locked until a valid badge is read". These are statements about the shape of a trajectory across time, not about a single value, and ordinary propositional logic cannot express them because it has no notion of "later" or "always". Temporal logic adds exactly that: operators that quantify over time.

The contrast with the rest of the book is worth stating sharply, because it is the reason this section exists. A forecaster maps a history to a distribution over future values; it is a function from the past to a guess. A temporal-logic formula maps a whole trajectory to a verdict about a property; it is a function from a behavior to a judgment about that behavior. The two compose rather than compete: the forecaster (or simulator, or deployed system) produces the trajectory, and the logic judges it. Nothing in Parts I through VI could phrase the judgment, because a judgment about "always" or "until" is not a number a regression head can emit. Adding the logic does not replace the learned model; it gives the learned model's output something to be held accountable to.

The cleanest starting point is Linear Temporal Logic. LTL reasons over an infinite (or long finite) sequence of states, where at each state a set of atomic propositions is either true or false. On top of the usual Boolean connectives ($\neg$, $\wedge$, $\vee$, $\Rightarrow$) it adds four temporal operators that range over the future of the sequence. Writing $\pi = s_0 s_1 s_2 \dots$ for the trajectory and $\pi_i$ for its suffix starting at position $i$, the operators are defined as:

From these four, the two most quoted patterns in all of verification follow immediately. Safety ("nothing bad ever happens") is $\mathbf{G}\,\neg\text{bad}$: globally, the bad proposition is false. Liveness ("something good keeps happening") is $\mathbf{G}\,\mathbf{F}\,\text{good}$: globally and finally, the good proposition recurs forever. The epigraph's stubborn formula is exactly $\mathbf{F}\,\text{good}$, asserting eventual satisfaction. Note that $\mathbf{F}$ and $\mathbf{G}$ are duals, $\mathbf{F}\,\varphi \equiv \neg\mathbf{G}\,\neg\varphi$ ("eventually $\varphi$" is "not always not $\varphi$"), and that $\mathbf{F}\,\varphi \equiv \text{true}\,\mathbf{U}\,\varphi$, so until is the primitive and the rest are conveniences.

It pays to dwell on why these patterns are not interchangeable, because the safety/liveness distinction structures the whole field of verification. A safety property is one whose violation is witnessed by a finite prefix: the instant the bad proposition becomes true, the property $\mathbf{G}\,\neg\text{bad}$ is irrevocably broken, and no future can repair it. That finiteness is exactly what makes safety properties monitorable at runtime: you can detect the breach the moment it happens. It is why every online monitor in subsection three watches a safety formula. A liveness property, by contrast, can never be falsified by any finite prefix: no matter how long you have waited for $\text{good}$ to recur, it might still happen one step later, so $\mathbf{G}\,\mathbf{F}\,\text{good}$ is only ever violated "in the limit". This asymmetry, breaches of safety are observable in finite time while breaches of liveness are not, is the reason runtime verification leans on safety and bounded-horizon properties, and it is the practical motivation for the time bounds that STL attaches to every operator.

LTL's limitation for our purposes is that it is Boolean and discrete: a proposition is true or false, and time is a sequence of indices. The signals of this book are real-valued and often continuous. Signal Temporal Logic (STL) is the lift. Its atomic objects are not propositions but predicates over real signal values, $\mu \equiv (f(s(t)) \ge 0)$ for some real function $f$, for example $\mu \equiv (\text{temperature}(t) \le 80)$ rewritten as $80 - \text{temperature}(t) \ge 0$. Its temporal operators carry explicit time bounds: $\mathbf{F}_{[a,b]}$ ("eventually within the window $[a,b]$"), $\mathbf{G}_{[a,b]}$ ("always over $[a,b]$"), and $\mathbf{U}_{[a,b]}$. So "the temperature reaches at least 70 within 5 minutes and then stays below 80 for the following hour" is a single STL formula $\mathbf{F}_{[0,5]}(\text{temp} \ge 70) \wedge \mathbf{G}_{[5,65]}(\text{temp} \le 80)$.

Before the quantitative leap, it is worth seeing that even Boolean STL is strictly more expressive for engineered systems than LTL, because the time bounds let it talk about deadlines and durations, not merely about "eventually". "The fault is eventually cleared" ($\mathbf{F}\,\text{clear}$) is a promise with no teeth: a system that clears the fault after a century satisfies it. "The fault is cleared within thirty seconds" ($\mathbf{F}_{[0,30]}\,\text{clear}$) is the requirement an engineer actually means, and it is checkable on a finite trace. The bounded-window operators are what make STL a specification language for real deadlines rather than an idealized account of infinite futures, and they are why an STL window is the natural object that Allen's interval algebra (subsection two) will later relate.

The decisive innovation of STL is not the time bounds but the quantitative semantics. Instead of returning true or false, STL returns a real number $\rho(\varphi, s, t)$, the robustness, that measures by how wide a margin the signal satisfies (positive) or violates (negative) the formula at time $t$. For a predicate it is just the signed margin of the function; for the connectives and temporal operators it is built from $\min$ and $\max$:

For until, $\rho(\varphi\,\mathbf{U}_{[a,b]}\psi, s, t) = \max_{t' \in [t+a,\, t+b]} \min\big(\rho(\psi, s, t'),\ \min_{t'' \in [t,\, t']} \rho(\varphi, s, t'')\big)$, read as: $\psi$ must eventually fire somewhere in the window, and $\varphi$ must hold robustly up to that moment.

Read these as the formal version of intuition. "Always over a window" ($\mathbf{G}$) is as robust as its weakest moment, hence the $\min$ over the window; one near-violation drags the whole conjunction down. "Eventually within a window" ($\mathbf{F}$) is as robust as its best moment, hence the $\max$; one comfortable satisfaction is enough. The sign of $\rho$ recovers the Boolean verdict ($\rho \ge 0$ means satisfied), and the magnitude tells you the safety margin, how much the signal could be perturbed before the verdict flips. That single real number is what makes STL so much more useful than LTL for engineered systems: it grades satisfaction instead of merely certifying it, and a graded score is something you can monitor for trends, rank scenarios by, and, as subsection four shows, differentiate.

2. Allen's Interval Algebra: Qualitative Reasoning About Durations Intermediate

LTL and STL reason about instants: at each timestep, is the property true. But much temporal reasoning is about events with duration, intervals rather than points, and about the qualitative relationships between them: did the outage happen during the maintenance window, or did it overlap the start of it, or come entirely before it? These distinctions matter for diagnosis, planning, and explanation, and they are often all we know: we may not have exact timestamps, only the qualitative fact that one event preceded another. Allen's interval algebra (Allen, 1983) is the canonical formalism for exactly this kind of qualitative temporal reasoning.

Allen's insight is that between any two time intervals there are exactly thirteen mutually exclusive, jointly exhaustive relations. Take two intervals $A = [A^-, A^+]$ and $B = [B^-, B^+]$. Six relations and their six inverses, plus the symmetric "equals", account for every possible arrangement of their endpoints. Figure 30.1.1 lays out the seven base relations (the other six are the inverses of the six asymmetric ones).

Why thirteen and not some other number? Because two intervals are fixed by four endpoints, $A^-, A^+, B^-, B^+$, with the only constraints $A^- < A^+$ and $B^- < B^+$, and the qualitative relation is determined entirely by the ordering of $A$'s endpoints against $B$'s. Enumerating the consistent orderings of those four points, and collapsing the ones that describe the same picture, yields exactly thirteen cases, no more and no fewer. This exhaustiveness is what makes the algebra a genuine algebra rather than a loose vocabulary: every pair of intervals falls into exactly one relation, so a set of pairwise relations is a complete qualitative description of a temporal scene, and reasoning over it is closed.

The power of the algebra is not the catalog but the composition table: given that $A$ relates to $B$ and $B$ relates to $C$, the algebra tells you which relations are possible between $A$ and $C$. If $A$ is before $B$ and $B$ is before $C$, then $A$ is necessarily before $C$; but if $A$ overlaps $B$ and $B$ during $C$, several $A$-to-$C$ relations remain possible, and the table enumerates them. This composition is what lets a system reason about time with incomplete information: feed it a handful of pairwise qualitative constraints and it propagates them to a globally consistent picture (or detects that no consistent picture exists), a constraint-satisfaction problem solved by a path-consistency algorithm (it repeatedly intersects each pairwise relation with what its neighbors allow via the composition table until nothing changes). That is qualitative temporal reasoning: deriving new temporal facts from known ones without ever needing a single numerical timestamp.

3. Temporal Logic in Temporal AI: Monitoring, Rewards, Constraints Intermediate

Having the logics, we now place them in the architecture of an intelligent temporal system. They earn their place in three distinct roles, and the same formula can serve more than one.

Monitoring requirements over a signal (runtime verification). The most direct use is to take a requirement, written as an STL formula, and check it continuously against a live or recorded signal. This is runtime verification or online monitoring: a monitor consumes the signal stream and, at each tick, reports the current robustness of the spec, raising an alarm the moment robustness goes negative. This is the formal, specification-driven cousin of the statistical anomaly and change-point detectors of Chapter 8 and the live callback monitors of the adaptive systems in Chapter 21: where those flag statistically surprising behavior, an STL monitor flags behavior that violates a stated requirement, and the two are complementary safety nets. Crucially, because robustness is a margin and not just a verdict, a monitor can warn of a declining margin before the breach actually occurs, an early-warning capability a Boolean monitor lacks.

Specifying tasks and rewards for agents. The agents of Part VI were driven by scalar reward functions, and a recurring pain there was that hand-designed rewards are brittle and hard to align with what we actually want. Temporal logic offers a principled alternative: specify the task as an LTL or STL formula and derive the reward from it. "Reach the goal region eventually while always avoiding the hazard" is $\mathbf{F}\,\text{goal} \wedge \mathbf{G}\,\neg\text{hazard}$, and the STL robustness of that formula, evaluated on the agent's trajectory, is a dense, shaped, automatically-generated reward that is positive exactly when the task is satisfied and grows with the margin. This is the basis of LTL/STL reward specification and reward machines, an active thread in reinforcement learning that connects directly back to the MDP reward design of Chapter 22 and the agent designs of Chapter 31.

Expressing constraints. The third role is as hard or soft constraints on a controller or planner: a model-predictive controller can be required to keep STL robustness non-negative over its prediction horizon, turning "stay safe" into an optimization constraint $\rho(\varphi, s, \cdot) \ge 0$. Because robustness is real-valued, it slots directly into the objective or the constraint set of a numerical optimizer, which is why STL has become a standard interface between high-level temporal requirements and low-level control.

These three roles are unified by one fact that bears emphasis: the same formula serves all of them. The requirement "always within bounds, eventually reach the target" is, without modification, an online monitor (evaluate its robustness on the live stream), a reward (feed its robustness to the agent as a per-step or per-episode signal), and a constraint (require its robustness non-negative inside the planner). This is the economy that makes temporal logic attractive to a systems builder: write the requirement once, in one precise language, and reuse it across specification, verification, training, and control. A hand-tuned scalar reward, by contrast, is good for exactly one of those roles and must be re-derived for each of the others, with no guarantee the three versions agree. The single-source-of-truth property is the practical core of why Part VII opens here.

4. The Bridge to Learning: Differentiable Robustness and Neuro-Symbolic Reasoning Advanced

The deepest reason STL belongs in this book is that its robustness is, with one small softening, differentiable, which makes a logical specification into a training objective and reconnects symbolic temporal reasoning to the gradient-based learning of Parts III through VI. The robustness of subsection one is built entirely from $\min$, $\max$, and the predicate functions $f$. The predicate functions are typically smooth; the only non-smooth pieces are $\min$ and $\max$. Replace them with smooth surrogates, the softmin and softmax,

and the entire robustness $\rho$ becomes a smooth, differentiable function of the signal, with the temperature $\beta$ controlling how closely the surrogate tracks the true (hard) robustness: large $\beta$ recovers the exact $\min$/$\max$, small $\beta$ smooths aggressively. Now a learned model that produces a signal, a forecaster, a generator, or a control policy, can be trained to maximize the robustness of an STL spec by ordinary backpropagation. The spec becomes a loss. "Produce trajectories that satisfy this temporal requirement as robustly as possible" is now a gradient-descent problem.

The softening is not free, and the temperature $\beta$ is the knob that prices it. With a finite $\beta$ the smoothed robustness $\widetilde{\rho}$ is a biased estimate of the true robustness $\rho$: softmin always reports something a little larger than the true minimum, softmax something a little smaller than the true maximum, so the smoothed margin systematically overstates how safe a near-violation is. As $\beta$ grows the bias vanishes but the gradient sharpens toward the hard, almost-everywhere-zero gradient of the true $\min$/$\max$, which is exactly the vanishing-signal problem optimization wanted to avoid. The practical recipe, familiar from temperature annealing elsewhere in the book, is to start with a small $\beta$ for a smooth, informative loss landscape and anneal it upward so the final objective tracks the true requirement. Choosing $\beta$ badly is the single most common way differentiable-STL training quietly fails: too small and the policy optimizes a margin that does not match the real spec; too large and the gradient carries no usable signal.

This is the entry point to neuro-symbolic temporal reasoning: the symbolic layer (the STL formula) supplies the structure and the requirement, the neural layer supplies the flexible function approximation, and differentiable robustness is the glue that lets gradients flow from the logical spec into the network weights. The arrangement appears in safe control (train a policy whose trajectories maximize safety robustness), in requirement-guided generation (train a sequence generator whose samples satisfy temporal constraints, connecting to the generative temporal models of Chapter 17), and in specification mining (learn the STL formula itself from labeled good and bad traces). The through-line of this book, that every classical idea returns in learned form, here reaches its symbolic frontier: a hand-written logical requirement and a learned network, joined by a differentiable margin.

5. Worked Example: An STL Robustness Monitor From Scratch, Then by Library Advanced

We now make robustness executable. The plan: implement the quantitative semantics of subsection one directly in numpy, monitor a signal against a spec that combines "always within a bound" and "eventually reaches a target", read off a single robustness number that decides safety, and then reproduce the same verdict with the rtamt runtime-monitoring library, stating the line-count reduction. Code 30.1.1 is the from-scratch monitor: each STL operator is one function, exactly mirroring the $\min$/$\max$ semantics.

import numpy as np

# A discrete-time signal: temperature read once per minute for 20 minutes.
t = np.arange(20)                                  # time stamps 0..19 (minutes)
temp = np.array([62, 64, 66, 69, 71, 73, 74, 75,   # rises, then settles in band
                 76, 77, 78, 77, 76, 75, 74, 73,
                 72, 71, 70, 69], dtype=float)

# --- STL predicates return the SIGNED MARGIN f(s(t)) at every time step ---
def pred_at_least(sig, c):   return sig - c        # rho of (sig >= c):  sig - c
def pred_at_most(sig, c):    return c - sig        # rho of (sig <= c):  c - sig

# --- temporal operators over a [a, b] window, in index units ---
def always(rho, a, b):
    """rho of G_[a,b] phi at each t = min of phi's robustness over the window."""
    n = len(rho); out = np.full(n, np.inf)
    for i in range(n):
        lo, hi = i + a, min(i + b, n - 1)          # clamp window to signal end
        if lo <= hi:
            out[i] = rho[lo:hi + 1].min()          # G -> weakest moment -> min
    return out

def eventually(rho, a, b):
    """rho of F_[a,b] phi at each t = max of phi's robustness over the window."""
    n = len(rho); out = np.full(n, -np.inf)
    for i in range(n):
        lo, hi = i + a, min(i + b, n - 1)
        if lo <= hi:
            out[i] = rho[lo:hi + 1].max()          # F -> best moment -> max
    return out

def conj(r1, r2):   return np.minimum(r1, r2)      # AND -> min

# Spec: ALWAYS temp <= 80 over the full 20-minute trace, AND EVENTUALLY temp >= 70 within 5 min.
r_bound  = always(pred_at_most(temp, 80), 0, 19)   # G_[0,19] (temp <= 80)
r_reach  = eventually(pred_at_least(temp, 70), 0, 5)# F_[0,5]  (temp >= 70)
r_spec   = conj(r_bound, r_reach)                  # the combined robustness signal

print("robustness at t=0 : %.1f" % r_spec[0])      # the headline safety margin
print("min robustness    : %.1f" % np.nanmin(r_spec[np.isfinite(r_spec)]))
print("verdict (rho>=0)  :", bool(r_spec[0] >= 0))

robustness at t=0 : 2.0
min robustness    : 2.0
verdict (rho>=0)  : True

The single number $+2.0$ is the whole point: it certifies satisfaction and quantifies the slack. Code 30.1.2 walks the numeric example explicitly, showing where that $2.0$ comes from and what happens when the signal nears the bound.

# Why is the margin exactly 2.0? Trace the binding (weakest) moment.
peak = temp.max()                                  # hottest reading = 78
print("peak temperature      :", peak)
print("bound margin at peak  :", 80 - peak)        # 80 - 78 = 2.0  -> sets G's min
print("reach margin at t=0   :", (temp[:6] - 70).max())  # F_[0,5]: best of first 6

# A counterfactual: shift the signal up by 3 degrees -> peak 81 breaches the 80 bound.
temp_hot = temp + 3.0
r_hot = conj(always(pred_at_most(temp_hot, 80), 0, 19),
             eventually(pred_at_least(temp_hot, 70), 0, 5))
print("hot-case robustness   : %.1f" % r_hot[0], "-> verdict",
      bool(r_hot[0] >= 0))                         # now NEGATIVE: violated

peak temperature      : 78.0
bound margin at peak  : 2.0
reach margin at t=0   : 8.0
hot-case robustness   : -1.0 -> verdict False

Now the library pair. The production tool for STL runtime monitoring is rtamt, which parses an STL spec written as a string and evaluates its robustness over a signal, handling the windowing, the operator semantics, and online or offline evaluation internally. Code 30.1.3 reproduces the verdict of Code 30.1.1 in a few lines.

import rtamt   # tested with rtamt>=0.4; the evaluate() signature varies by release

# Declare the spec in rtamt's STL string syntax, then evaluate offline.
spec = rtamt.StlDiscreteTimeSpecification()
spec.declare_var('temp', 'float')
spec.spec = '(always[0:19] (temp <= 80)) and (eventually[0:5] (temp >= 70))'
spec.parse()

# Feed the same signal; rtamt returns the robustness trace.
# Newer rtamt releases prefer a dict dataset instead:
#   rob = spec.evaluate({'time': t.tolist(), 'temp': temp.tolist()})
rob = spec.evaluate(['temp', list(zip(t.tolist(), temp.tolist()))])
print("rtamt robustness at t=0 :", rob[0][1])     # matches Code 30.1.1: 2.0

rtamt robustness at t=0 : 2.0

Read the three blocks together. Code 30.1.1 implemented the STL quantitative semantics of subsection one directly, one function per operator. Code 30.1.2 traced the resulting robustness to its binding moment and showed the sign flip under a counterfactual, the numeric example made concrete. Code 30.1.3 reproduced the verdict with rtamt in a fraction of the lines. The payoff is that STL monitoring is not a black box: you can compute robustness by hand, a library computes the same number, and the single signed margin is both a safety verdict and, after the softening of subsection four, a training objective.

6. Exercises

These exercises move from reading formulas, to implementing semantics, to an open design question. Selected solutions appear in Appendix G.