In classical motion planning, the pipeline is typically: (i) write an informal goal description, (ii) run a planner (graph-based, sampling-based, or optimization-based), (iii) test whether the resulting trajectory or policy is safe and meets the task. In correct-by-construction planning, we invert parts of this pipeline: we start from a formal specification and an abstract model of the robot and environment, then synthesize a strategy that is guaranteed to satisfy the specification for all admissible behaviors of the environment captured by the model.

At the level of finite abstractions, the generic ingredients are:

• A labeled transition system or game modeling the robot and environment dynamics over a discrete state space.
• A formal specification, typically in linear temporal logic (LTL) or deterministic ω-automata, capturing safety (“nothing bad ever happens”) and liveness (“something good eventually happens”) requirements.
• A synthesis algorithm that computes a winning set of states and a winning strategy over this model such that all closed-loop executions satisfy the specification.

Conceptually, this replaces “plan then verify” by “verify while planning”. The planner is no longer a heuristic search procedure but a construction of a strategy that is correct by design, given the abstraction.

flowchart TD
  Spec["Formal spec (e.g., LTL)"] --> A["Translate spec to automaton"]
  Model["Robot + environment model \n(transition system / game)"] --> B["Compose with spec automaton (product)"]
  A --> B
  B --> C["Solve game / fixed-point computation"]
  C --> Strat["Winning strategy (correct-by-construction)"]
  Strat --> Exec["Execution on physical robot (via interface layer)"]
        

We model the high-level dynamics of a robot in an environment by a labeled transition system. For purely planning problems (no adversarial environment), a nondeterministic labeled transition system suffices:

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

where:

• \(S\): finite set of abstract states (e.g., grid cells, symbolic modes);
• \(S_0 \subseteq S\): set of initial states;
• \(U\): finite set of control actions;
• \(\delta : S \times U \rightrightarrows S\): nondeterministic transition function, mapping a state and action to a (possibly empty) set of successor states;
• \(AP\): finite set of atomic propositions (e.g., "goal", "obstacle", "unsafe");
• \(L : S \to 2^{AP}\): labeling function that assigns to each state the set of atomic propositions true in that state.

A (possibly infinite) run of \(\mathcal{T}\) is a sequence of states \(\rho = s_0 s_1 s_2 \dots\) satisfying:

\[ s_0 \in S_0, \quad \forall k \ge 0 \; \exists u_k \in U : s_{k+1} \in \delta(s_k, u_k). \]

The corresponding word over atomic propositions observed along a run is \(w(\rho) = L(s_0)L(s_1)L(s_2)\dots\in (2^{AP})^\omega\).

To model an explicit adversarial environment (e.g., disturbances, exogenous events), we use a two-player turn-based game structure where the robot (player 1) and environment (player 2) choose actions alternately. A simple form is:

\[ \mathcal{G} = (S, S_0, U_r, U_e, \delta, AP, L), \]

where \(U_r\) and \(U_e\) are finite action sets of the robot and environment, and \(\delta : S \times U_r \times U_e \to S\) is a deterministic transition function. We assume that in each round:

\[ s_{k+1} = \delta(s_k, u^r_k, u^e_k), \]

where \(u^r_k \in U_r\) is chosen by the robot and \(u^e_k \in U_e\) by the environment.

A (robot) strategy is a mapping from non-empty state histories to actions:

\[ \pi : S^+ \to U_r. \]

A strategy \(\pi\) realizes a temporal-logic specification \(\varphi\) from an initial state \(s_0\) if every run of the game resulting from playing \(\pi\) against any environment behavior satisfies \(\varphi\).

In Lessons 2 and 3 you saw that LTL specifications over atomic propositions in \(AP\) can be translated into ω-automata, such as Büchi automata, that recognize exactly those infinite words satisfying the specification. For an LTL formula \(\varphi\), let

\[ \mathcal{A}_\varphi = (Q, q_0, \Sigma, \Delta, F) \]

be a (nondeterministic) Büchi automaton with:

• \(Q\): finite set of automaton states,
• \(q_0 \in Q\): initial automaton state,
• \(\Sigma = 2^{AP}\): input alphabet,
• \(\Delta : Q \times \Sigma \to 2^Q\): transition function, and
• \(F \subseteq Q\): set of accepting states.

A run of the automaton on a word \(w = a_0 a_1 a_2 \dots\) with \(a_k \in \Sigma\) is a sequence \(q_0 q_1 q_2 \dots\) such that \(q_{k+1} \in \Delta(q_k, a_k)\). The run is accepting if it visits states in \(F\) infinitely often.

To enforce a specification \(\varphi\) on a transition system \(\mathcal{T}\), we construct the synchronous product:

\[ \mathcal{P} = \mathcal{T} \otimes \mathcal{A}_\varphi = (S \times Q, S_0 \times \{q_0\}, U, \delta_P, F_P), \]

where the product transition function and accepting set are defined by:

\[ \delta_P((s,q), u) = \{(s',q') \mid s' \in \delta(s,u),\; q' \in \Delta(q, L(s'))\}, \quad F_P = S \times F. \]

A run of \(\mathcal{P}\) projects to a run of the original transition system and simultaneously to a run of the specification automaton. A strategy that ensures Büchi acceptance in \(\mathcal{P}\) from the initial states yields a correct-by-construction strategy for the original system with respect to the specification \(\varphi\).

For full LTL, the resulting Büchi automata may be large, and the associated games are “generalized” ω-regular games. To keep the exposition manageable in this lesson while retaining planning relevance, we now specialize to a practically important fragment: conjunctions of safety and reachability properties.

Consider a common class of high-level tasks of the form:

• Safety: always avoid states labeled as "unsafe" (e.g., collisions, joint-limit violations),
• Reachability: eventually reach some "goal" region (e.g., a target pose or region in C-space).

Let the atomic propositions contain at least "unsafe" and "goal". We define the sets:

\[ \text{Safe} = \{ s \in S \mid \text{"unsafe"} \notin L(s)\}, \quad \text{Goal} = \{ s \in S \mid \text{"goal"} \in L(s)\}. \]

The specification can be written in LTL as \(\varphi = \mathbf{G}\,\text{safe} \wedge \mathbf{F}\,\text{goal}\). For nondeterministic transitions (or a game with adversarial environment), the robot must ensure that all possible successor states stay within a certain invariant set while progress toward the goal is made.

Define the controllable predecessor operator:

\[ \operatorname{Pre}(X) = \{ s \in S \mid \exists u \in U : \delta(s,u) \subseteq X \}. \]

Intuitively, \(\operatorname{Pre}(X)\) consists of states from which the robot has a control action such that all possible next states are contained in \(X\). For the safety + reachability specification, we are interested in the greatest set of states from which the robot can force eventual reach of \(\text{Goal}\) while remaining in \(\text{Safe}\) along all prefixes. We compute a sequence of sets \(W^0, W^1, \dots\) by:

\[ W^0 = \text{Safe} \cap \text{Goal}, \]

\[ W^{k+1} = W^k \cup \big(\text{Safe} \cap \operatorname{Pre}(W^k)\big), \quad k \ge 0. \]

Because the state space \(S\) is finite and the sequence \(W^k\) is monotonically non-decreasing, it stabilizes in finitely many iterations at:

\[ W^\ast = \bigcup_{k \ge 0} W^k. \]

The set \(W^\ast\) is the winning set for the specification \(\mathbf{G}\,\text{safe} \wedge \mathbf{F}\,\text{goal}\): from any initial state \(s_0 \in W^\ast\) there exists a strategy that keeps the system within \(\text{Safe}\) and ensures that some state in \(\text{Goal}\) is eventually reached, regardless of nondeterministic branching of \(\delta\).

The sequence \(W^k\) introduced above can be seen as iterations of a monotone operator on subsets of \(S\). Define:

\[ F(X) = X \cup \big(\text{Safe} \cap \operatorname{Pre}(X)\big). \]

Then \(W^{k+1} = F(W^k)\), and \(W^0 \subseteq W^1 \subseteq \dots\). Because \(F\) is monotone with respect to set inclusion (i.e., \(X \subseteq Y \Rightarrow F(X) \subseteq F(Y)\)), classical fixed-point theory on finite lattices implies:

• The limit \(W^\ast\) exists and is the least fixed point of \(F\) containing \(\text{Safe} \cap \text{Goal}\).
• \(F(W^\ast) = W^\ast\).

We sketch why \(W^\ast\) is exactly the set of winning states.

Soundness. Suppose \(s_0 \in W^\ast\). We construct a strategy \(\pi\) that prescribes a control action at each state in \(W^\ast\). By definition of \(\operatorname{Pre}\), for any \(s \in W^\ast \setminus \text{Goal}\), there exists a control \(u\) such that \(\delta(s,u) \subseteq W^\ast\) and \(\delta(s,u) \cap W^k \neq \emptyset\) for some index \(k\) such that \(s \in W^{k+1} \setminus W^k\). Choosing such a control ensures that the system never leaves \(W^\ast\) and that, at each step where we are not yet in \(\text{Goal}\), we can move to a state that is closer (in terms of iteration index) to the base set \(\text{Safe} \cap \text{Goal}\). As the indices cannot decrease indefinitely, every play consistent with \(\pi\) reaches \(\text{Goal}\) in finitely many steps while staying in \(\text{Safe}\).

Completeness. Conversely, suppose \(s_0 \notin W^\ast\). We show that no strategy can guarantee satisfaction of \(\mathbf{G}\,\text{safe} \wedge \mathbf{F}\,\text{goal}\). Consider the complement \(S \setminus W^\ast\); these states never enter \(\text{Goal}\) through actions that keep the system in \(\text{Safe}\) under all nondeterministic choices. One can define an adversarial environment (or a particular resolution of nondeterminism) that always drives the system to stay within \(S \setminus W^\ast\), thereby either violating safety (reaching an unsafe state) or preventing ever reaching a goal state. Thus, no correct strategy exists from those states, and they must be losing states.

As a result, the fixed-point computation of \(W^\ast\) gives a correct-by-construction characterization of all initial states from which the specification can be satisfied, together with a method to extract a winning strategy.

We now implement the above fixed-point synthesis in Python for a finite gridworld. The robot moves on a rectangular grid with four-neighbor actions. Some cells are obstacles (unsafe), one or more cells are goals, and we compute the winning set and a strategy that satisfies \(\mathbf{G}\,\text{safe} \wedge \mathbf{F}\,\text{goal}\).

from collections import defaultdict, deque

# Grid definition
W, H = 5, 4  # width and height
obstacles = {(1, 1), (2, 1)}
goals = {(4, 3)}
start = (0, 0)

# Actions: up, down, left, right
ACTIONS = {
    "up":    (0, 1),
    "down":  (0, -1),
    "left":  (-1, 0),
    "right": (1, 0),
}

def in_bounds(x, y):
    return 0 <= x < W and 0 <= y < H

# Build state set and transition relation delta(s, u) as a mapping
states = {(x, y) for x in range(W) for y in range(H)}
safe_states = {s for s in states if s not in obstacles}
goal_states = {s for s in states if s in goals}

# Here we use deterministic transitions; for illustration we keep the type "set" of successors
delta = defaultdict(dict)  # delta[s][u] = set of successors

for (x, y) in states:
    for u, (dx, dy) in ACTIONS.items():
        nx, ny = x + dx, y + dy
        if in_bounds(nx, ny):
            succ = (nx, ny)
        else:
            # Invalid moves: stay in place (could model as nondeterministic alternatives)
            succ = (x, y)
        delta[(x, y)][u] = {succ}

def controllable_pre(X):
    """
    Compute Pre(X) = { s | exists u: delta(s,u) subset of X }.
    """
    pre = set()
    for s in safe_states:
        # Skip states already in X to save some work (optional)
        if s in X:
            pre.add(s)
            continue
        for u, succs in delta[s].items():
            # Ensure all successors are in X (nondeterminism-safe)
            if succs and all(sp in X for sp in succs):
                pre.add(s)
                break
    return pre

def winning_set_and_strategy():
    # Fixed-point iteration
    W_set = safe_states & goal_states  # W^0
    while True:
        pre_W = controllable_pre(W_set)
        new_W = W_set | (safe_states & pre_W)
        if new_W == W_set:
            break
        W_set = new_W

    # Synthesize a (memoryless) strategy on winning states
    strategy = {}
    for s in W_set:
        if s in goal_states:
            # Already at goal; we can choose any safe action that keeps us in W_set
            pass
        for u, succs in delta[s].items():
            if succs and all(sp in W_set for sp in succs):
                strategy[s] = u
                break
    return W_set, strategy

W_star, strat = winning_set_and_strategy()

print("Winning set size:", len(W_star))
print("Is start winning?", start in W_star)
print("Strategy at start:", strat.get(start, None))

# Extract one concrete plan from start by following the memoryless strategy
def extract_plan(start_state, strategy, horizon=50):
    if start_state not in strategy:
        return []
    s = start_state
    path = [s]
    for _ in range(horizon):
        if s in goals:
            break
        u = strategy.get(s)
        if u is None:
            break
        succs = delta[s][u]
        # Deterministic choice
        s = next(iter(succs))
        path.append(s)
    return path

plan = extract_plan(start, strat, horizon=50)
print("Plan:", plan)
      

This implementation computes the fixed point \(W^\ast\) and then chooses a memoryless strategy (a function of the current state only). For this class of games (safety + reachability on finite graphs), memoryless strategies are sufficient.

In C++, we can implement the same fixed-point computation using adjacency lists for the transition relation and boolean arrays for safe, goal, and winning states. The following sketch assumes a finite set of states indexed by integers \(\{0, \dots, n-1\}\).

#include <vector>
#include <iostream>
#include <limits>

struct Transition {
    int action_id;
    std::vector<int> succ;  // successors for this (state, action)
};

int main() {
    int n_states = 10;
    int n_actions = 4;

    // For each state, a list of (action, successors)
    std::vector<std::vector<Transition>> delta(n_states);

    // Example: fill delta[s] with transitions (application-specific)
    // ...

    std::vector<bool> safe(n_states, true);
    std::vector<bool> goal(n_states, false);

    // Mark some states as unsafe / goal
    // safe[i] = false for obstacles, goal[i] = true for goals

    // W^0 = Safe ∩ Goal
    std::vector<bool> W(n_states, false);
    for (int s = 0; s < n_states; ++s) {
        if (safe[s] && goal[s]) {
            W[s] = true;
        }
    }

    bool changed = true;
    while (changed) {
        changed = false;
        for (int s = 0; s < n_states; ++s) {
            if (!safe[s] || W[s]) continue;  // skip unsafe or already winning
            bool can_control = false;
            for (const auto &tr : delta[s]) {
                if (tr.succ.empty()) continue;
                bool all_in_W = true;
                for (int sp : tr.succ) {
                    if (!W[sp]) {
                        all_in_W = false;
                        break;
                    }
                }
                if (all_in_W) {
                    can_control = true;
                    break;
                }
            }
            if (can_control) {
                W[s] = true;
                changed = true;
            }
        }
    }

    // Extract a memoryless strategy: for each winning state, choose one action
    std::vector<int> strategy(n_states, -1);
    for (int s = 0; s < n_states; ++s) {
        if (!W[s]) continue;
        for (const auto &tr : delta[s]) {
            if (tr.succ.empty()) continue;
            bool all_in_W = true;
            for (int sp : tr.succ) {
                if (!W[sp]) {
                    all_in_W = false;
                    break;
                }
            }
            if (all_in_W) {
                strategy[s] = tr.action_id;
                break;
            }
        }
    }

    int start_state = 0;
    std::cout << "Is start winning? " << (W[start_state] ? "yes" : "no") << std::endl;
    std::cout << "Strategy at start: " << strategy[start_state] << std::endl;

    return 0;
}
      

In a robotics software stack, the integer states would correspond to abstract nodes (e.g., symbolic poses or configuration cells), and each action_id could be linked to a motion primitive or low-level controller.

A Java implementation follows the same structure, using lists and maps. We again assume integer state indices and a finite number of actions.

import java.util.*;

class Transition {
    int actionId;
    List<Integer> succ;
    Transition(int actionId, List<Integer> succ) {
        this.actionId = actionId;
        this.succ = succ;
    }
}

public class CorrectByConstructionPlanner {

    public static void main(String[] args) {
        int nStates = 10;

        List<List<Transition>> delta = new ArrayList<>(nStates);
        for (int i = 0; i < nStates; ++i) {
            delta.add(new ArrayList<>());
        }

        // TODO: fill delta with transitions

        boolean[] safe = new boolean[nStates];
        boolean[] goal = new boolean[nStates];
        Arrays.fill(safe, true);
        Arrays.fill(goal, false);

        // Mark some states as unsafe / goal
        // safe[i] = false; goal[j] = true; etc.

        // W^0 = Safe ∩ Goal
        boolean[] W = new boolean[nStates];
        for (int s = 0; s < nStates; ++s) {
            W[s] = safe[s] && goal[s];
        }

        boolean changed = true;
        while (changed) {
            changed = false;
            for (int s = 0; s < nStates; ++s) {
                if (!safe[s] || W[s]) continue;
                boolean canControl = false;
                for (Transition tr : delta.get(s)) {
                    if (tr.succ.isEmpty()) continue;
                    boolean allInW = true;
                    for (int sp : tr.succ) {
                        if (!W[sp]) {
                            allInW = false;
                            break;
                        }
                    }
                    if (allInW) {
                        canControl = true;
                        break;
                    }
                }
                if (canControl) {
                    W[s] = true;
                    changed = true;
                }
            }
        }

        int[] strategy = new int[nStates];
        Arrays.fill(strategy, -1);
        for (int s = 0; s < nStates; ++s) {
            if (!W[s]) continue;
            for (Transition tr : delta.get(s)) {
                if (tr.succ.isEmpty()) continue;
                boolean allInW = true;
                for (int sp : tr.succ) {
                    if (!W[sp]) {
                        allInW = false;
                        break;
                    }
                }
                if (allInW) {
                    strategy[s] = tr.actionId;
                    break;
                }
            }
        }

        int startState = 0;
        System.out.println("Is start winning? " + W[startState]);
        System.out.println("Strategy at start: " + strategy[startState]);
    }
}
      

In a Java-based robotic middleware, such a planner could be integrated as a service that publishes discrete actions or waypoints to a lower-level controller.

In MATLAB, we can represent the transition system using adjacency lists or sparse matrices. Below is a function that computes the winning set and a memoryless strategy. A Simulink implementation would typically realize the state machine and strategy as a Stateflow chart or a combination of lookup tables and switching logic.

function [W, strategy] = cbcPlanner(safe, goal, delta)
% safe, goal: logical row vectors of length nStates
% delta: cell array of size nStates
%   delta{s} is a struct array with fields:
%     .actionId : integer
%     .succ     : row vector of successor state indices

nStates = numel(safe);
W = false(1, nStates);

% W^0 = Safe ∩ Goal
W(safe & goal) = true;

changed = true;
while changed
    changed = false;
    for s = 1:nStates
        if ~safe(s) || W(s)
            continue;
        end
        trList = delta{s};
        canControl = false;
        for k = 1:numel(trList)
            succ = trList(k).succ;
            if isempty(succ), continue; end
            if all(W(succ))
                canControl = true;
                break;
            end
        end
        if canControl
            W(s) = true;
            changed = true;
        end
    end
end

strategy = -1 * ones(1, nStates);
for s = 1:nStates
    if ~W(s), continue; end
    trList = delta{s};
    for k = 1:numel(trList)
        succ = trList(k).succ;
        if isempty(succ), continue; end
        if all(W(succ))
            strategy(s) = trList(k).actionId;
            break;
        end
    end
end
end
      

In Simulink/Stateflow, one possible architecture is: a Stateflow chart implements the discrete state machine governed by strategy(s), while continuous dynamics and low-level controllers are modeled in separate Simulink subsystems. The correct-by-construction guarantee applies to the abstract states; an interface layer must ensure that physical motion stays consistent with this abstraction.

Mathematica is convenient for manipulating sets and graphs symbolically. The following code uses lists of states and rules to implement the fixed-point computation:

(* Example finite set of states *)
states = Range[0, 9];

(* Safe and goal sets (boolean functions or explicit lists) *)
safeQ[s_] := MemberQ[states, s] && s =!= 3
goalQ[s_] := s == 9

safeStates = Select[states, safeQ];
goalStates = Select[states, goalQ];

(* Transition relation: list of rules {state, action} -> {succ1, succ2, ...} *)
delta = {
  { {0, 1} -> {1} },
  { {1, 1} -> {2} },
  { {2, 1} -> {5} },
  (* ... fill with problem-specific transitions ... *)
};

(* Helper to get successors for a given state and action *)
Succ[s_, a_] := Module[{rhs},
  rhs = Cases[delta, { {s, a} -> succ_ } :> succ];
  If[rhs === {}, {}, First[rhs]]
];

(* Controllable predecessor operator *)
Pre[X_List] := Module[{setX = X, pre = {}},
  Do[
    If[!safeQ[s], Continue[]];
    (* find any action whose successors are included in X *)
    Module[{actions, found = False},
      actions = Union[First /@ Cases[delta, { {s, a_} -> _ } :> a]];
      Do[
        With[{succs = Succ[s, a]},
          If[succs =!= {} && SubsetQ[setX, succs],
            found = True; Break[];
          ];
        ],
        {a, actions}
      ];
      If[found, pre = Append[pre, s]];
    ],
    {s, safeStates}
  ];
  Union[pre, Intersection[setX, safeStates]]
];

(* Fixed-point iteration *)
W = Intersection[safeStates, goalStates];
While[True,
  newW = Union[W, Pre[W]];
  If[newW === W, Break[]];
  W = newW;
];

Print["Winning set: ", W];

(* Strategy extraction: pick one action per winning state *)
strategy = Association[];
Do[
  If[MemberQ[W, s],
    Module[{actions, chosen = None},
      actions = Union[First /@ Cases[delta, { {s, a_} -> _ } :> a]];
      Do[
        With[{succs = Succ[s, a]},
          If[succs =!= {} && SubsetQ[W, succs],
            chosen = a; Break[];
          ];
        ],
        {a, actions}
      ];
      strategy[s] = chosen;
    ];
  ],
  {s, states}
];

Print["Strategy: ", strategy];
      

Mathematica is particularly useful for prototyping and verifying properties of such algorithms on small models before porting them into a real-time robotics implementation.

Problem 1 (Winning Set on a Small Transition System). Consider the following finite transition system with three states \(S = \{s_0, s_1, s_2\}\) and a single control action \(u\). The transition structure is:

flowchart LR
  S0["s0"] -->|u| S1["s1"]
  S1 -->|u| S1
  S0 -->|u| S2["s2"]
  S2 -->|u| S2
        

States are labeled as follows: \(\text{Safe} = \{s_0, s_1\}\), \(\text{Goal} = \{s_1\}\), and \(s_2\) is unsafe. Compute the winning set \(W^\ast\) for the specification \(\mathbf{G}\,\text{safe} \wedge \mathbf{F}\,\text{goal}\) using the fixed-point equations from Section 4, and decide whether \(s_0\) is a winning initial state.

Solution. We have:

\[ \text{Safe} = \{s_0, s_1\}, \quad \text{Goal} = \{s_1\}. \]

The base set is:

\[ W^0 = \text{Safe} \cap \text{Goal} = \{s_1\}. \]

We now compute \(\operatorname{Pre}(W^0)\). For state \(s_1\), the unique successor under \(u\) is \(s_1\), which is in \(W^0\), so \(s_1 \in \operatorname{Pre}(W^0)\). For \(s_0\), there are two successors under \(u\): \(s_1\) and \(s_2\) (nondeterministic branching). Because \(s_2 \notin W^0\), we have \(\{s_1, s_2\} \not\subseteq W^0\), and thus \(s_0 \notin \operatorname{Pre}(W^0)\).

\[ \operatorname{Pre}(W^0) = \{s_1\}, \quad W^1 = W^0 \cup (\text{Safe} \cap \operatorname{Pre}(W^0)) = \{s_1\}. \]

The sequence has stabilized with \(W^\ast = \{s_1\}\). Hence \(s_0 \notin W^\ast\) and is not a winning state: any strategy (here, the only choice is \(u\)) allows the environment to steer the system to unsafe \(s_2\).

Problem 2 (Monotonicity of the Pre Operator). Let \(\operatorname{Pre}\) be defined as in Section 4. Show that if \(X \subseteq Y \subseteq S\), then \(\operatorname{Pre}(X) \subseteq \operatorname{Pre}(Y)\). Conclude that the operator \(F(X) = X \cup (\text{Safe} \cap \operatorname{Pre}(X))\) is monotone.

Solution. Suppose \(X \subseteq Y\) and take an arbitrary \(s \in \operatorname{Pre}(X)\). By definition of \(\operatorname{Pre}\), there exists \(u \in U\) such that

\[ \delta(s,u) \subseteq X. \]

Since \(X \subseteq Y\), we also have \(\delta(s,u) \subseteq Y\), so the same action \(u\) certifies that \(s \in \operatorname{Pre}(Y)\). Therefore \(\operatorname{Pre}(X) \subseteq \operatorname{Pre}(Y)\), and \(\operatorname{Pre}\) is monotone.

Now consider:

\[ F(X) = X \cup (\text{Safe} \cap \operatorname{Pre}(X)). \]

If \(X \subseteq Y\), then \(\operatorname{Pre}(X) \subseteq \operatorname{Pre}(Y)\) and hence \(\text{Safe} \cap \operatorname{Pre}(X) \subseteq \text{Safe} \cap \operatorname{Pre}(Y)\). Using monotonicity of union, we obtain \(F(X) \subseteq F(Y)\), so \(F\) is a monotone operator on \(2^S\).

Problem 3 (Safety-Only Specifications). Consider a pure safety specification \(\varphi_{\text{s}} = \mathbf{G}\,\text{safe}\), with the same definition of \(\text{Safe}\) as before. Show that the set of states from which the robot can enforce safety forever is the greatest fixed point of the operator

\[ G(X) = \text{Safe} \cap \operatorname{Pre}(X). \]

Give an iterative algorithm to compute this set and argue why an initial state outside this set is losing for safety.

Solution. For safety-only, every state must be kept inside \(\text{Safe}\) at all times. We therefore look for the largest set \(S_{\text{safe}}\) such that from any state in this set the robot has a control action whose successors stay in the set. This is exactly the definition of a greatest fixed point of \(G\).

We compute the descending sequence:

\[ S^0 = S, \quad S^{k+1} = G(S^k) = \text{Safe} \cap \operatorname{Pre}(S^k). \]

Since the sequence is monotonically non-increasing and \(S\) is finite, it stabilizes at some \(S^\ast\) with \(G(S^\ast) = S^\ast\). Any state eliminated from \(S^k\) at some step either violates safety directly (was not in \(\text{Safe}\)) or has no control that keeps all successors within \(S^k\). Hence from such a state, an adversarial environment can force a safety violation in finitely many steps, and the state is losing. Conversely, from any state in \(S^\ast\) the robot can always choose a control that keeps the system inside \(S^\ast\), maintaining safety.

Problem 4 (Relation to Reachability-Based Planning). Let the transition system be deterministic. Show that for deterministic \(\delta\), the definition of \(\operatorname{Pre}(X)\) simplifies to the standard predecessor operator used in backward reachability (only existential quantification over actions, not universal over successors). Explain why nondeterminism (or adversarial environment) forces us to use universal quantification over successors in the definition used in this lesson.

Solution. If \(\delta\) is deterministic, then \(|\delta(s,u)| \in \{0,1\}\). In particular, if \(\delta(s,u) = \{s'\}\), then \(\delta(s,u) \subseteq X\) is equivalent to \(s' \in X\). Therefore,

\[ \operatorname{Pre}(X) = \{ s \in S \mid \exists u \in U : \delta(s,u) \subseteq X \} = \{ s \in S \mid \exists u \in U, s' \in X : \delta(s,u) = \{s'\} \}, \]

which is exactly the usual notion of predecessor used in backward dynamic programming and graph search.

In the nondeterministic or adversarial case, however, a single control \(u\) at state \(s\) may lead to multiple possible successors \(\delta(s,u)\). To ensure the specification holds for all realizations of nondeterminism (i.e., for all environment choices), we must require that all these successors lie in the candidate winning set. This is why the definition uses \(\delta(s,u) \subseteq X\), rather than a single successor membership test.

In this lesson, we formalized correct-by-construction planning as the synthesis of strategies that guarantee satisfaction of temporal-logic specifications on finite transition systems and games. We:

• Modeled robot and environment dynamics as labeled transition systems and game structures.
• Recalled the translation of temporal-logic formulas into ω-automata and the product construction that unifies system and specification.
• Focused on safety + reachability specifications and derived a fixed-point algorithm computing a winning set and a correct-by-construction strategy.
• Sketched rigorous correctness arguments using monotone operators and fixed-point theory.
• Implemented the synthesis algorithm in Python, C++, Java, MATLAB, and Mathematica, illustrating how such methods can be embedded in practical robotic software stacks.

These constructions generalize to richer ω-regular specifications and more complex game structures (e.g., GR(1) fragments, parity conditions), yielding a broad toolkit for synthesizing robot controllers with formal correctness guarantees.