In previous lessons, we saw how to express high-level robotic tasks using temporal logic (LTL/CTL) and how to build finite abstractions or automata from robot motion primitives. In this lesson, the central mathematical object is a (labeled) transition system that models the discrete behavior of the robot and its environment.

A (finite) transition system for robotics is typically written as

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

where:

• \( S \): finite set of states (e.g., cells in a grid decomposition, modes of a manipulator).
• \( S_0 \subseteq S \): set of initial states (e.g., known initial pose region).
• \( \rightarrow \subseteq S \times S \): transition relation, where \( (s,s') \in \rightarrow \) means the robot can move from state \( s \) to \( s' \) in one step.
• \( AP \): a set of atomic propositions (e.g., in_goal, collision).
• \( L : S \to 2^{AP} \): labeling function assigning truth values to propositions in each state.

A state \( s \in S \) is reachable if there exists a finite path from some initial state to \( s \):

\[ s_0 \in S_0,\; s_k = s,\; (s_i,s_{i+1}) \in \rightarrow \text{ for } i=0,\dots,k-1. \]

The set of all reachable states from \( S_0 \) is called the reachable set and is foundational for verifying safety, deadlock-freedom, and task satisfaction.

flowchart TD
  A["Robot dynamics / planner"] --> B["Finite abstraction (transition system)"]
  B --> C["Reachability analysis (forward / backward)"]
  C --> D["Check safety: no 'bad' state reachable"]
  C --> E["Check liveness: is 'goal' eventually reachable?"]
  D --> F["If violated: counterexample path"]
  E --> G["If satisfied: certificate of correctness"]
        

Forward reachability iteratively expands the set of states that can be visited by the robot. Define the post operator for a set of states \( X \subseteq S \) as

\[ \operatorname{Post}(X) = \{ s' \in S \mid \exists s \in X : (s,s') \in \rightarrow \}. \]

Starting from initial states \( S_0 \), we define the sequence \( R_k \) of reachable sets:

\[ R_0 = S_0,\quad R_{k+1} = R_k \cup \operatorname{Post}(R_k). \]

This sequence is monotonically nondecreasing: \( R_0 \subseteq R_1 \subseteq R_2 \subseteq \dots \). In finite state spaces, it stabilizes at a finite step:

\[ \exists N \le |S| \text{ such that } R_N = R_{N+1} = \dots = R^\ast, \]

and the limit \( R^\ast \) is the set of all reachable states.

2.1 Proof of Fixpoint Property (Finite Case)

Theorem. For a finite transition system \( \mathcal{T} = (S, S_0, \rightarrow, AP, L) \), the sequence \( R_k \) defined above stabilizes after at most \( |S| \) steps at a fixpoint \( R^\ast \), and \( R^\ast \) is exactly the set of all reachable states.

Proof.

1. Monotonicity: By definition, \( R_{k+1} = R_k \cup \operatorname{Post}(R_k) \supseteq R_k \).
2. Finite stabilization: Because \( S \) is finite and \( R_k \subseteq S \) for all \( k \), the chain can strictly grow at most \( |S| \) times. Hence \( R_N = R_{N+1} \) for some \( N \le |S| \). Define \( R^\ast = R_N \).
3. Fixpoint: For this \( N \), \( R^\ast = R_N = R_{N+1} = R_N \cup \operatorname{Post}(R_N) \), so \( \operatorname{Post}(R^\ast) \subseteq R^\ast \).
4. All reachable states are in \( R^\ast \). Any path \( s_0,\dots,s_k \) with \( s_0 \in S_0 \) satisfies \( s_i \in R_i \subseteq R^\ast \) by induction: for \( i=0 \), \( s_0 \in S_0 = R_0 \); assuming \( s_i \in R_i \subseteq R^\ast \), we have \( s_{i+1} \in \operatorname{Post}(R_i) \subseteq R_{i+1} \).
5. Only reachable states are in \( R^\ast \). Conversely, elements are added to \( R_k \) only if they are initial or successors of already reachable states, so membership in \( R^\ast \) implies reachability.

Therefore, the fixpoint \( R^\ast \) is exactly the reachable set.

Safety properties of robot behavior often have the form \( \square \varphi \) (LTL) or \( \text{AG } \varphi \) (CTL): “something bad never happens”. A typical example is “the manipulator never enters a collision region”.

Let \( Bad \subseteq S \) denote the set of unsafe states, e.g., those where collision is in \( L(s) \). Instead of exploring forward from \( S_0 \), we can perform backward reachability from \( Bad \) to find all states that can potentially lead to a collision.

Define the pre operator:

\[ \operatorname{Pre}(X) = \{ s \in S \mid \exists s' \in X : (s,s') \in \rightarrow \}. \]

Then define the sequence:

\[ B_0 = Bad,\quad B_{k+1} = B_k \cup \operatorname{Pre}(B_k). \]

Again, this sequence is monotonically nondecreasing and stabilizes at a fixpoint \( B^\ast \). Intuitively, \( B^\ast \) is the set of states that can eventually reach an unsafe state.

Proposition. The safety property “no bad state is reachable from initial states” holds if and only if \( S_0 \cap B^\ast = \emptyset \).

Proof.

• If \( S_0 \cap B^\ast \neq \emptyset \), there is an initial state \( s_0 \) in \( B^\ast \), so by construction of \( B_k \) there is a path from \( s_0 \) to some \( s \in Bad \); safety is violated.
• If safety is violated, some path from \( s_0 \in S_0 \) reaches \( Bad \). Reversing the path, all states on the path are included in some \( B_k \), hence \( s_0 \in B^\ast \) and \( S_0 \cap B^\ast \neq \emptyset \).

In CTL notation, verifying \( \text{AG } \neg collision \) is thus equivalent to checking that no initial state belongs to the backward-reachable set of collision states.

For general temporal-logic specifications, model checking typically proceeds by building an automaton that accepts exactly the behaviors that violate or satisfy the formula, and then forming a product of the robot transition system with this automaton (previous lesson: automata-based planning).

Let \( \mathcal{T} = (S, S_0, \rightarrow, AP, L) \) be the robot transition system, and let \( \mathcal{A}_\varphi \) be a Büchi automaton representing the negation of an LTL formula \( \varphi \). The model-checking construction builds the product \( \mathcal{T} \otimes \mathcal{A}_\varphi \), whose states we denote by \( (s,q) \).

The model-checking problem then reduces to a reachability (or repeated reachability) question on the product:

• Does there exist a reachable cycle visiting an accepting state infinitely often?
• Does there exist a reachable accepting strongly connected component (SCC)?

For safety properties, this simplifies to simple reachability of “bad” product states. The following flow summarizes the process:

flowchart TD
  A["Temporal logic spec phi"] --> B["Build automaton for not phi"]
  B --> C["Product of robot TS and automaton"]
  C --> D["Run reachability / SCC search"]
  D --> E["If accepting state (or SCC) reachable: spec violated"]
  D --> F["If none reachable: spec satisfied"]
        

In robotics, the transition system typically comes from a discretized configuration or state space, while the automaton encodes task-level temporal patterns such as “always avoid obstacles and eventually visit all required regions”.

We now implement reachability on an explicit-state transition system using Python. States are integers, transitions are adjacency lists, and a subset of states is labeled as bad. We compute:

• the set of reachable states from \( S_0 \) (forward),
• the set of states that can reach bad (backward),
• the safety verdict by checking intersection.

from collections import deque

# Explicit transition system for a simple mobile base on a grid
# States are integers 0..N-1; edges encode discrete moves.
N = 8
adj = {
    0: [1, 2],
    1: [3],
    2: [3, 4],
    3: [5],
    4: [5, 6],
    5: [7],
    6: [7],
    7: []
}

S0 = {0}       # initial state
Bad = {6}      # e.g., "collision" region

def forward_reach(adj, S0):
    """Compute R* using BFS-like forward reachability."""
    reachable = set(S0)
    queue = deque(S0)
    while queue:
        s = queue.popleft()
        for s_next in adj.get(s, []):
            if s_next not in reachable:
                reachable.add(s_next)
                queue.append(s_next)
    return reachable

def backward_reach(adj, Bad):
    """Compute B* using reverse edges and backward reachability."""
    # Build reverse adjacency
    radj = {s: [] for s in adj}
    for s, outs in adj.items():
        for s_next in outs:
            radj[s_next].append(s)

    backward = set(Bad)
    queue = deque(Bad)
    while queue:
        s = queue.popleft()
        for s_prev in radj.get(s, []):
            if s_prev not in backward:
                backward.add(s_prev)
                queue.append(s_prev)
    return backward

R_star = forward_reach(adj, S0)
B_star = backward_reach(adj, Bad)

print("Reachable states from S0:", R_star)
print("Backward reachable states to Bad:", B_star)
print("Safety holds?" , S0.isdisjoint(B_star))
      

This code implements exactly the fixpoint computations from Sections 2 and 3, using the standard BFS pattern. For larger robotic abstractions, performance can be improved via symbolic representations (e.g., BDDs) or constraint solvers, but the core reachability idea remains the same.

In C++, we can implement the same reachability routines using STL containers. This snippet uses std::vector for adjacency lists and std::queue for BFS.

#include <iostream>
#include <vector>
#include <queue>
#include <unordered_set>

using AdjList = std::vector<std::vector<int>>;

std::unordered_set<int> forwardReach(const AdjList& adj,
                                      const std::unordered_set<int>& S0) {
    std::unordered_set<int> reachable = S0;
    std::queue<int> q;
    for (int s : S0) q.push(s);

    while (!q.empty()) {
        int s = q.front();
        q.pop();
        for (int s_next : adj[s]) {
            if (reachable.find(s_next) == reachable.end()) {
                reachable.insert(s_next);
                q.push(s_next);
            }
        }
    }
    return reachable;
}

std::unordered_set<int> backwardReach(const AdjList& adj,
                                       const std::unordered_set<int>& Bad) {
    int N = static_cast<int>(adj.size());
    AdjList radj(N);
    for (int s = 0; s < N; ++s) {
        for (int s_next : adj[s]) {
            radj[s_next].push_back(s);
        }
    }

    std::unordered_set<int> backward = Bad;
    std::queue<int> q;
    for (int s : Bad) q.push(s);

    while (!q.empty()) {
        int s = q.front();
        q.pop();
        for (int s_prev : radj[s]) {
            if (backward.find(s_prev) == backward.end()) {
                backward.insert(s_prev);
                q.push(s_prev);
            }
        }
    }
    return backward;
}

int main() {
    AdjList adj = {
        {1, 2},    // 0
        {3},       // 1
        {3, 4},    // 2
        {5},       // 3
        {5, 6},    // 4
        {7},       // 5
        {7},       // 6
        {}         // 7
    };

    std::unordered_set<int> S0 = {0};
    std::unordered_set<int> Bad = {6};

    auto R_star = forwardReach(adj, S0);
    auto B_star = backwardReach(adj, Bad);

    std::cout << "Reachable from S0: ";
    for (int s : R_star) std::cout << s << " ";
    std::cout << std::endl;

    std::cout << "Backward reachable to Bad: ";
    for (int s : B_star) std::cout << s << " ";
    std::cout << std::endl;

    bool safe = (S0.size() == 0);
    for (int s0 : S0) {
        if (B_star.find(s0) != B_star.end()) {
            safe = false;
        }
    }
    std::cout << "Safety holds? " << (safe ? "true" : "false") << std::endl;
    return 0;
}
      

This code structure is suitable for integration into low-level robotic software stacks, where the transition system may come from a discretized planner or a finite-state supervisor.

The same logic can be expressed in Java, using List and Queue. This is useful when building verification tools as part of a larger Java-based robotics framework.

import java.util.*;

public class TransitionSystemReachability {

    public static Set<Integer> forwardReach(List<List<Integer>> adj,
                                             Set<Integer> S0) {
        Set<Integer> reachable = new HashSet<>(S0);
        Queue<Integer> queue = new ArrayDeque<>(S0);

        while (!queue.isEmpty()) {
            int s = queue.poll();
            for (int sNext : adj.get(s)) {
                if (!reachable.contains(sNext)) {
                    reachable.add(sNext);
                    queue.add(sNext);
                }
            }
        }
        return reachable;
    }

    public static Set<Integer> backwardReach(List<List<Integer>> adj,
                                              Set<Integer> bad) {
        int n = adj.size();
        List<List<Integer>> radj = new ArrayList<>(n);
        for (int i = 0; i < n; ++i) {
            radj.add(new ArrayList<>());
        }
        for (int s = 0; s < n; ++s) {
            for (int sNext : adj.get(s)) {
                radj.get(sNext).add(s);
            }
        }

        Set<Integer> backward = new HashSet<>(bad);
        Queue<Integer> queue = new ArrayDeque<>(bad);

        while (!queue.isEmpty()) {
            int s = queue.poll();
            for (int sPrev : radj.get(s)) {
                if (!backward.contains(sPrev)) {
                    backward.add(sPrev);
                    queue.add(sPrev);
                }
            }
        }
        return backward;
    }

    public static void main(String[] args) {
        List<List<Integer>> adj = new ArrayList<>();
        adj.add(Arrays.asList(1, 2)); // 0
        adj.add(Arrays.asList(3));    // 1
        adj.add(Arrays.asList(3, 4)); // 2
        adj.add(Arrays.asList(5));    // 3
        adj.add(Arrays.asList(5, 6)); // 4
        adj.add(Arrays.asList(7));    // 5
        adj.add(Arrays.asList(7));    // 6
        adj.add(Collections.emptyList()); // 7

        Set<Integer> S0 = new HashSet<>(Collections.singletonList(0));
        Set<Integer> Bad = new HashSet<>(Collections.singletonList(6));

        Set<Integer> Rstar = forwardReach(adj, S0);
        Set<Integer> Bstar = backwardReach(adj, Bad);

        System.out.println("Reachable from S0: " + Rstar);
        System.out.println("Backward reachable to Bad: " + Bstar);

        boolean safe = true;
        for (int s0 : S0) {
            if (Bstar.contains(s0)) {
                safe = false;
            }
        }
        System.out.println("Safety holds? " + safe);
    }
}
      

The Java version closely mirrors the Python and C++ implementations, illustrating how reachability algorithms can be ported across languages while preserving their mathematical structure.

In MATLAB, we can represent the transition relation via an adjacency matrix and implement reachability using simple loops. Such scripts can be connected to Simulink by exporting reachable sets or by embedding them in MATLAB Function blocks.

% Adjacency matrix for N = 8 states
N  = 8;
Adj = zeros(N, N);
Adj(1, [2 3]) = 1;  % 0 -> 1,2
Adj(2, 4)     = 1;  % 1 -> 3
Adj(3, [4 5]) = 1;  % 2 -> 3,4
Adj(4, 6)     = 1;  % 3 -> 5
Adj(5, [6 7]) = 1;  % 4 -> 5,6
Adj(6, 8)     = 1;  % 5 -> 7
Adj(7, 8)     = 1;  % 6 -> 7

S0  = [1];   % MATLAB indices for state 0
Bad = [7];   % state 6

% Forward reachability
reachable = false(N, 1);
queue     = S0(:);
reachable(S0) = true;

while ~isempty(queue)
    s = queue(1);
    queue(1) = [];
    succ = find(Adj(s, :) > 0);
    for k = 1:numel(succ)
        sn = succ(k);
        if ~reachable(sn)
            reachable(sn) = true;
            queue(end+1) = sn; %#ok<AGROW>
        end
    end
end

R_star = find(reachable) - 1;  % subtract 1 to get 0-based labels

% Backward reachability
backward = false(N, 1);
queue    = Bad(:);
backward(Bad) = true;

AdjT = Adj.';  % transpose for predecessors

while ~isempty(queue)
    s = queue(1);
    queue(1) = [];
    pred = find(AdjT(s, :) > 0);
    for k = 1:numel(pred)
        sp = pred(k);
        if ~backward(sp)
            backward(sp) = true;
            queue(end+1) = sp; %#ok<AGROW>
        end
    end
end

B_star = find(backward) - 1;

disp('Reachable from S0:');
disp(R_star);
disp('Backward reachable to Bad:');
disp(B_star);

safe = isempty(intersect(S0 - 1, B_star));
disp(['Safety holds? ', num2str(safe)]);

% In Simulink:
% - Use a Stateflow chart or a custom discrete-time model to generate the TS.
% - Export the adjacency matrix and integrate this script for offline verification.
      

For more advanced workflows, Simulink Design Verifier and Stateflow offer native model-checking and test-generation capabilities, which internally rely on similar reachability computations.

For continuous linear systems, reachable sets can be characterized analytically using the matrix exponential. Consider the system

\[ \dot{x}(t) = A x(t) + B u(t), \quad x(0) = x_0. \]

The solution is

\[ x(t) = e^{A t} x_0 + \int_0^t e^{A (t - \tau)} B u(\tau) \, d\tau. \]

If \( u(t) \) is piecewise constant from a finite set of inputs, we can sample at discrete times \( t_k = k h \) and obtain a discrete-time system suitable for reachability analysis. The following Mathematica code computes the reachable set of a simple double integrator under a bounded constant input over a short horizon:

(* Double integrator: x_dot = v, v_dot = u, |u| <= umax *)
A = { {0, 1}, {0, 0} };
B = { {0}, {1} };
umax = 1.0;

(* Discretize with sampling period h *)
h = 0.1;
Ad = MatrixExp[A h];
Bd = Integrate[MatrixExp[A (h - tau)].B, {tau, 0, h}];

(* Initial set: small box around origin *)
X0 = { {-0.1, 0.1}, {-0.1, 0.1} }; (* bounds for x and v *)

(* Enumerate inputs u in {-umax, 0, umax} *)
Uset = {-umax, 0.0, umax};

(* Helper: propagate box with all inputs, overapproximation by convex hull *)
Clear[stepReach];
stepReach[box_] := Module[{xmin, xmax, vmin, vmax, corners, points},
  {xmin, xmax} = box[[1]];
  {vmin, vmax} = box[[2]];
  corners = Tuples[{ {xmin, xmax}, {vmin, vmax} }];
  points = Flatten[
    Table[
      Ad.c + Bd.u,
      {c, corners},
      {u, Uset}
    ],
    1
  ];
  {
    {Min[points[[All, 1]]], Max[points[[All, 1]]]},
    {Min[points[[All, 2]]], Max[points[[All, 2]]]}
  }
];

(* Iterate reachable boxes for K steps *)
K = 10;
boxes = NestList[stepReach, X0, K];

boxes
      

Each element of boxes is a simple axis-aligned overapproximation of the reachable set at time \( k h \). In practice, more precise set representations (e.g., polytopes, zonotopes, ellipsoids) are used, but the core idea of iterating a reachability operator remains the same.

Problem 1 (Fixpoint Stabilization Bound): Let \( \mathcal{T} = (S, S_0, \rightarrow) \) be a finite transition system with \( |S| = n \). Consider the sequence \( R_0 = S_0 \), \( R_{k+1} = R_k \cup \operatorname{Post}(R_k) \). Prove that \( R_k = R_{k+1} \) for some \( k \le n-1 \).

Solution.

The sequence \( (R_k)_{k \ge 0} \) is monotonically nondecreasing and each \( R_k \) is a subset of \( S \). If \( R_k \neq R_{k+1} \), then at least one new state is added: \( |R_{k+1}| > |R_k| \). Since there are only \( n \) states, this can happen at most \( n-1 \) times (starting from \( |R_0| \ge 1 \) if \( S_0 \neq \emptyset \)). Therefore, \( R_k = R_{k+1} \) for some \( k \le n-1 \).

Problem 2 (Backward Reachability and Safety): Let \( Bad \subseteq S \) be an unsafe set, and \( B_0 = Bad \), \( B_{k+1} = B_k \cup \operatorname{Pre}(B_k) \). Prove that a state \( s \in S \) belongs to \( B^\ast = \bigcup_{k \ge 0} B_k \) if and only if there exists a path from \( s \) to some \( b \in Bad \).

Solution.

• (If) Suppose there is a path \( s = s_0, s_1, \dots, s_k = b \) with \( b \in Bad \). Then \( b \in B_0 \). By construction, \( s_{k-1} \in \operatorname{Pre}(B_0) \subseteq B_1 \), \( s_{k-2} \in \operatorname{Pre}(B_1) \subseteq B_2 \), and so on. By induction, \( s = s_0 \in B_k \subseteq B^\ast \).
• (Only if) Suppose \( s \in B^\ast \). Then \( s \in B_k \) for some minimal \( k \). If \( k = 0 \), then \( s \in Bad \), and the path is trivial. If \( k > 0 \), then by the definition of \( B_k \), there exists \( s_1 \in B_{k-1} \) with \( (s,s_1) \in \rightarrow \). By minimality, we can recursively construct a path \( s_1, s_2, \dots, s_m \in Bad \), and concatenating gives a path from \( s \) to \( Bad \).

Problem 3 (Safety Property Verification): Consider the transition system from the Python example with initial set \( S_0 = \{0\} \) and \( Bad = \{6\} \). Compute \( R^\ast \) and \( B^\ast \) by hand and decide whether the safety property “never reach state 6” holds.

Solution.

Forward: From 0, successors are 1,2. From 1, successor is 3. From 2, successors are 3,4. From 3, successor is 5. From 4, successors are 5,6. From 5, successor is 7. From 6, successor is 7. From 7, no successors. Therefore \( R^\ast = \{0,1,2,3,4,5,6,7\} \).

Backward: Start from \( B_0 = \{6\} \). Predecessors of 6 are \( \{4\} \), so \( B_1 = \{4,6\} \). Predecessors of 4 are \( \{2\} \), so \( B_2 = \{2,4,6\} \). Predecessors of 2 are \( \{0\} \), so \( B_3 = \{0,2,4,6\} \). No additional predecessors exist, so \( B^\ast = \{0,2,4,6\} \).

Since \( S_0 \cap B^\ast = \{0\} \neq \emptyset \), the initial state can reach 6 and the safety property is violated. The violating path is, e.g., \( 0 \to 2 \to 4 \to 6 \).

Problem 4 (Product System Size): Let a robot transition system have \( n \) states and a Büchi automaton for the negation of an LTL specification have \( m \) states. Show that the product system has at most \( n \cdot m \) states and discuss implications for model-checking complexity.

Solution.

By construction, each product state is a pair \( (s,q) \) with \( s \in S \) from the robot and \( q \in Q \) from the automaton. Thus, the state space is a subset of the Cartesian product \( S \times Q \), which has cardinality \( |S| \cdot |Q| = n \cdot m \). Some pairs may be unreachable and can be ignored in practice, but the worst-case size is still \( n \cdot m \). Because standard model-checking algorithms are polynomial in the size of the product graph, their complexity becomes \( \mathcal{O}(n \cdot m) \) in the number of states, illustrating the state-explosion problem when both \( n \) and \( m \) grow.

Problem 5 (Linear System Discrete Reachability): Consider the discrete-time linear system

\[ x_{k+1} = A x_k,\quad x_0 \in X_0, \]

where \( A \in \mathbb{R}^{n \times n} \) is fixed and \( X_0 \subseteq \mathbb{R}^n \) is finite. Show that the reachable set \( \{ x_k \mid k \ge 0 \} \) is finite and is contained in the set \( \{ A^k x_0^i \mid 0 \le k \le K,\; x_0^i \in X_0 \} \) for some finite \( K \) if and only if there exist two integers \( p \lt q \) such that \( A^p = A^q \).

Solution.

(If) Suppose \( A^p = A^q \) with \( p \lt q \). Then \( A^{p+k} = A^{q+k} \) for all \( k \ge 0 \) by multiplying on the right by \( A^k \). Hence, for any \( x_0 \), the sequence \( x_k = A^k x_0 \) is ultimately periodic with period \( q-p \). Therefore, the set of all states \( \{ x_k \mid k \ge 0 \} \) is finite and contained in \( \{ A^k x_0 \mid 0 \le k \le q-1 \} \). Taking the union over a finite initial set \( X_0 \) yields finiteness and a suitable \( K \).

(Only if) Conversely, suppose the reachable set from each \( x_0^i \in X_0 \) is finite and contained in \( \{ A^k x_0^i \mid 0 \le k \le K_i \} \). If there were no integers \( p \lt q \) with \( A^p = A^q \), then the sequence \( A^k \) would be infinite and pairwise distinct, and for some \( x_0^i \) the states \( A^k x_0^i \) would also be pairwise distinct, contradicting finiteness. Therefore, equality \( A^p = A^q \) must hold for some \( p \lt q \).

This illustrates how algebraic properties of the system matrix constrain the structure of reachable states and can be exploited in symbolic verification.

In this lesson, we introduced reachability as a central concept in formal verification for robotics. We defined forward and backward reachability on finite transition systems, proved their fixpoint characterizations, and connected them directly to safety verification and automata-based model checking. We saw how model checking reduces to reachability over a product system and implemented core reachability algorithms in Python, C++, Java, MATLAB/Simulink, and Wolfram Mathematica, including an example of continuous linear-system reachability via matrix exponentials. These tools form the basis for correct-by-construction planning, which is the focus of the next lesson.