In classical control and kinematics, specifications are often given as pointwise constraints on state or input, such as \( q(t) \in \mathcal{Q}_{\text{safe}} \) or \( \|u(t)\| \leq u_{\max} \). For high-level autonomy we need temporal specifications over entire executions, for example:

• “Always avoid collision.”
• “Eventually reach the charging station.”
• “Visit region A infinitely often, while never entering region C.”

Let \( AP \) be a finite set of atomic propositions, encoding predicates over robot states, such as \( AP = \{\mathit{goal}, \mathit{collision}, \mathit{inA}, \mathit{inB}\} \). A (discrete) robot execution can be abstracted as a sequence of labels indicating which propositions hold at each time:

\[ (2^{AP})^{\omega} = \{\ \pi = \ell_0\,\ell_1\,\ell_2\,\dotsm \mid \ell_i \subseteq AP \text{ for all } i \ \}, \]

where each \( \ell_i \) describes which regions, goals, or events are true at discrete time step \( i \). A property is then a subset \( \mathcal{P} \subseteq (2^{AP})^{\omega} \).

Temporal logics like LTL and CTL give us a symbolic syntax to describe such sets \( \mathcal{P} \) using logical connectives and temporal operators.

flowchart TD
  A["Task in natural language"] --> B["Define atomic propositions (AP)"]
  B --> C["Write temporal-logic formula (LTL/CTL)"]
  C --> D["Use planner/controller synthesis"]
  D --> E["Execute and monitor on robot"]
        

We work with a discrete-time abstraction of the robot as a labeled transition system. This abstraction can come, for example, from a discretized motion planner graph, a high-level finite-state controller, or an abstraction of a hybrid system.

\[ \mathcal{T} = (S, S_0, \rightarrow, AP, L) \]

• \( S \) is a finite set of states.
• \( S_0 \subseteq S \) is the set of initial states.
• \( \rightarrow \subseteq S \times S \) is the transition relation.
• \( AP \) is the set of atomic propositions.
• \( L : S \rightarrow 2^{AP} \) is a labeling function mapping each state to the set of propositions true there.

A (maximal) run of \( \mathcal{T} \) is an infinite sequence \( \pi = s_0 s_1 s_2 \dotsm \) such that \( s_0 \in S_0 \) and \( (s_i, s_{i+1}) \in \rightarrow \) for all \( i \geq 0 \). The associated label sequence is \( L(\pi) = L(s_0)L(s_1)L(s_2)\dotsm \in (2^{AP})^{\omega} \).

We write \( \pi[i] \) for state \( s_i \) and \( \pi[i..] \) for the suffix \( s_i s_{i+1} s_{i+2} \dotsm \).

Linear Temporal Logic (LTL) describes properties of single infinite runs. Its formulas are built from atomic propositions and temporal operators:

\[ \varphi ::= \top \mid p \mid \neg \varphi \mid \varphi_1 \land \varphi_2 \mid \mathbf{X}\varphi \mid \mathbf{F}\varphi \mid \mathbf{G}\varphi \mid \varphi_1\,\mathbf{U}\,\varphi_2, \]

where \( p \in AP \). Intuitively:

• \( \mathbf{X}\varphi \): “next” — \( \varphi \) holds at the next time step.
• \( \mathbf{F}\varphi \): “eventually” — at some future time, \( \varphi \) holds.
• \( \mathbf{G}\varphi \): “always” — at all future times, \( \varphi \) holds.
• \( \varphi_1\,\mathbf{U}\,\varphi_2 \): “until” — \( \varphi_1 \) holds up to (but not necessarily at) the point where \( \varphi_2 \) first holds.

Common robotic patterns:

• Safety: \( \varphi_{\text{safety}} = \mathbf{G}\neg\mathit{collision} \)
  “Collision never occurs.”
• Reachability: \( \varphi_{\text{reach}} = \mathbf{F}\mathit{goal} \)
  “Eventually the goal is reached.”
• Response: \( \mathbf{G}(\mathit{request} \rightarrow \mathbf{F}\mathit{service}) \)
  “Every request is eventually served.”

LTL formulas are interpreted over runs of the transition system. We write \( (\mathcal{T}, \pi, i) \models \varphi \) to mean that formula \( \varphi \) holds at position \( i \) of run \( \pi \). The semantics is defined inductively:

\[ \begin{aligned} (\mathcal{T}, \pi, i) \models p &\quad \text{iff} \quad p \in L(\pi[i]), \\[0.4em] (\mathcal{T}, \pi, i) \models \neg \varphi &\quad \text{iff} \quad (\mathcal{T}, \pi, i) \not\models \varphi, \\[0.4em] (\mathcal{T}, \pi, i) \models \varphi_1 \land \varphi_2 &\quad \text{iff} \quad (\mathcal{T}, \pi, i) \models \varphi_1 \text{ and } (\mathcal{T}, \pi, i) \models \varphi_2, \\[0.4em] (\mathcal{T}, \pi, i) \models \mathbf{X}\varphi &\quad \text{iff} \quad (\mathcal{T}, \pi, i+1) \models \varphi, \\[0.4em] (\mathcal{T}, \pi, i) \models \mathbf{F}\varphi &\quad \text{iff} \quad \exists j \geq i : (\mathcal{T}, \pi, j) \models \varphi, \\[0.4em] (\mathcal{T}, \pi, i) \models \mathbf{G}\varphi &\quad \text{iff} \quad \forall j \geq i : (\mathcal{T}, \pi, j) \models \varphi, \\[0.4em] (\mathcal{T}, \pi, i) \models \varphi_1\,\mathbf{U}\,\varphi_2 &\quad \text{iff} \quad \exists j \geq i : (\mathcal{T}, \pi, j) \models \varphi_2 \\[-0.2em] &\qquad\qquad\text{and}\quad \forall k\ \text{with}\ i \leq k < j:\ (\mathcal{T}, \pi, k) \models \varphi_1. \end{aligned} \]

A run \( \pi \) of \( \mathcal{T} \) satisfies \( \varphi \) if \( (\mathcal{T}, \pi, 0) \models \varphi \). The system as a whole satisfies \( \varphi \), written \( \mathcal{T} \models \varphi \), if all its runs satisfy \( \varphi \).

In robotic terms, \( \mathcal{T} \models \mathbf{G}\neg\mathit{collision} \) means that the robot is collision-free along every feasible closed-loop execution induced by the model \( \mathcal{T} \).

While LTL looks at a single path at a time, Computation Tree Logic (CTL) treats the future of a state as a branching tree of possibilities. It adds path quantifiers:

• \( \text{A} \): “for all paths starting at this state”.
• \( \text{E} \): “there exists at least one path”.

CTL formulas are evaluated at states and combine these quantifiers with temporal operators. A typical fragment is:

\[ \varphi ::= \top \mid p \mid \neg \varphi \mid \varphi_1 \land \varphi_2 \mid \text{A}\,\mathbf{X}\varphi \mid \text{E}\,\mathbf{X}\varphi \mid \text{A}[\varphi_1\,\mathbf{U}\,\varphi_2] \mid \text{E}[\varphi_1\,\mathbf{U}\,\varphi_2]. \]

Example CTL formulas for robot tasks:

• \( \text{AG}\neg\mathit{collision} \): on all paths, always collision-free.
• \( \text{EF}\mathit{goal} \): there exists a path that eventually reaches the goal.
• \( \text{AG}\,\text{EF}\mathit{goal} \): from every reachable state there exists a path to the goal (robust reachability).

Semantically, for a state \( s \in S \) and formula \( \varphi \), we write \( (\mathcal{T}, s) \models \varphi \). For instance:

\[ \begin{aligned} (\mathcal{T}, s) \models \text{E}\,\mathbf{F}\psi &\quad \text{iff} \quad \exists \pi \in \text{Paths}(s)\ \exists i \geq 0: (\mathcal{T}, \pi[i]) \models \psi, \\[0.4em] (\mathcal{T}, s) \models \text{A}\,\mathbf{G}\psi &\quad \text{iff} \quad \forall \pi \in \text{Paths}(s)\ \forall i \geq 0: (\mathcal{T}, \pi[i]) \models \psi, \end{aligned} \]

where \( \text{Paths}(s) \) is the set of all runs starting from \( s \).

flowchart TD
  S0["state s0"] --> S1a["s1 on path 1"]
  S1a --> S2a["s2 on path 1"]
  S0 --> S1b["s1' on path 2"]
  S1b --> S2b["s2' on path 2"]
  S1a -. "LTL: single-path formula" .-> LTL["evaluate over \nsequence s0,s1,s2,..."]
  S0 -. "CTL: A,E over all paths" .-> CTL["quantify over \nbranching futures"]
        

Both LTL and CTL can express safety and liveness properties, but they take different perspectives:

• LTL: formulas are interpreted over single runs. A system satisfies an LTL formula if all its runs satisfy it. It is natural for specifying behaviors of a single controller.
• CTL: formulas are interpreted over states with branching futures, using path quantifiers. It is natural when the environment or scheduler introduces nondeterministic choices.

Some properties are easy to express in LTL but not in pure CTL, and vice versa. A classical example is the CTL formula \( \text{AG}\,\text{EF}\mathit{goal} \), which says: “from every reachable state there exists a way to eventually reach the goal.” This captures a kind of “controllable reachability” that is not expressible in standard LTL.

In motion planning, LTL is often used to encode a desired single behavior of the closed-loop robot, whereas CTL is central in model checking, where we want to verify a design against all possible environment choices.

We now implement a minimal LTL interpreter on finite prefixes of robot executions. In a robotics pipeline, the transition system could be derived from an OMPL-based roadmap (C++ side) while this Python code runs as a monitor on recorded traces (e.g., via ROS bag files).

from __future__ import annotations
from dataclasses import dataclass
from typing import Set, List, Union, Dict

# --- Representation of a labeled transition system (finite depth) ---

State = str
AtomicProp = str

@dataclass
class TransitionSystem:
    states: Set[State]
    init: State
    edges: Dict[State, List[State]]
    labels: Dict[State, Set[AtomicProp]]

    def run(self, policy, horizon: int) -> List[State]:
        """
        Simulate one run of length 'horizon' under a simple policy.
        'policy' maps current state to a successor state.
        """
        path = [self.init]
        s = self.init
        for _ in range(horizon):
            s = policy(s, self.edges[s])
            path.append(s)
        return path

    def label_trace(self, path: List[State]) -> List[Set[AtomicProp]]:
        return [self.labels[s] for s in path]

# --- LTL formula AST ---

class Formula:
    pass

@dataclass
class AP(Formula):
    name: AtomicProp

@dataclass
class Not(Formula):
    sub: Formula

@dataclass
class And(Formula):
    left: Formula
    right: Formula

@dataclass
class Or(Formula):
    left: Formula
    right: Formula

@dataclass
class Next(Formula):
    sub: Formula

@dataclass
class Until(Formula):
    left: Formula
    right: Formula

@dataclass
class Globally(Formula):
    sub: Formula

@dataclass
class Eventually(Formula):
    sub: Formula

# --- LTL semantics over a finite trace (bounded check) ---

def holds(formula: Formula,
          trace: List[Set[AtomicProp]],
          i: int = 0) -> bool:
    """
    Bounded semantics on a finite trace l_0,...,l_{N-1}.
    For temporal operators that require 'future' steps, we truncate at the end.
    """
    N = len(trace)

    if isinstance(formula, AP):
        return formula.name in trace[i]
    if isinstance(formula, Not):
        return not holds(formula.sub, trace, i)
    if isinstance(formula, And):
        return holds(formula.left, trace, i) and holds(formula.right, trace, i)
    if isinstance(formula, Or):
        return holds(formula.left, trace, i) or holds(formula.right, trace, i)
    if isinstance(formula, Next):
        if i + 1 >= N:
            return False
        return holds(formula.sub, trace, i + 1)
    if isinstance(formula, Globally):
        return all(holds(formula.sub, trace, j) for j in range(i, N))
    if isinstance(formula, Eventually):
        return any(holds(formula.sub, trace, j) for j in range(i, N))
    if isinstance(formula, Until):
        # phi U psi: exists j>=i with psi at j and phi at all k in [i,j)
        for j in range(i, N):
            if holds(formula.right, trace, j):
                if all(holds(formula.left, trace, k) for k in range(i, j)):
                    return True
        return False
    raise TypeError(f"Unknown formula type: {type(formula)}")

# --- Example: small navigation abstraction ---

# States: s0 (start), s1 (corridor), s2 (goal), sx (collision state)
ts = TransitionSystem(
    states={"s0", "s1", "s2", "sx"},
    init="s0",
    edges={
        "s0": ["s1", "sx"],
        "s1": ["s2", "sx"],
        "s2": ["s2"],
        "sx": ["sx"],
    },
    labels={
        "s0": set(),
        "s1": set(),
        "s2": {"goal"},
        "sx": {"collision"},
    },
)

def safe_policy(s: State, succ: List[State]) -> State:
    # Avoid successor states labeled with "collision" if possible
    for t in succ:
        if "collision" not in ts.labels[t]:
            return t
    return succ[0]

path = ts.run(safe_policy, horizon=5)
trace = ts.label_trace(path)

phi_safety = Globally(Not(AP("collision")))
phi_reach_goal = Eventually(AP("goal"))
phi_task = And(phi_safety, phi_reach_goal)

print("Path:", path)
print("Safety holds?", holds(phi_safety, trace))
print("Reach goal holds?", holds(phi_reach_goal, trace))
print("Combined task holds?", holds(phi_task, trace))
      

This simple interpreter lets us test whether a particular closed-loop behavior obeys an LTL specification such as \( \mathbf{G}\neg\mathit{collision} \land \mathbf{F}\mathit{goal} \). Later lessons will connect such specifications to correct-by-construction planners and model checkers.

On the C++ side (typical in OMPL-based or real-time controllers) one can embed temporal-logic monitors into the planning loop. Below is a minimal skeleton for checking a safety property along a discrete trace:

#include <vector>
#include <string>
#include <unordered_set>

using State = std::string;
using AP = std::string;
using Label = std::unordered_set<AP>;

// Finite trace of labels
bool checkGloballyNotCollision(const std::vector<Label>& trace) {
    for (const auto& lab : trace) {
        if (lab.count("collision") != 0) {
            return false;
        }
    }
    return true;
}

// Example integration point: after generating a path in a planner
bool checkTask(const std::vector<Label>& trace) {
    // G !collision  and  F goal
    bool safety = checkGloballyNotCollision(trace);
    bool reachGoal = false;
    for (const auto& lab : trace) {
        if (lab.count("goal") != 0) {
            reachGoal = true;
            break;
        }
    }
    return safety && reachGoal;
}
      

For Java-based robotic frameworks (e.g., for high-level task planners or Android-based robot interfaces), one can use an object-oriented representation of LTL/CTL formulas:

interface Formula { }

final class AP implements Formula {
    public final String name;
    public AP(String name) { this.name = name; }
}

final class Not implements Formula {
    public final Formula sub;
    public Not(Formula sub) { this.sub = sub; }
}

final class And implements Formula {
    public final Formula left, right;
    public And(Formula left, Formula right) {
        this.left = left; this.right = right;
    }
}

// Extend with Next, Globally, Eventually, Until, etc.

import java.util.List;
import java.util.Set;

class LTL {
    public static boolean holds(Formula f,
                                List<Set<String>> trace,
                                int i) {
        if (f instanceof AP) {
            return trace.get(i).contains(((AP) f).name);
        } else if (f instanceof Not) {
            return !holds(((Not) f).sub, trace, i);
        } else if (f instanceof And) {
            And g = (And) f;
            return holds(g.left, trace, i) && holds(g.right, trace, i);
        }
        // Add remaining cases...
        throw new IllegalArgumentException("Unknown formula");
    }
}
      

These skeletons can be connected to motion-planning libraries (such as OMPL in C++) or symbolic task planners in Java, with LTL/CTL used to encode high-level mission constraints.

In Matlab, a discrete abstraction of a robot (e.g. from a Stateflow chart or Simulink controller) can be stored as an adjacency matrix and label sets. The following script checks a bounded-time version of \( \mathbf{G}\neg\mathit{collision} \land \mathbf{F}\mathit{goal} \) along all paths up to a given depth:

% States are 1..n; adjacency matrix A(i,j)=1 if transition i->j allowed
A = [0 1 1 0;
     0 0 1 1;
     0 0 1 0;
     0 0 0 1];
labels = { {}, {}, {'goal'}, {'collision'} };
init = 1;
maxDepth = 5;

function ok = check_trace(seq, labels)
    hasGoal = false;
    for k = 1:numel(seq)
        Lk = labels{seq(k)};
        if ismember('collision', Lk)
            ok = false; return;
        end
        if ismember('goal', Lk)
            hasGoal = true;
        end
    end
    ok = hasGoal;
end

function ok = dfs_all_paths(A, labels, state, depth, seq, maxDepth)
    seq(end+1) = state; %#ok<AGROW>
    if depth == maxDepth
        ok = check_trace(seq, labels);
        return;
    end
    % If no outgoing edges, treat as stutter (stay in same state)
    succ = find(A(state,:) ~= 0);
    if isempty(succ)
        succ = state;
    end
    ok = true;
    for s = succ
        if ~dfs_all_paths(A, labels, s, depth+1, seq, maxDepth)
            ok = false; return;
        end
    end
end

all_ok = dfs_all_paths(A, labels, init, 0, [], maxDepth);
disp(all_ok);
      

Simulink Design Verifier and Simulink Test provide higher-level property blocks where LTL-like patterns can be expressed as assertions, but the above illustrates how to encode temporal properties directly in Matlab.

In Wolfram Mathematica, we can represent the transition system as a graph and define a simple LTL evaluator on traces:

states = {"s0","s1","s2","sx"};
edges = {"s0" -> "s1", "s0" -> "sx",
         "s1" -> "s2", "s1" -> "sx",
         "s2" -> "s2", "sx" -> "sx"};
labels = <|
  "s0" -> {},
  "s1" -> {},
  "s2" -> {"goal"},
  "sx" -> {"collision"}
|>;

ltlHolds[phi_, trace_, i_:1] := Which[
  Head[phi] === "AP",
    MemberQ[labels[trace[[i]]], phi[[1]]],
  Head[phi] === "Not",
    Not@ltlHolds[phi[[1]], trace, i],
  Head[phi] === "And",
    ltlHolds[phi[[1]], trace, i] && ltlHolds[phi[[2]], trace, i],
  Head[phi] === "G",
    And @@ Table[ltlHolds[phi[[1]], trace, k], {k, i, Length[trace]}],
  Head[phi] === "F",
    Or @@ Table[ltlHolds[phi[[1]], trace, k], {k, i, Length[trace]}],
  True,
    (* Extend with other operators as needed *)
    False
];

phiSafety = "G"["Not"["AP"["collision"]]];
phiReach  = "F"["AP"["goal"]];
phiTask   = "And"[phiSafety, phiReach];

exampleTrace = {"s0","s1","s2","s2","s2"};
ltlHolds[phiTask, exampleTrace]
      

Such symbolic encodings are useful in theoretical work and for prototyping new logics for robotic tasks before implementing them in lower-level languages.

Many robotic properties fall into two broad classes: safety (“nothing bad ever happens”) and liveness (“something good eventually happens”).

A property \( \mathcal{P} \subseteq (2^{AP})^{\omega} \) is a safety property if whenever a run violates it, there is a finite prefix that already witnesses the violation. For example, \( \mathbf{G}\neg\mathit{collision} \) is safety: as soon as \( \mathit{collision} \) becomes true, we can stop and know the property is violated.

A property is liveness if no finite prefix suffices to rule it out. The canonical example is \( \mathbf{F}\mathit{goal} \): after any finite prefix without reaching the goal, the next step might still reach it.

Several important equivalences relate temporal operators. First, “eventually” is expressible via “until”:

\[ \mathbf{F}\varphi \equiv \top\,\mathbf{U}\,\varphi. \]

Proof sketch.

• (\( \Rightarrow \)) If \( (\mathcal{T}, \pi, i) \models \mathbf{F}\varphi \), then by definition there exists \( j \geq i \) such that \( (\mathcal{T}, \pi, j) \models \varphi \). For all \( k \) with \( i \leq k < j \), \( \top \) holds trivially, so the condition for \( \top\,\mathbf{U}\,\varphi \) is satisfied.
• (\( \Leftarrow \)) Conversely, if \( (\mathcal{T}, \pi, i) \models \top\,\mathbf{U}\,\varphi \), there exists \( j \geq i \) with \( (\mathcal{T}, \pi, j) \models \varphi \), which is exactly the condition for \( \mathbf{F}\varphi \).

Another pair of dualities is

\[ \mathbf{G}\varphi \equiv \neg \mathbf{F}\neg\varphi, \qquad \mathbf{F}\varphi \equiv \neg \mathbf{G}\neg\varphi. \]

For CTL, there are analogous dualities, e.g. \( \text{AG}\psi \equiv \neg\,\text{EF}\neg\psi \). These equivalences are widely used when transforming specifications into normal forms for model checking and for constructing automata.

Problem 1 (Classifying properties). Let \( AP = \{\mathit{goal}, \mathit{collision}\} \). Consider the following LTL formulas:

1. \( \mathbf{G}\neg\mathit{collision} \)
2. \( \mathbf{F}\mathit{goal} \)
3. \( \mathbf{G}(\mathit{request} \rightarrow \mathbf{F}\mathit{goal}) \)

For each, decide whether it is (primarily) a safety property, liveness property, or a mixture. Justify informally.

Solution.

1. \( \mathbf{G}\neg\mathit{collision} \) is a pure safety property. Any violation appears as soon as \( \mathit{collision} \) becomes true, and this finite prefix suffices to witness violation.
2. \( \mathbf{F}\mathit{goal} \) is a pure liveness property: no finite prefix without \( \mathit{goal} \) can guarantee violation, since the goal could be reached later.
3. \( \mathbf{G}(\mathit{request} \rightarrow \mathbf{F}\mathit{goal}) \) is a response property, which has both safety and liveness aspects. A violation occurs when a particular request is never followed by a goal; this can only be detected in the limit, so the property has an essential liveness component.

Problem 2 (From English to LTL/CTL). A mobile robot must always avoid collisions and infinitely often visit region A. Express this requirement in:

1. LTL over \( AP = \{\mathit{collision}, \mathit{inA}\} \).
2. CTL over the same set of atomic propositions.

Solution.

1. In LTL, a suitable formula is \( \mathbf{G}\neg\mathit{collision} \land \mathbf{G}\mathbf{F}\mathit{inA} \). The subformula \( \mathbf{G}\mathbf{F}\mathit{inA} \) says that from every time instant, \( \mathit{inA} \) will hold again in the future, i.e. region A is visited infinitely often.
2. In CTL, we express the same intuition as \( \text{AG}\neg\mathit{collision} \land \text{AG}\,\text{EF}\mathit{inA} \). Here, \( \text{AG}\neg\mathit{collision} \) enforces safety on all paths, while \( \text{AG}\,\text{EF}\mathit{inA} \) says that from every reachable state there exists a continuation that eventually visits A, which is a branching-time analogue of recurrence.

Problem 3 (Proving an LTL duality). Show that \( \mathbf{G}\varphi \equiv \neg\mathbf{F}\neg\varphi \) for any LTL formula \( \varphi \), using the semantics from Section 4.

Solution.

Fix a transition system \( \mathcal{T} \), run \( \pi \), and position \( i \). By definition,

\[ (\mathcal{T}, \pi, i) \models \mathbf{G}\varphi \quad \text{iff} \quad \forall j \geq i:\ (\mathcal{T}, \pi, j) \models \varphi. \]

Similarly,

\[ (\mathcal{T}, \pi, i) \models \mathbf{F}\neg\varphi \quad \text{iff} \quad \exists j \geq i:\ (\mathcal{T}, \pi, j) \models \neg\varphi. \]

Therefore, \( (\mathcal{T}, \pi, i) \models \neg\mathbf{F}\neg\varphi \) holds iff it is not the case that there exists such a violating \( j \), i.e. iff for all \( j \geq i \), we have \( (\mathcal{T}, \pi, j) \models \varphi \). This is exactly the semantics of \( \mathbf{G}\varphi \), so the equivalence holds.

Problem 4 (Interpreting a CTL formula). Consider the CTL formula \( \text{AG}\,\text{EF}\mathit{goal} \).

1. Give an informal English interpretation.
2. Explain why this property is stronger than simply requiring \( \text{EF}\mathit{goal} \) at the initial state.

Solution.

1. The formula means: “At every reachable state, there exists a path that eventually reaches the goal.” This expresses that no matter where the system finds itself, it is still possible to achieve the goal in the future.
2. The weaker property \( \text{EF}\mathit{goal} \) at the initial state only guarantees the existence of some path to the goal from the initial condition. It does not exclude the possibility that, after taking certain actions, the system might enter a “dead end” from which the goal is no longer reachable. In contrast, \( \text{AG}\,\text{EF}\mathit{goal} \) rules out such dead ends: every reachable state must lie on at least one path that still leads to the goal.

Problem 5 (Simple monitor design). Let \( \varphi = \mathbf{G}\neg\mathit{collision} \land \mathbf{F}\mathit{goal} \). Using the Python-style semantics from Section 7, describe how you would build an online monitor that reads a stream of labels \( \ell_0, \ell_1, \dotsc \) and can:

• Immediately report a violation of the safety part \( \mathbf{G}\neg\mathit{collision} \).
• Report satisfaction of the reachability part \( \mathbf{F}\mathit{goal} \) as soon as it becomes true.

Solution.

Maintain two Boolean flags: \( \mathit{safe} \) initially \( \text{true} \), and \( \mathit{reachedGoal} \) initially \( \text{false} \). For each new label \( \ell_i \):

• If \( \mathit{collision} \in \ell_i \), set \( \mathit{safe} := \text{false} \) and emit a violation: the safety part of \( \varphi \) is irreversibly broken.
• If \( \mathit{goal} \in \ell_i \), set \( \mathit{reachedGoal} := \text{true} \) and emit that the liveness part \( \mathbf{F}\mathit{goal} \) is now satisfied.

This monitor never needs to look back in time and implements the prefix-based nature of safety violations together with the eventual nature of reachability.

In this lesson we introduced temporal logics as a rigorous language for specifying robot behaviors over time. We formalized labeled transition systems as discrete models of robotic executions, defined the syntax and semantics of LTL over runs, and highlighted the branching-time view captured by CTL via path quantifiers. We discussed how typical robotic missions (safety, reachability, recurrence) map to temporal formulas, presented key dualities such as \( \mathbf{G}\varphi \equiv \neg\mathbf{F}\neg\varphi \), and implemented small interpreters in Python, C++, Java, Matlab, and Mathematica. Subsequent lessons will use these logics as the specification layer for automata-based planning and model checking.