In automata-based planning, the robot and its environment are modeled as a labeled transition system, and high-level tasks are written as temporal logic formulas (introduced in Lesson 2). These formulas are then translated into an ω-automaton (typically a Büchi automaton). Planning becomes a language emptiness problem for the product of the transition system and the automaton.

Let the robot transition system be \( TS = (S, s_0, Act, \rightarrow, AP, L) \), where

• \( S \): finite set of states (discrete configurations or regions),
• \( s_0 \in S \): initial state,
• \( Act \): set of actions,
• \( \rightarrow \subseteq S \times Act \times S \): transition relation,
• \( AP \): set of atomic propositions,
• \( L : S \rightarrow 2^{AP} \): labeling function.

A (finite or infinite) run of the system is a sequence \( \pi = s_0 s_1 s_2 \dots \) such that

\[ \forall i \ge 0:\ \exists a_i \in Act \text{ such that } (s_i, a_i, s_{i+1}) \in \rightarrow. \]

The trace of a run is the infinite word over \( 2^{AP} \) given by

\[ \mathsf{trace}(\pi) = L(s_0)L(s_1)L(s_2)\dots \in (2^{AP})^{\omega}. \]

A temporal logic specification \( \varphi \) (e.g., in LTL) defines a set of acceptable traces \( \mathcal{L}(\varphi) \subseteq (2^{AP})^{\omega} \).

Automata-based planning proceeds in three conceptual steps:

1. Translate the specification \( \varphi \) into an ω-automaton \( \mathcal{A}_{\varphi} \) over the alphabet \( 2^{AP} \).
2. Construct the synchronous product \( TS \otimes \mathcal{A}_{\varphi} \), which is itself an automaton over robot actions.
3. Search for an accepting run in the product; if one exists, extract a discrete plan that guarantees satisfaction of \( \varphi \).

flowchart TD
  A["Robot TS (S, Act, →, AP, L)"] --> C["Product TS x Spec"]
  B["Temporal logic spec phi"] --> D["Omega automaton A_phi"]
  A --> C
  D --> C
  C --> E["Graph search for accepting run"]
  E --> F["Discrete plan satisfying phi"]
        

To use automata-based planning, continuous robot dynamics must be abstracted into a finite transition system. For instance, a planar robot with configuration space \( \mathcal{C} \subset \mathbb{R}^2 \) can be discretized into cells \( S = \{ s_1,\dots,s_n \} \), each corresponding to a region \( C_i \subset \mathcal{C} \). A cell adjacency induces transitions.

Formally, consider a partition \( \{C_i\}_{i=1}^n \) of the free configuration space \( \mathcal{C}_{\mathrm{free}} \). Define

\[ S = \{1,\dots,n\}, \quad L(i) = \{ p \in AP \mid C_i \subseteq \mathsf{Region}(p) \}. \]

The transition relation is given by feasibility of motion primitives or local planners:

\[ (i,a,j) \in \rightarrow \ \Leftrightarrow\ \text{action } a \text{ can move the robot from some } \\ q \in C_i \text{ to some } q' \in C_j \text{ without collision.} \]

Under suitable conditions (e.g., sufficient discretization and robust local controllers), one can prove that any run of the transition system can be refined into a continuous-state trajectory. For this lesson we assume such an abstraction has already been constructed by previous planning layers.

A run \( \pi \) of the transition system satisfies a temporal logic formula \( \varphi \) iff its trace belongs to the language of \( \varphi \):

\[ TS,\pi \models \varphi \quad \Leftrightarrow \quad \mathsf{trace}(\pi) \in \mathcal{L}(\varphi). \]

A Büchi automaton over alphabet \( \Sigma \) is a tuple \( \mathcal{A} = (Q, \Sigma, \delta, Q_0, F) \), where:

• \( Q \) is a finite set of states,
• \( \Sigma \) is a finite alphabet (here \( \Sigma = 2^{AP} \)),
• \( \delta \subseteq Q \times \Sigma \times Q \) is a transition relation,
• \( Q_0 \subseteq Q \) is a set of initial states,
• \( F \subseteq Q \) is a set of accepting states.

An infinite word \( w = \sigma_0 \sigma_1 \sigma_2 \dots \in \Sigma^{\omega} \) is accepted by \( \mathcal{A} \) if there exists a run

\[ \rho = q_0 q_1 q_2 \dots,\quad q_0 \in Q_0,\ \forall i \ge 0:\ (q_i,\sigma_i,q_{i+1}) \in \delta, \]

such that some accepting state is visited infinitely often:

\[ \mathsf{Inf}(\rho) = \{ q \in Q \mid \text{for infinitely many } i,\ q_i = q \}, \quad \mathsf{Inf}(\rho) \cap F \neq \emptyset. \]

The language of \( \mathcal{A} \) is \( \mathcal{L}(\mathcal{A}) \subseteq \Sigma^{\omega} \). For every LTL formula \( \varphi \) over \( AP \), there exists a Büchi automaton \( \mathcal{A}_{\varphi} \) such that

\[ \mathcal{L}(\mathcal{A}_{\varphi}) = \{ w \in (2^{AP})^{\omega} \mid w \models \varphi \}. \]

The translation \( \varphi \mapsto \mathcal{A}_{\varphi} \) is exponential in the length of \( \varphi \), but for many robotic tasks of moderate complexity, the resulting automaton remains tractable.

As a concrete example, consider the LTL formula \( \varphi = \mathbf{F}\,p \) ("eventually \( p \)"). One Büchi automaton over alphabet \( \Sigma = 2^{\{p\}} \) is:

• \( Q = \{q_0,q_1\} \), \( Q_0 = \{q_0\} \), \( F = \{q_1\} \),
• transitions:

  \[ \delta(q_0,\sigma) = \begin{cases} \{q_1\}, & p \in \sigma,\\ \{q_0\}, & p \notin \sigma, \end{cases} \quad \delta(q_1,\sigma) = \{q_1\} \text{ for all } \sigma \subseteq \{p\}. \]

Intuitively, \( q_0 \) represents "have not seen \( p \) yet", and \( q_1 \) represents "have seen \( p \) at least once". Any word that eventually contains \( p \) produces a run that eventually stays in the accepting state \( q_1 \).

Given a robot transition system \( TS = (S, s_0, Act, \rightarrow, AP, L) \) and a Büchi automaton \( \mathcal{A}_{\varphi} = (Q, 2^{AP}, \delta, Q_0, F) \), the product automaton is defined as

\[ TS \otimes \mathcal{A}_{\varphi} = (S \times Q, s_0', Act, \rightarrow', F'), \]

where

• \( s_0' = (s_0, q_0) \) for some \( q_0 \in Q_0 \),
• \( F' = S \times F \),
• the transition relation is given by

  \[ ((s,q), a, (s', q')) \in \rightarrow' \ \Leftrightarrow\ (s,a,s') \in \rightarrow \ \text{ and }\ (q, L(s), q') \in \delta. \]

Thus, the product synchronizes the evolution of the robot (via \( TS \)) with the evolution of the specification (via \( \mathcal{A}_{\varphi} \)) using the labeling \( L \).

A run of the product is a sequence \( (s_0,q_0)(s_1,q_1)(s_2,q_2)\dots \), and it is accepting if its sequence of automaton components \( q_0 q_1 q_2 \dots \) visits \( F \) infinitely often, equivalently if \( (s_i,q_i) \in F' \) infinitely often.

The crucial correctness connection is:

\[ \exists \text{ accepting run of } TS \otimes \mathcal{A}_{\varphi} \ \Leftrightarrow\ \exists \text{ run } \pi \text{ of } TS \text{ such that } TS,\pi \models \varphi. \]

Intuitively, projecting an accepting product run onto the \( S \)-component yields a robot run whose trace is accepted by \( \mathcal{A}_{\varphi} \), hence satisfies \( \varphi \).

flowchart LR
  S["TS state s in S"] --- Q["Spec state q in Q"]
  SQ["Product state (s,q)"]:::prod
  S --> SQ
  Q --> SQ
  classDef prod stroke-width:3px;
        

The automata-based planning problem reduces to detecting an accepting run in the product automaton. A standard representation is a lasso:

\[ (s_0,q_0) \dots (s_k,q_k)\ (s_{k+1},q_{k+1}) \dots (s_{m},q_{m}), \]

where \( (s_k,q_k) = (s_m,q_m) \) is an accepting state and the suffix from \( k \) to \( m \) is a cycle. Repeating the suffix infinitely many times yields an accepting infinite run.

A typical algorithm:

1. Construct \( TS \otimes \mathcal{A}_{\varphi} \).
2. Compute the set of reachable states from \( s_0' \) via BFS/DFS.
3. Restrict to reachable accepting states \( F'_{\mathrm{reach}} \).
4. On the reachable subgraph, compute strongly connected components (SCCs).
5. Any SCC that contains an accepting state and has a cycle reachable from \( s_0' \) corresponds to an accepting run; extract a prefix path and a cycle.

Complexity: if \( |S| = n \) and \( |Q| = m \), then the product has at most \( nm \) states. The graph search (BFS/DFS + SCC detection via, e.g., Tarjan's algorithm) runs in time

\[ \mathcal{O}(|S||Q| + |\rightarrow'||), \]

which is polynomial in the size of the product (but exponential in the size of the formula due to the automaton construction).

The discrete plan is obtained by projecting the accepting lasso onto robot states and actions, and then refined into a continuous trajectory by the lower-level planners from earlier chapters.

We now implement a minimal automata-based planner in Python for a grid-world robot with specification \( \varphi = \mathbf{F}\,p \) ("eventually reach a goal cell"). For larger systems, these structures would be generated from ROS/OMPL-based planners, but the core logic is the same.

from collections import defaultdict, deque
from typing import Dict, Set, Tuple, List

State = Tuple[int, int]  # grid coordinates (i, j)

class TransitionSystem:
    def __init__(self):
        self.states: Set[State] = set()
        self.initial: State = None
        self.actions = ["up", "down", "left", "right"]
        self.transitions: Dict[Tuple[State, str], Set[State]] = defaultdict(set)
        self.ap: Set[str] = {"goal", "unsafe"}
        self.label: Dict[State, Set[str]] = dict()

    def add_state(self, s: State, is_initial: bool = False,
                  props: Set[str] = None):
        self.states.add(s)
        if is_initial:
            self.initial = s
        self.label[s] = set(props) if props is not None else set()

    def add_transition(self, s: State, a: str, s_next: State):
        self.transitions[(s, a)].add(s_next)

class BuchiAutomaton:
    def __init__(self):
        # For phi = F goal
        self.states: Set[str] = {"q0", "q1"}
        self.initial: str = "q0"
        self.accepting: Set[str] = {"q1"}

    def delta(self, q: str, sigma: Set[str]) -> str:
        has_goal = "goal" in sigma
        if q == "q0":
            return "q1" if has_goal else "q0"
        else:
            # q1 is absorbing
            return "q1"

def build_grid_ts(width: int, height: int,
                  obstacles: Set[State],
                  goal: State,
                  start: State) -> TransitionSystem:
    ts = TransitionSystem()
    for i in range(height):
        for j in range(width):
            s = (i, j)
            if s in obstacles:
                continue
            props = set()
            if s == goal:
                props.add("goal")
            ts.add_state(s, is_initial=(s == start), props=props)

    # 4-neighborhood
    dirs = {"up": (-1, 0), "down": (1, 0),
            "left": (0, -1), "right": (0, 1)}
    for s in ts.states:
        i, j = s
        for a, (di, dj) in dirs.items():
            s_next = (i + di, j + dj)
            if s_next in ts.states:
                ts.add_transition(s, a, s_next)
    return ts

def product_initial(ts: TransitionSystem, ba: BuchiAutomaton):
    return (ts.initial, ba.initial)

def product_successors(ts: TransitionSystem, ba: BuchiAutomaton,
                       s_prod: Tuple[State, str]) -> List[Tuple[Tuple[State, str], str]]:
    (s, q) = s_prod
    result = []
    for a in ts.actions:
        for s_next in ts.transitions.get((s, a), []):
            sigma = ts.label[s]
            q_next = ba.delta(q, sigma)
            result.append(((s_next, q_next), a))
    return result

def find_accepting_lasso(ts: TransitionSystem, ba: BuchiAutomaton):
    start = product_initial(ts, ba)
    # BFS for reachable states and predecessor map
    queue = deque([start])
    pred: Dict[Tuple[State, str], Tuple[Tuple[State, str], str]] = {}
    visited = {start}
    accepting_states = set()

    while queue:
        cur = queue.popleft()
        (s, q) = cur
        if q in ba.accepting:
            accepting_states.add(cur)
        for nxt, act in product_successors(ts, ba, cur):
            if nxt not in visited:
                visited.add(nxt)
                pred[nxt] = (cur, act)
                queue.append(nxt)

    if not accepting_states:
        return None  # no plan

    # For simplicity, pick one accepting state and search for a cycle to itself
    acc = next(iter(accepting_states))

    # DFS within visited states to find a cycle starting and ending at acc
    def dfs_cycle(cur, target, visited_local, path):
        if cur == target and path:
            return path
        visited_local.add(cur)
        for nxt, act in product_successors(ts, ba, cur):
            if nxt not in visited or nxt not in visited_local:
                res = dfs_cycle(nxt, target, visited_local, path + [(nxt, act)])
                if res is not None:
                    return res
        return None

    # Recover prefix to acc
    prefix_states_actions = []
    cur = acc
    while cur != start:
        prev, act = pred[cur]
        prefix_states_actions.append((cur, act))
        cur = prev
    prefix_states_actions.reverse()

    cycle = dfs_cycle(acc, acc, set(), [])
    if cycle is None:
        return None  # no lasso found

    return start, prefix_states_actions, cycle

if __name__ == "__main__":
    width, height = 4, 3
    obstacles = {(1, 1)}
    goal = (0, 3)
    start = (2, 0)
    ts = build_grid_ts(width, height, obstacles, goal, start)
    ba = BuchiAutomaton()
    lasso = find_accepting_lasso(ts, ba)
    if lasso is None:
        print("No plan satisfying F(goal) found.")
    else:
        start, prefix, cycle = lasso
        print("Prefix:")
        print(prefix)
        print("Cycle:")
        print(cycle)
      

This code performs explicit product construction on-the-fly and searches for an accepting lasso. In a full robotic stack, the transition system would be generated from a motion planner (e.g., OMPL), and low-level controllers would track the discrete plan.

In C++, we can represent the product graph explicitly and reuse generic graph-search routines. The snippet below illustrates core structures and a BFS from the initial product state; integration with OMPL or other planning libraries would populate the transition system.

#include <iostream>
#include <vector>
#include <queue>
#include <map>
#include <set>
#include <utility>

struct State2D {
    int i, j;
    bool operator<(const State2D& other) const {
        if (i != other.i) return i < other.i;
        return j < other.j;
    }
    bool operator==(const State2D& other) const {
        return i == other.i && j == other.j;
    }
};

struct TS {
    std::set<State2D> states;
    State2D initial;
    std::vector<std::string> actions{"up", "down", "left", "right"};
    std::map<std::pair<State2D,std::string>, std::set<State2D> > trans;
    std::map<State2D, std::set<std::string> > label;
};

struct Buchi {
    // F goal
    std::set<std::string> states{"q0", "q1"};
    std::string initial{"q0"};
    std::set<std::string> accepting{"q1"};

    std::string delta(const std::string& q,
                      const std::set<std::string>& sigma) const {
        bool has_goal = sigma.find("goal") != sigma.end();
        if (q == "q0") {
            return has_goal ? "q1" : "q0";
        } else {
            return "q1";
        }
    }
};

using ProdState = std::pair<State2D,std::string>;

struct ProdStateLess {
    bool operator()(const ProdState& a, const ProdState& b) const {
        if (a.first < b.first) return true;
        if (b.first < a.first) return false;
        return a.second < b.second;
    }
};

std::vector<std::pair<ProdState,std::string> >
productSuccessors(const TS& ts, const Buchi& ba,
                  const ProdState& ps) {
    std::vector<std::pair<ProdState,std::string> > out;
    const State2D& s = ps.first;
    const std::string& q = ps.second;
    auto it_label = ts.label.find(s);
    const std::set<std::string>& sigma =
        (it_label != ts.label.end()) ? it_label->second
                                     : *new std::set<std::string>();
    for (const auto& act : ts.actions) {
        auto it = ts.trans.find(std::make_pair(s, act));
        if (it == ts.trans.end()) continue;
        for (const auto& s_next : it->second) {
            std::string q_next = ba.delta(q, sigma);
            out.push_back({ProdState{s_next, q_next}, act});
        }
    }
    return out;
}

int main() {
    TS ts;
    // Here you would fill ts.states, ts.initial, ts.trans, ts.label

    Buchi ba;
    ProdState start{ts.initial, ba.initial};

    std::queue<ProdState> q;
    std::set<ProdState,ProdStateLess> visited;
    q.push(start);
    visited.insert(start);

    while (!q.empty()) {
        ProdState cur = q.front(); q.pop();
        const std::string& q_ba = cur.second;
        bool is_accepting = ba.accepting.find(q_ba) != ba.accepting.end();
        if (is_accepting) {
            std::cout << "Found reachable accepting product state" << std::endl;
            break;
        }
        for (auto& succ : productSuccessors(ts, ba, cur)) {
            const ProdState& nxt = succ.first;
            if (visited.find(nxt) == visited.end()) {
                visited.insert(nxt);
                q.push(nxt);
            }
        }
    }
    return 0;
}
      

Extending this snippet with SCC computation and path reconstruction yields a complete C++ implementation of the automata-based planner. The transition system can be obtained from a motion-planning library such as OMPL.

In Java, graph libraries such as JGraphT can be used to represent the product automaton. Below is a core logic sketch using basic collections.

import java.util.*;

class State2D {
    public final int i, j;
    public State2D(int i, int j) { this.i = i; this.j = j; }

    @Override
    public boolean equals(Object o) {
        if (!(o instanceof State2D)) return false;
        State2D s = (State2D) o;
        return i == s.i && j == s.j;
    }

    @Override
    public int hashCode() { return Objects.hash(i, j); }
}

class TransitionSystem {
    Set<State2D> states = new HashSet<>();
    State2D initial;
    List<String> actions = Arrays.asList("up", "down", "left", "right");
    Map<State2D, Set<String>> label = new HashMap<>();
    Map<String, Set<State2D>> successors = new HashMap<>();

    void addState(State2D s, boolean isInitial, Set<String> props) {
        states.add(s);
        if (isInitial) initial = s;
        label.put(s, new HashSet<>(props));
    }

    void addTransition(State2D s, String act, State2D sNext) {
        String key = s.i + "," + s.j + ":" + act;
        successors.computeIfAbsent(key, k -> new HashSet<>()).add(sNext);
    }

    Set<State2D> getSuccessors(State2D s, String act) {
        String key = s.i + "," + s.j + ":" + act;
        return successors.getOrDefault(key, Collections.emptySet());
    }
}

class Buchi {
    String initial = "q0";
    Set<String> accepting = new HashSet<>(Arrays.asList("q1"));

    String delta(String q, Set<String> sigma) {
        boolean hasGoal = sigma.contains("goal");
        if (q.equals("q0")) {
            return hasGoal ? "q1" : "q0";
        } else {
            return "q1";
        }
    }
}

class ProdState {
    final State2D s;
    final String q;
    ProdState(State2D s, String q) { this.s = s; this.q = q; }

    @Override
    public boolean equals(Object o) {
        if (!(o instanceof ProdState)) return false;
        ProdState p = (ProdState) o;
        return s.equals(p.s) && q.equals(p.q);
    }

    @Override
    public int hashCode() { return Objects.hash(s, q); }
}

public class AutomataPlanner {
    static List<ProdState> bfsToAccepting(TransitionSystem ts, Buchi ba) {
        ProdState start = new ProdState(ts.initial, ba.initial);
        Queue<ProdState> q = new ArrayDeque<>();
        Map<ProdState, ProdState> pred = new HashMap<>();
        q.add(start);
        Set<ProdState> visited = new HashSet<>();
        visited.add(start);

        ProdState accepting = null;
        while (!q.isEmpty()) {
            ProdState cur = q.remove();
            if (ba.accepting.contains(cur.q)) {
                accepting = cur;
                break;
            }
            for (String act : ts.actions) {
                for (State2D sNext : ts.getSuccessors(cur.s, act)) {
                    String qNext = ba.delta(cur.q, ts.label.get(cur.s));
                    ProdState nxt = new ProdState(sNext, qNext);
                    if (!visited.contains(nxt)) {
                        visited.add(nxt);
                        pred.put(nxt, cur);
                        q.add(nxt);
                    }
                }
            }
        }

        if (accepting == null) return Collections.emptyList();

        List<ProdState> path = new ArrayList<>();
        ProdState cur = accepting;
        while (cur != null) {
            path.add(cur);
            cur = pred.get(cur);
        }
        Collections.reverse(path);
        return path;
    }

    public static void main(String[] args) {
        TransitionSystem ts = new TransitionSystem();
        // Populate ts with grid states and transitions...
        Buchi ba = new Buchi();
        List<ProdState> plan = bfsToAccepting(ts, ba);
        if (plan.isEmpty()) {
            System.out.println("No satisfying plan");
        } else {
            System.out.println("Found path length = " + plan.size());
        }
    }
}
      

SCC computation and lasso extraction can be added similarly. In practice, TS would come from an upstream planner or simulator.

MATLAB provides convenient graph and digraph types for representing transition systems. In Simulink, Stateflow charts can encode the Büchi automaton, with transitions guarded by atomic propositions. Below is a basic MATLAB function for product exploration.

function prefix = automata_based_plan(ts, ba)
% ts: struct with fields:
%   states: N-by-2 matrix of grid coordinates
%   initial: 1-by-2 initial coordinate
%   actions: cell array of action names
%   trans: containers.Map with key '"i,j:act"' and value: M-by-2 successors
%   label: containers.Map from '"i,j"' to cell array of propositions
%
% ba: struct implementing F(goal) Buchi with:
%   initial: 'q0'
%   accepting: {'q1'}

start = {ts.initial, ba.initial}; % cell: { [i j], 'q' }

visited = containers.Map();
queue = {};
pred = containers.Map();

key = key_prod(start{1}, start{2});
visited(key) = true;
queue{end+1} = start;

acc_key = '';
while ~isempty(queue)
    cur = queue{1};
    queue(1) = [];
    s = cur{1}; q = cur{2};
    if any(strcmp(ba.accepting, q))
        acc_key = key_prod(s, q);
        break;
    end
    lbl_key = sprintf('%d,%d', s(1), s(2));
    if isKey(ts.label, lbl_key)
        sigma = ts.label(lbl_key);
    else
        sigma = {};
    end
    for a_idx = 1:numel(ts.actions)
        act = ts.actions{a_idx};
        t_key = sprintf('%d,%d:%s', s(1), s(2), act);
        if ~isKey(ts.trans, t_key), continue; end
        succs = ts.trans(t_key); % K-by-2
        for k = 1:size(succs,1)
            s_next = succs(k,:);
            q_next = buchi_delta(ba, q, sigma);
            nxt_key = key_prod(s_next, q_next);
            if ~isKey(visited, nxt_key)
                visited(nxt_key) = true;
                queue{end+1} = {s_next, q_next}; %#ok<AGROW>
                pred(nxt_key) = struct('s', s, 'q', q);
            end
        end
    end
end

if isempty(acc_key)
    prefix = {};
    return;
end

% reconstruct prefix from acc_key to start
path = {};
cur_key = acc_key;
while true
    entry = split(cur_key, ';');
    s = sscanf(entry{1}, '%d,%d');
    q = entry{2};
    path{end+1} = {s.', q}; %#ok<AGROW>
    if strcmp(cur_key, key_prod(ts.initial, ba.initial))
        break;
    end
    prev = pred(cur_key);
    cur_key = key_prod(prev.s, prev.q);
end
path = fliplr(path);
prefix = path;
end

function q_next = buchi_delta(ba, q, sigma)
has_goal = any(strcmp(sigma, 'goal'));
if strcmp(q, 'q0')
    if has_goal, q_next = 'q1'; else, q_next = 'q0'; end
else
    q_next = 'q1';
end
end

function k = key_prod(s, q)
k = sprintf('%d,%d;%s', s(1), s(2), q);
end
      

In Simulink, the transition system can be simulated as a discrete-time subsystem, while a Stateflow chart implements the Büchi automaton. A MATLAB Function block can then execute the product-search logic online or offline to generate a plan.

Mathematica has strong support for graphs and symbolic manipulation, making it useful for prototyping automata-based planners.

(* Transition system *)
tsStates = { {0, 0}, {0, 1}, {1, 0}, {1, 1} };
tsInitial = {0, 0};
goal = {1, 1};
labels = Association[
  {0, 0} -> {}, {0, 1} -> {}, {1, 0} -> {}, {1, 1} -> {"goal"}
];

tsEdges = Flatten@Table[
   With[{s = tsStates[[k]], t = tsStates[[l]]},
    If[Norm[s - t, 1] == 1, {s -> t}, {}]
   ],
   {k, Length[tsStates]}, {l, Length[tsStates]}
];
tsGraph = Graph[tsEdges];

(* Buchi for F(goal) with states q0, q1 *)
buchiDelta[q_, sigma_] :=
  Which[
    q === "q0" && MemberQ[sigma, "goal"], "q1",
    q === "q0", "q0",
    True, "q1"
  ];

(* On-the-fly product search for a path reaching accepting state (s,q1) *)
Clear[productSuccessors];
productSuccessors[{s_, q_}] :=
  Module[{sigma = Lookup[labels, s, {}], qnext, succStates},
    qnext = buchiDelta[q, sigma];
    succStates = VertexOutNeighbors[tsGraph, s];
    Table[{t, qnext}, {t, succStates}]
  ];

bfs[start_] :=
  Module[{queue = {start}, visited = <||>, pred = <||>, acc = None},
    visited[start] = True;
    While[queue =!= {} && acc === None,
      {s, q} = First[queue]; queue = Rest[queue];
      If[q === "q1", acc = {s, q}; Break[]];
      Do[
        If[!KeyExistsQ[visited, nxt],
          visited[nxt] = True;
          pred[nxt] = {s, q};
          queue = Append[queue, nxt];
        ],
        {nxt, productSuccessors[{s, q}]}
      ];
    ];
    If[acc === None, {},
      (* reconstruct path *)
      NestWhileList[pred, acc, KeyExistsQ[pred, #] &] // Reverse
    ]
  ];

startProd = {tsInitial, "q0"};
prefix = bfs[startProd];
prefix
      

Symbolic tools can also be used to inspect and manipulate temporal logic formulas and derived automata, facilitating theoretical exploration of automata-based planning algorithms.

Problem 1 (Product Automaton Size Bound). Let \( TS = (S, s_0, Act, \rightarrow, AP, L) \) and \( \mathcal{A}_{\varphi} = (Q, 2^{AP}, \delta, Q_0, F) \). Prove that the product automaton \( TS \otimes \mathcal{A}_{\varphi} \) has at most \( |S|\cdot|Q| \) states and at most \( |\rightarrow|\cdot \max_{q,\sigma}|\delta(q,\sigma)| \) transitions.

Solution. By definition, the state set of the product is \( S \times Q \), so

\[ |S \times Q| = |S|\cdot|Q|. \]

Each product transition corresponds to a pair of transitions: one in \( TS \) and one in \( \mathcal{A}_{\varphi} \). For any \( (s,a,s') \in \rightarrow \), the number of possible automaton successors is at most \( \max_{q,\sigma} |\delta(q,\sigma)| \) (since the label \( \sigma = L(s) \) is fixed and \( q \) ranges over \( Q \)). Hence, the total number of product transitions is bounded by

\[ |\rightarrow'| \le |\rightarrow| \cdot \max_{q,\sigma}|\delta(q,\sigma)|. \]

Problem 2 (Soundness of Automata-Based Planning). Show that if there exists an accepting run of \( TS \otimes \mathcal{A}_{\varphi} \), then there exists a run \( \pi \) of \( TS \) such that \( TS,\pi \models \varphi \).

Solution. Let \( \rho = (s_0,q_0)(s_1,q_1)(s_2,q_2)\dots \) be an accepting run of the product. By the definition of product transitions, for each \( i \ge 0 \) there exists \( a_i \in Act \) such that \( (s_i,a_i,s_{i+1}) \in \rightarrow \) and \( (q_i, L(s_i), q_{i+1}) \in \delta \). Therefore, \( s_0 s_1 s_2 \dots \) is a run \( \pi \) of \( TS \), and the word \( w = \mathsf{trace}(\pi) \) induces the automaton run \( q_0 q_1 q_2 \dots \) in \( \mathcal{A}_{\varphi} \). The run is accepting, so by the definition of Büchi acceptance,

\[ w \in \mathcal{L}(\mathcal{A}_{\varphi}). \]

By the correctness of the LTL-to-automaton translation, \( \mathcal{L}(\mathcal{A}_{\varphi}) = \{w \mid w \models \varphi\} \), so \( w \models \varphi \). Hence \( TS,\pi \models \varphi \), establishing soundness.

Problem 3 (Completeness under Exact Abstraction). Assume the abstraction is exact, in the sense that for every run \( \pi \) of \( TS \) there exists a continuous robot trajectory realizing it, and that the LTL-to-Büchi translation is language-equivalent. Prove that if there exists a run \( \pi \) of \( TS \) such that \( TS,\pi \models \varphi \), then there exists an accepting run of \( TS \otimes \mathcal{A}_{\varphi} \).

Solution. Let \( \pi = s_0 s_1 s_2 \dots \) be a run of \( TS \) with \( TS,\pi \models \varphi \). Then \( w = \mathsf{trace}(\pi) \) satisfies \( w \models \varphi \), so

\[ w \in \mathcal{L}(\mathcal{A}_{\varphi}). \]

Hence there exists an accepting run \( q_0 q_1 q_2 \dots \) of \( \mathcal{A}_{\varphi} \) on \( w \), i.e., \( q_0 \in Q_0 \) and \( (q_i, L(s_i), q_{i+1}) \in \delta \) for all \( i \ge 0 \), and some accepting state in \( F \) appears infinitely often. Therefore, \( (s_0,q_0)(s_1,q_1)(s_2,q_2)\dots \) is a run of the product automaton, and since the automaton component is accepting, the product run is accepting. This proves completeness.

Problem 4 (Example: F(goal) for a Line World). Consider a line world with states \( S = \{0,1,2,3\} \), transitions \( i \rightarrow i+1 \) for \( i = 0,1,2 \), and labeling \( L(3) = \{p\} \), \( L(i) = \emptyset \) for \( i \neq 3 \). Let \( \varphi = \mathbf{F}\,p \). Construct explicitly the product automaton and give a lasso corresponding to a satisfying plan.

Solution. The Büchi automaton for \( \mathbf{F}\,p \) has states \( q_0,q_1 \) as in Section 3. The product states are pairs \( (i,q_j) \) with \( i \in \{0,1,2,3\} \), \( j \in \{0,1\} \). The initial state is \( (0,q_0) \) because \( s_0 = 0 \) and \( q_0 \in Q_0 \).

The labeling ensures that for \( i \neq 3 \), \( \delta(q_0,L(i)) = q_0 \), while at \( i = 3 \), \( \delta(q_0,L(3)) = q_1 \) and \( \delta(q_1,L(3)) = q_1 \). The product transitions mirror the line:

• \( (0,q_0) \rightarrow' (1,q_0) \rightarrow' (2,q_0) \rightarrow' (3,q_1) \),
• and from \( (3,q_1) \), self-loops \( (3,q_1) \rightarrow' (3,q_1) \).

A lasso is given by the prefix \( (0,q_0)(1,q_0)(2,q_0)(3,q_1) \) followed by the cycle \( (3,q_1)(3,q_1) \). Repeating the self-loop infinitely many times yields an accepting run; the projected plan moves the robot from 0 to 3 and then stays at 3.

Problem 5 (Prefix-Suffix Structure). Explain why any accepting run of a finite product automaton can be written in prefix-suffix (lasso) form and outline how this structure is used to generate an infinite-horizon plan.

Solution. The product automaton has a finite number of states. Consider an accepting run \( \rho = x_0 x_1 x_2 \dots \). Since \( F' \neq \emptyset \) and the run is accepting, some accepting state \( f \in F' \) appears infinitely often. By finiteness of the state space, there exist indices \( k < m \) such that \( x_k = x_m = f \). Then the run splits into a finite prefix \( x_0 \dots x_k \) and a finite cycle \( x_{k+1} \dots x_m \). Repeating the cycle infinitely often reconstructs an accepting run. The corresponding infinite-horizon plan is implemented by executing the prefix once and the suffix cycle repeatedly, ensuring the Büchi acceptance condition is satisfied.

In this lesson we formalized automata-based planning: temporal logic specifications are compiled into Büchi automata, which are then synchronized with robot transition systems via product construction. Planning reduces to accepting-run search in the product, typically via graph algorithms that identify prefix-suffix (lasso) structures. We provided implementation sketches in Python, C++, Java, MATLAB/Simulink, and Wolfram Mathematica, forming a bridge between formal methods and practical robotic planning pipelines.