Keywords: Neuro-symbolic planning, planning domain description language (PDDL), signal temporal logic (STL), safety guarantees, constrained control

1 Introduction↩︎

LLM and vision-language models can transform natural instructions, images, and demonstrations into plausible action proposals, but a pure LLM-based plan does not by itself guarantee executability or safety. Conversely, classical PDDL planners give machine-checkable guarantees only after a problem is fully formalised, and they underuse LLMs’ ability to read context and propose repairs. This paper takes a best-of-both-worlds view: a neural model generates and repairs candidate plans, while symbolic validation and data-derived temporal-logic constraints decide which candidates may be executed.

Figure 1 shows the offline mining pipeline (top row) and the online plan-and-check loop (bottom row). In our framework the LLM is not a standalone planner but a proposal mechanism inside a machine-checkable loop. All LLM calls run on a locally-hosted open-weight model (Qwen3-32B in our experiments), supporting on-robot deployment with no cloud dependency. We instantiate this view with three contributions. The first is an offline procedure that mines a single global Signal Temporal Logic (STL) constraint \(\Phi_{\mathrm{mob}}\) from demonstration data (Sec. 4.1). Because every recorded trace is by construction acceptable behaviour, the data is one-class. We synthesise the missing negative class with counterfactual perturbations and an LLM violation generator, turning constraint mining into a supervised classification problem. The constraint is global: it is not attached to a particular action schema but encodes how the robot must move at all times (bounds on speed, clearance, social spacing), so it applies uniformly to every mobility action any plan invokes. The same procedure recovers codified rules (mined from nuPlan [1] driving logs) or population preferences (mined from SCAND [2] teleoperation), depending on what the data encodes.

The second is an evolutionary PDDL planner (Sec. 4.2). Rather than calling a classical search procedure, an LLM proposes and repairs plans against a fixed PDDL problem \(P\) and domain \(D\), and a programmatic validator cascade scores each candidate. Elitism on validator feedback grows the validated prefix of the plan monotonically over iterations, without any explicit suffix-only mutation. The result is a system that uses LLM generation only inside a formally evaluated loop.

The third is the constrained execution loop (Sec. 4.3). The planner emits a plan \(\pi=(a_1,\ldots,a_n)\) from a PDDL problem encoding the natural-language task; each action \(a_k\) is dispatched to a navigation layer that produces a waypoint sequence \(w_k\), which is checked against \(\Phi_{\mathrm{mob}}\). A violation rejects \(a_k\), commits the verified prefix, updates the initial state, and re-invokes the planner. For the Gazebo demonstration we instantiate the navigation layer with a trajectory planner that produces a waypoint sequence; the sequence is checked against \(\Phi_{\mathrm{mob}}\) before each action is executed.

We evaluate the planner on open-world ALFWorld Text, where it outperforms strong baselines and stays robust under goal/action-vocabulary misalignment (Sec. 5.2). We evaluate the mined constraint as a shield over a Qwen2.5-VL driver on Bench2Drive and two discrete-action navigation policies on HA-VLN-CE (Sec. 5.1). We illustrate the constrained execution loop in Gazebo (Sec. 5.3); additional demonstrations are in the appendix.

2 Related Work↩︎

2.0.0.1 LLM/VLM planning with formal representations.

Recent work combines foundation models with formal planners to overcome the brittleness of one-shot natural-language planning. VLMFP generates PDDL domain and problem files from visual observations using a dual-VLM loop, then checks symbolic execution against simulated outcomes [3]. NL-PDDL replaces rigid symbolic predicates with natural-language counterparts and uses lifted regression with commonsense entailment to handle open-world goal-action misalignment [4]. PIP-LLM uses PDDL for team-level task decomposition and integer programming for robot-level allocation in multi-robot coordination [5]. These systems show the value of formal intermediate languages, but they generally focus on symbolic plan generation rather than learned signal-level execution contracts.

2.0.0.2 Safety-aware symbolic planning and verification.

Classical PDDL planning separates domain schemas from problem instances [6], and validators such as VAL provide independent checks of plan executability [7]. SafeGen-LLM extends this line by training LLMs for safety-aware PDDL3 planning with verifier-derived rewards [8]. Our approach differs by learning STL contracts from real trajectories and enforcing them during continuous execution, so a symbolic effect is asserted only after the measured trace certifies that the skill actually occurred.

2.0.0.3 Temporal logic learning, evolutionary search, and robot safety.

STL provides a language for temporal properties over real-valued signals [9], and robustness semantics support quantitative monitoring [10]. Recent methods learn temporal-logic predicates from data with statistical guarantees [11], motivating our constraint-identification stage. AlphaEvolve demonstrates that LLM-guided evolutionary search can improve machine-gradable symbolic artifacts through automatic evaluation [12]; we apply this pattern to PDDL plans and STL contracts. Complementary work on grounded heterogeneous teams [13] and robot constitutions [14] highlights the need for closed-loop grounding and semantic safety in real robot systems. Appendix 10 gives an extended comparison.

3 Problem Definition↩︎

We address the problem of executing a natural-language task in a partially known, dynamic world while satisfying implicit norms that are not stated in the task itself, given only unannotated prior robot operation logs as the source of those norms.

3.0.0.1 Inputs.

A deployment instance is the tuple \(\mathcal{I} = (\mathcal{W},\, \mathcal{A},\, g_{\mathrm{lang}},\, \mathcal{N},\, \mathcal{D})\). The partially known world model \(\mathcal{W} = (\mathcal{S}, \widehat{T})\) has a state space \(\mathcal{S}\) observed only locally through a perception stack and an incomplete transition model \(\widehat{T}\): regions are unmapped, semantic labels are noisy, and other-agent dynamics are not given in closed form. A set of dynamic agents \(\mathcal{A}\) (pedestrians, vehicles, or other moving entities) is observed online but not provided in advance. The explicit language task \(g_{\mathrm{lang}}\) is expressed in natural language (e.g., “drive to the cafeteria”). The implicit norms \(\mathcal{N}\), which the robot must additionally satisfy, are codified rules (e.g., stop at red lights) or population preferences (e.g., maintain social distance), depending on the domain; crucially, \(\mathcal{N}\) is not given in symbolic form, only implicitly in the data. The corpus \(\mathcal{D} = \{\tau_1, \ldots, \tau_n\}\) of unannotated prior operation logs contains time series of signals over robot, environment, and other-agent state; by construction every trace is acceptable behaviour, but no \(\mathcal{N}\) annotation is attached to any signal.

3.0.0.2 Output.

A constrained execution trace that achieves \(g_{\mathrm{lang}}\): a PDDL plan \(\pi=(a_1,\ldots,a_n)\) produced by a discrete planner from a domain \(D\) and a problem \(P\) that encodes \(g_{\mathrm{lang}}\), such that (i) \(\pi\) is symbolically valid (preconditions, effects, goal reachability), (ii) each action \(a_k\) is mapped by a navigation layer to a waypoint sequence \(w_k\), and (iii) the concatenated trace \(w_1\cdots w_n\) satisfies the implicit norms \(\mathcal{N}\). When \(w_k\) violates \(\mathcal{N}\) at runtime, the verified prefix \(a_1\ldots a_{k-1}\) is committed, the resulting world state becomes the new initial state, and the planner is re-invoked to produce a fresh suffix-replacing plan.

3.0.0.3 What makes this hard.

Three properties of the setting jointly rule out the standard fixes. (1) Partial observability and dynamics. The world model is incomplete and the moving agents’ trajectories must be tracked online from sensor data, so any planner that relies on a fully-specified environment will fail at deployment. (2) Underspecification of the prompt. The language task \(g_{\mathrm{lang}}\) underspecifies the full normative requirement: a planner that optimises only for \(g_{\mathrm{lang}}\) can satisfy the prompt (“you reached the goal”) while violating \(\mathcal{N}\) (“you ran a red light”, “you brushed past a pedestrian”). (3) One-class data. The only prior signal is the unannotated corpus \(\mathcal{D}\) in which every recorded trajectory is acceptable behaviour; there are no labelled violations, no preference pairs, and no symbolic specification of \(\mathcal{N}\). Conventional fixes (reward shaping with hand-coded penalties, behaviour cloning, or RL from preference pairs) each require either a manually written specification of \(\mathcal{N}\), explicitly annotated violation data, or pairwise preference labels. This problem statement assumes none of these are available.

3.0.0.4 Approach.

Offline, we recover \(\mathcal{N}\) from the unannotated corpus \(\mathcal{D}\) by synthesising counterfactual negatives that turn one-class data into a supervised discrimination problem, then fitting a global mobility constraint \(\Phi_{\mathrm{mob}}\) over signals that separates acceptable demonstrations from violations (Sec. 4.1). \(\Phi_{\mathrm{mob}}\) is a single STL formula that applies uniformly to every mobility action; the same procedure produces rule-like \(\Phi_{\mathrm{mob}}\) when \(\mathcal{D}\) encodes a rule-governed domain and preference-like \(\Phi_{\mathrm{mob}}\) when \(\mathcal{D}\) encodes a population’s implicit envelope (Sec. 5.1). Online, the language task \(g_{\mathrm{lang}}\) is translated into a PDDL problem, and an LLM-driven evolutionary PDDL planner (Sec. 4.2) generates a syntactically and symbolically valid plan \(\pi\) against the action domain. Each action \(a_k\) in \(\pi\) is dispatched to the navigation layer, which produces the waypoint sequence \(w_k\); \(w_k\) is checked against \(\Phi_{\mathrm{mob}}\) before execution. If \(w_k\) satisfies \(\Phi_{\mathrm{mob}}\), \(a_k\) is scheduled for execution; otherwise, the verified prefix \(a_1\ldots a_{k-1}\) is committed, the initial state is updated from the resulting world, and the planner is re-invoked with the same goal under the updated state, yielding a new plan whose remaining actions are themselves re-checked under \(\Phi_{\mathrm{mob}}\).

4 EvoPlan Framework↩︎

Figure 1 provides a roadmap. The three subsections below cover, in order: the offline row that produces \(\Phi_{\mathrm{mob}}\) (Sec. 4.1); the evolutionary PDDL solver and PDDL validation blocks (Sec. 4.2); and the trajectory planner, global STL check, and monitor+replan blocks (Sec. 4.3).

4.1 Evolutionary STL constraint mining↩︎

4.1.0.1 One procedure, two kinds of constraint.

We learn a single global mobility constraint \(\Phi_{\mathrm{mob}}\) from demonstrations: a Signal Temporal Logic (STL) formula over named sensor signals (speed, clearances, time-to-collision, etc.) that every move in any plan must satisfy. The same procedure recovers two kinds of constraint depending on the source data. For codified rules (e.g., driving norms), the formula uses exact thresholds and “if A then B” clauses that encode each rule directly. For population preferences (e.g., social navigation), it learns tight bounds that match what operators consistently do. The grammar, the search, and the shield are identical; only the source data and the counterfactual generator change. Sec. 5.1 demonstrates both: rules mined from nuPlan [1] shield a Qwen2.5-VL driving policy on Bench2Drive [15]; preferences mined from SCAND [2] shield two indoor navigation policies on HA-VLN-CE.

4.1.0.2 Counterfactual negatives.

The demonstrations are one-class data: every recorded trace is acceptable, so there are no labelled bad examples to fit against. We create them with counterfactual perturbations. Ten procedural modes (speeding, reckless_turn, crowding_front, density_mismatch, red_light_run, tailgating, …) push one or two signals out of range; an LLMgenerator adds one realistic violation per clip. This gives the positive set \(\mathcal{D}^+\) (demonstrations) and a contrastive set \(\mathcal{D}^-\) (counterfactuals), so constraint mining becomes a classification problem.

4.1.0.3 Evolutionary STL constraint fitting.

We learn the constraint by evolving STL formulas via an LLM-driven search over program edits [12]. The grammar has atoms such as \(d_{obs}\ge c\), \(d_{human}\ge c\), \(v\le c\), \(inside(z)\), \(coverage(z)\ge c\), and \(link\ge c\). Each candidate is scored by its STL robustness on \(\mathcal{D}^+\) and \(\mathcal{D}^-\), minus complexity and triviality penalties: \[\max_{\Phi\in\mathcal{G}}\; \underbrace{\mathbb{E}_{\tau\in\mathcal{D}^+}\rho(\tau,\Phi)}_{\text{expert satisfaction}} -\lambda_-\underbrace{\mathbb{E}_{\tau\in\mathcal{D}^-}\max(0,\rho(\tau,\Phi))}_{\text{reject unsafe traces}} -\lambda_c\,\mathrm{complexity}(\Phi).\] Closely related work learns STL predicates from data with conformal prediction [11]; here, the learned formula becomes a global constraint applied to every move in every plan.

4.1.0.4 Downstream enforcement.

Because \(\Phi_{\mathrm{mob}}\) is defined over sensor signals rather than inside a particular controller, it can be enforced on any task without retraining the policy. We use two modes: a trajectory planner that closes the constrained execution loop (Sec. 4.3), and a black-box shield that vetoes an arbitrary discrete-action policy via predicted min-robustness and MPC substitution under a policy-prior weight \(\alpha\) (Sec. 5.1; details in Appendix 7.6.0.4).

4.2 Evolutionary PDDL plan synthesis↩︎

We cast PDDL plan search as machine-gradable evolution [12]: an LLM proposes plan edits, a programmatic cascade decides which survive, and the cascade’s descriptive feedback (the failing action and its unsatisfied precondition) conditions the next LLM mutation, so the loop evolves plans in response to verifier signals rather than free-form sampling. The same loop handles closed-world tasks and open-world tasks with partial belief states.

4.2.0.1 Evolutionary search loop.

A candidate is a grounded action sequence \(\pi\) evolved against a fixed PDDL problem \(P\) and domain \(D\). Each generation, the LLM proposes an edit to the current best candidate conditioned on the parent’s validator feedback; typical edits include inserting a missing precondition action, repairing an object binding, swapping independent actions, or resampling a suffix, but the edit type is not constrained ex ante. A four-stage cascade scores the child: PDDL syntax, VAL [7] simulation, goal reachability, and (when continuous execution is involved) predicted robustness against the global constraint \(\Phi_{\mathrm{mob}}\) from Sec. 4.1. Stages short-circuit. Invalid plans are demoted by the cascade, not by an LLM critic.

4.2.0.2 Verified-prefix preservation.

Although no prefix is explicitly frozen, the validated fraction \(|\pi_{\mathrm{valid}}|/|\pi|\) grows monotonically over iterations on hard tasks in both open- and closed-world runs (Fig. 2). Token usage stays proportional to the unverified work because VAL feedback marks only the failing action.

4.2.0.3 Open-world and misaligned deployments.

In open-world deployments the problem \(P\) is built from a belief \(B\); an “object-not-declared” validator failure triggers exploration, \(B\) grows monotonically, \(P\) is rebuilt, and the search resumes (budget tracked in simulator steps, matching ALFWorld’s 50-step protocol). When the goal vocabulary \(\not\subseteq\) action vocabulary (e.g., goal “heated” vs.action toast), a single LLM call produces a predicate-symbol map \(\mu\) applied to the goal predicates of \(P\) just before VAL. It composes cleanly with open-world belief growth: as new objects are observed and inserted into \(P\), the same \(\mu\) rewrites their goal predicates uniformly, with no per-object re-entailment.

Pseudocode for the outer task loop and the inner evolutionary subroutine is given in Appendix 8.1.

4.3 Constrained execution loop↩︎

The two evolved artifacts plug together at runtime through a single bridge. The evolutionary PDDL planner (Sec. 4.2) emits a plan \(\pi=(a_1,\ldots,a_n)\); each action \(a_k\) is then expanded by a navigation layer into a waypoint sequence \(w_k\), which is checked against the mined STL constraint \(\Phi_{\mathrm{mob}}\) (Sec. 4.1) before execution. If \(w_k\) satisfies \(\Phi_{\mathrm{mob}}\) it is dispatched to the robot; if not, the verified prefix \(a_1\ldots a_{k-1}\) is committed, the state is refreshed from the resulting world, and the planner is re-invoked from the updated initial state.

The bridge is implemented as a ROS 2 adapter that uses a differential-drive robot model (a simulated Jackal in our Gazebo demonstration), local distance fields, human tracking, and terrain labels; the navigation layer is realised by a trajectory planner whose global and local stages produce a waypoint sequence. The grounded \(\Phi_{\mathrm{mob}}\) predicates are evaluated on this waypoint sequence before execution; a violation rejects the action, commits the verified prefix, and triggers a replan with an updated initial state. An online monitor recomputes robustness from the measured trace and emits failure facts (e.g., route-blocked, no-safe-approach) that the next replan can consume. Implementation details and additional demonstrations are in Appendix 9.

5 Experiments↩︎

5.1 Mined STL constraints transfer to downstream policies↩︎

We evaluate the STL constraint mining of Sec. 4.1 on two cases: rules mined from driving demonstrations and preferences mined from social-navigation teleoperation. The extraction procedure and shield are identical across both; only the source corpus, base policy, target benchmark, and policy-prior weight \(\alpha\) change.

5.1.1 Rule showcase: nuPlan \(\to\) Bench2Drive↩︎

Driving signals (kinematics, clearance, time-to-collision, lane context, traffic-light state) replace the SCAND social ones; the recovered formula encodes codified norms (stop-on-red, clearance and time-to-collision floors, lane-aware speed caps). Unlike the social-navigation preferences of Sec. 5.1.2, each clause has binary right/wrong semantics, and the contrastive negatives that falsify them are unambiguous rule violations rather than envelope-tightness perturbations. The constraint shields a Qwen2.5-VL [16] driving stack on Bench2Drive [15]: the shield operates on a four-keyword discrete decision, which a P-controller expands into continuous (throttle, steer, brake) actions (interface and shield mechanics: Appendix 7.5).

The strict shield (\(\alpha{=}0\)) cuts red-light infractions by \(77\%\) and collisions by \(71\%\) while improving the Driving Score; \(\alpha{=}0.30\) reaches the best Driving Score in the sweep (Table [tbl:tab:downstream95b2d]). The nuPlan-mined constraint suppresses Bench2Drive’s two heaviest penalty categories zero-shot, with no benchmark-specific training.

5.1.2 Preference showcase: SCAND \(\to\) HA-VLN-CE↩︎

Applied to SCAND outdoor sidewalk teleoperation [2], the same procedure recovers implicit social-navigation preferences. The constraint shields two discrete-action policies on HA-VLN-CE [17]: a pretrained PointNav (DD-PPO [18]) and an MLP trained by behaviour cloning. Unlike the driving showcase, where a P-controller bridges the discrete shield to a continuous actuation space, the policies’ effective action space here is itself discrete, so the shield’s veto-and-substitute step composes directly with the policy’s output. The full \(17\)-predicate formula, metric definitions, and per-cause collision decomposition are in Appendix 7.6.

With only \(\alpha\) tuned per policy, the shield removes \(82\%\) of avoidable contacts on PointNav and \(93\%\) on the MLP (Table [tbl:tab:downstream95headline]); Fig. 3 shows the unsafe tails of the per-episode safety distributions collapse rather than the means merely shifting. Together with the rule showcase, the same mining recipe and shield handle both rules and preferences with no method-level changes beyond source data and \(\alpha\).

5.2 Evolutionary PDDL planner↩︎

We evaluate on the NL-PDDL benchmark [4]: AlfredTWEnv TextWorld on \(N{=}134\) unseen validation tasks with a \(50\)-step budget. The simulator provides a ground-truth perception and affordance oracle, isolating the planner from recognition errors; the agent must explore to reveal task-relevant objects before interacting with them. Table 1 reports the result; EvoPlanalso solves tasks whose optimal plans exceed depth \(10\), where NL-PDDL’s fixed-horizon planner “fails beyond depth \(10\)” [4]. In the closed-world setting, EvoPlan(Qwen3-32B) reaches \(99.7\%\) on Blocksworld Plain, \(74.0\%\) on Mystery, \(78.7\%\) on Randomized, and \(100\%\) on Misalignment (FD: \(0\%\)); on the alfred ALFWorld domain (\(N{=}134\) valid_unseen), \(90.3\%\). These gains come at a higher LLM token cost than the fully-symbolic NL-PDDL (\(25\)–\(150\times\) on Blocksworld); the trade-off and the cost analysis are in App. 8.2. Additional local-model comparisons and ablations are in Appendix 8.

4pt

5.3 Constrained execution loop end-to-end↩︎

We illustrate the constrained execution loop in a Gazebo factory scene where a Jackal completes pick-and-drop missions (Fig. 4). Plans from the evolutionary PDDL planner (Sec. 4.2) are produced action-by-action: each PDDL move is grounded into a route by Nav2 and checked against \(\Phi_{\mathrm{mob}}\) before execution; a clearance-floor violation rejects the action, commits the verified prefix, and triggers a replan.

5.3.0.1 Quantitative shield results.

We run \(5\) pick-and-drop missions (\(1\) run each) at \(9\)–\(15\) pedestrians per scene with the SCAND-mined \(\Phi_{\mathrm{mob}}\) active. The shield completes every planned route and keeps four of five runs collision-free; the lone failure (M4) records a collision when the densest cluster leaves no admissible replan within the budget, and clearance falls to \(0.05\) m. Personal-zone (\({<}1.2\) m) exposure stays under \(13\%\) of ticks across all five runs while social-zone exposure climbs to \(40\)–\(68\%\), showing that the loop spends most of each run within \(3.6\) m of a pedestrian yet rarely within personal distance. M3 maintains both low exposure (\(0\%\) personal, \(P_{\mathrm{int}}{=}12.7\)) and the second-highest minimum clearance (\(0.90\) m) by routing around the densest cluster, while M2 takes the longest path (\(90.3\) m) through a sustained dense aisle and accumulates \(P_{\mathrm{int}}{=}115.2\) at clearance \(0.40\) m. The loop therefore degrades gracefully under crowded operation: it trades clearance margin for an isolated failure rather than collapsing wholesale (Table 2).

3pt

6 Conclusion and Limitations↩︎

We presented a hybrid PDDL–STL framework for learning and deploying safe robot plans. One-class demonstrations are converted into a single global STL constraint \(\Phi_{\mathrm{mob}}\) via counterfactual perturbations and an LLM violation generator; an evolutionary LLM-guided planner proposes and repairs PDDL plans against a programmatic validator cascade; and a constrained execution loop grounds each action into a waypoint sequence and accepts it only if \(\Phi_{\mathrm{mob}}\) holds. The resulting system treats neural models as generators of candidates rather than sources of unchecked authority. Limitations include dependence on demonstration quality, the expressivity and tractability of the STL grammar, perception uncertainty, sensitivity to the proposal backbone, and the need for broader hardware validation. Future work will extend the framework to richer multi-robot tasks, stronger statistical guarantees for learned constraints, and per-skill constraint families beyond global mobility.

7 Constraint mining: method and validation↩︎

7.1 Trajectory inputs and preprocessing↩︎

Each trajectory is converted into a time-indexed record \[\tau=(x_{0:T},u_{0:T-1},z_{0:T},m_{0:T}),\] where \(x_t\) is robot state, \(u_t\) is control, \(z_t\) is perceptual context, and \(m_t\) contains derived metric signals such as obstacle distance, human distance, terrain label, and region membership. For egocentric videos without reliable pose, structure-from-motion and visual odometry provide approximate trajectories. For SCAND-style data, odometry, joystick commands, lidar, camera, and IMU streams are aligned before mining.

7.2 STL grammar↩︎

A compact grammar for the mobility constraint is \[\begin{align} \phi &::= \mu \mid \neg \phi \mid \phi\wedge\phi \mid \phi\vee\phi \mid \Box_{[a,b]}\phi \mid \Diamond_{[a,b]}\phi,\\ \mu &::= d_{obs}\ge c \mid d_{human}\ge c \mid v\le c \mid inside(z) \mid coverage(z)\ge c \mid link\ge c \mid battery\ge c. \end{align}\] In practice the learned \(\Phi_{\mathrm{mob}}\) is dominated by global \(\Box\) (always) bounds on threshold atoms; the bounded temporal operators \(\Box_{[a,b]}\) and \(\Diamond_{[a,b]}\) are in the grammar but rarely selected by the evolutionary search on this corpus (the full mined formula in App. 7.6.0.3 is \(17\) conjoined \(\Box\)-bounded clauses).

7.3 Evolution operators and acceptance tests↩︎

Formula mutations include threshold perturbation, time-window shift, atom replacement, insertion of \(\Box\) or \(\Diamond\), and Boolean composition. Crossover swaps subtrees between formulas with compatible signal vocabularies. A formula is accepted when it satisfies four tests: positive held-out robustness on expert traces, low satisfaction rate on contrastive unsafe traces, bounded expression complexity, and interpretability by a human reviewer.

7.4 Mining failure cases↩︎

Common failures include over-specific formulas that memorize a particular route, trivial formulas that are always true, and constraints that depend on unavailable runtime signals. These failures are handled by grammar restrictions, complexity penalties, and signal-availability checks.

7.5 Rule showcase: Bench2Drive shield setup and full results↩︎

7.5.0.1 Recovered formula.

The nuPlan extraction recovers a small set of conditional implications, each with binary right/wrong semantics: a stop-on-red-light implication, vehicle-clearance and time-to-collision floors, and lane-aware speed caps. The contrastive negatives that falsify these clauses (a red_light_run; a closing-rate spike inside the lead-vehicle gap) are unambiguous rule violations rather than envelope-tightness perturbations.

7.5.0.2 Keyword interface and continuous expansion.

The Qwen2.5-VL agent is prompted every ten simulator ticks (\(\approx\!1\) Hz) on the forward-camera frame and emits one of four keywords \(\{\mathrm{\small accelerate}, \mathrm{\small coast}, \mathrm{\small brake}, \mathrm{\small emergency\_stop}\}\). A latched target-speed updated by each keyword (e.g., accelerate raises it by \(\Delta v\), brake halves it) and a per-tick P-controller produce continuous (throttle, steer, brake) commands to CARLA on every intervening tick. The policy’s effective control authority is therefore continuous even though the shield’s decision space is the four-option discrete keyword set.

7.5.0.3 Shield loop.

The shield wraps the keyword decision identically to the HA-VLN-CE case of App. 7.6.0.4: predict the short-horizon rollout for each candidate keyword, compute min-robustness \(\rho\) against the mined formula, veto when \(\rho{<}0\) under an imminence gate, and substitute via MPC over the four keywords with the policy-prior weight \(\alpha\).

7.5.0.4 Full Bench2Drive sweep.

Table 3 adds the full policy-prior sweep on Bench2Drive (all seven \(\alpha\) settings) with three additional metrics (route completion, total vetoes, completed routes) on top of the condensed main-text Table [tbl:tab:downstream95b2d].

7.6 Preference showcase: architecture, formula, shield mechanism, \(\alpha\) analysis↩︎

7.6.0.1 Base policies.

PointNav is the pretrained PointNavResNet50\(+\)LSTM policy from DD-PPO [18], evaluated on RGB+depth observations from the HA-VLN-CE simulator. The MLP is a stateless two-hidden-layer network (\(256{\times}256\), ReLU) trained by behaviour cloning on the PointNav policy’s own decisions across the train split, so it represents a memoryless approximation of the same input–output mapping. Both policies emit one of four discrete actions \(\{\mathrm{\small stop}, \mathrm{\small fwd}, \mathrm{\small left}, \mathrm{\small right}\}\) per tick directly to the simulator.

7.6.0.2 Episode protocol and metrics.

Each condition is evaluated on the full HA-VLN-CE val_unseen split, \(N{=}1839\) episodes, paired by episode ID so the unshielded and shielded conditions experience the same humans, layouts, and goal poses. An episode is a collision-termination (CT) when the simulator’s collision counter increments while min_clearance\({<}1.0\) m. A success is reached-goal-and-never-human-collision. We additionally classify each collision-terminated episode by its final-tick safety log into avoidable contacts (the agent walked into a stationary or slowly-moving human) and trajectory-crossings (a side-cone human only became visible inside the \(K\)-step shield rollout); the per-cause decomposition appears in App. 7.7.

7.6.0.3 Full mined STL formula.

The OpenEvolve [19] mining loop converges to the conjunction of \(17\) globally-quantified predicates below. Thresholds match the tightest demonstrator extrema and are recovered by the evolutionary search rather than hand-set.

G(speed              <= 2.603) &
G(yaw_rate           <= 3.293) &
G(accel              <= 3.213) &
G(jerk               <= 5.862) &
G(lat_accel          <= 2.228) &
G(cmd_steer          <= 1.000) &
G(min_clearance      >= 0.483) &
G(crowd_count >= 3 | min_clearance >= 0.6) &
G(front_clearance    >= 0.505) &
G(left_clearance     >= 0.500) &
G(right_clearance    >= 0.500) &
G(rear_clearance     >= 0.483) &
G(ttc                >= 0.452) &
G(ped_approach_rate  <= 5.000) &
G(ped_clearance      >= 0.500) &
G(front_ped_clearance>= 0.500) &
G(ped_ttc            >= 0.422)

Three clause families are present. The kinematic comfort envelope (six clauses) bounds speed, yaw_rate, accel, jerk, lat_accel, and operator cmd_steer. The social keep-distance floors (seven clauses) bound every directional clearance bin and the time-to-collision, and add the crowd-conditioned disjunction G(crowd_count\({\ge}\)​3| min_clearance\({\ge}\)​0.6) that catches the density_mismatch counterfactual negatives the flat min_clearance floor misses. The pedestrian-specific clauses (four clauses) mirror the same structure on ped_clearance signals available when perception has separated pedestrians from generic returns; the \(0.5\) m floor on front_ped_clearance is the binding clause at downstream shield time.

7.6.0.4 Shield mechanism.

At each control tick the shield performs the following steps.

1. Extract a current signal dictionary from the live simulator (the same clearance bins SCAND uses, computed without perception because HA-VLN exposes ground-truth human positions).

2. Call the base agent’s act(obs) to get a proposed action \(a_t\).

3. Hypothesise the next-tick signals under \(a_t\), append them to a \(10\)-tick rolling window, and evaluate the formula’s min-robustness \(\rho\).

4. If \(\rho<0\) and the predicted next-tick front_ped_clearance is below an imminence threshold, the action is vetoed; the imminence threshold is calibrated per base agent (\(0.7\) m for the privileged Oracle, \(1.0\) m for the noisy SPF and PointNav, none for Random).

5. On veto, a \(K{=}5\)-step model-predictive substitution enumerates the four discrete actions, rolls each forward under constant-velocity human motion and analytic agent kinematics, scores by predicted \(\rho\), and commits the argmax first action. An optional beam variant (width \(B{=}4\)) plans over action sequences of length mpc_horizon; it finds recovery patterns such as “stop, turn, forward” that the single-step substitution misses.

7.6.0.5 Predictive imminence.

An early version of the shield gated only on the next-tick front_ped_clearance. Side humans about to cross the agent’s path \(2\)–\(5\) ticks ahead kept this signal high at tick \(1\), so the shield silently let the agent walk into the crossing; this trajectory-crossing failure mode dominated \(65\%\) of the residual collisions. The current shield gates on the minimum clearance over the full \(K\)-step rollout, taken across min_clearance (any direction), front_ped_clearance, and front_obstacle_clearance. The any-direction component is the critical addition: side humans that do not show up in the front cone do show up in min_clearance.

7.6.0.6 Policy-prior weight \(\alpha\).

A soft policy prior augments the candidate score by the log-probability the base policy assigned to each action: \[\hat{a} = \operatorname*{arg\,max}_{a}\; \rho(\tau_a) + \alpha\,\log\bigl(\max(\epsilon, \Pr_\pi[a])\bigr),\] with \(\epsilon{=}10^{-2}\) flooring the log to keep the bonus bounded. At \(\alpha{=}0\) the prior is disabled and the picker recovers the original min-robustness argmax. With the floor, the maximum penalty for a zero-probability action is \(\alpha\log(10^{-2})\approx -4.6\alpha\), so for \(\alpha\in\{0.05, 0.1, 0.2\}\) the prior caps at \(\{0.23, 0.46, 0.92\}\) m of \(\rho\)-equivalent: a meaningful tiebreak among comparable-safety candidates that never overrides a \({>}1\) m clearance differential. On PointNav, \(\alpha{=}0.05\) is the only sweep value that does not over-trust the policy (\(\alpha\in\{0.1,0.2\}\) pushes the veto rate to \(6\)–\(7\%\) and degrades both SR and CT); on the stateless MLP, \(\alpha{=}0\) already preserves SR within noise and no prior is needed.

7.6.0.7 Why the prior is necessary: preserving PointNav’s training distribution.

PointNav is a DD-PPO-trained recurrent policy [18]: its LSTM hidden state encodes recent actions through a learned prev_action embedding, and the policy is almost deterministic given an observation. Without the prior, the safety picker substitutes whenever any candidate has higher predicted \(\rho\), even by a margin much smaller than the typical safety differential. Each such substitution drives the LSTM off-distribution at every subsequent tick: the hidden state has “just moved forward” encoded in it while the simulator actually advanced under stop or a turn, so the visual encoder sees paths DD-PPO never traversed during training. The prior fixes this by requiring a substitution’s safety advantage to exceed the policy’s own confidence in its proposal. The bounded \(-4.6\alpha\) floor keeps this soft: a substantial \(\rho\) gap (\({>}1\) m clearance for \(\alpha{=}0.05\)) still overrides the prior, so the prior only suppresses small-margin substitutions that would have desynced the policy without buying real safety. The stateless MLP needs no prior because it has no recurrent state to corrupt — which is why \(\alpha{=}0\) preserves SR on MLP (Table [tbl:tab:downstream95headline]) but costs \(4.3\) pp on PointNav, and \(\alpha{=}0.05\) is the smallest nonzero setting that closes that gap.

7.6.0.8 Full HA-VLN-CE results with confidence intervals.

Table 4 adds the McNemar paired \(95\%\) confidence intervals on \(\Delta\)SR and \(\Delta\)CT for HA-VLN-CE.

7.7 Per-cause collision decomposition↩︎

We classify each collision-terminated episode using the \(5\)-tick safety log captured immediately before termination. An avoidable contact is one where, in the final tick, the agent was moving forward (speed\({>}0.1\)) and the colliding human was in the front cone (front_clearance\({<}1.5\) m), so a stop would have prevented the contact. A trajectory-crossing contact is one where the agent was moving but the colliding human was not in the front cone; the human’s path crossed the agent’s from the side or rear, leaving only the predictive-rollout horizon to react. A third bucket, human-into-static-agent, is always empty in our data because HA-VLN’s previous_step_collided flag only fires when the agent attempts a move that is physically blocked.

Two takeaways from Table 5. First, the shield is near-perfect on its core jurisdiction: avoidable contacts drop by \({\ge}82\%\) on both policies, the cleanest demonstration that the mined constraint does what its name promises. The \(82\%\)/\(93\%\) gap reflects the stateless MLP having more avoidable contacts to begin with, not the shield being more effective on MLP per se. Second, the shield also helps on trajectory-crossings (\(-35\%\) on PointNav, \(-76\%\) on MLP) because the \(K\)-step predictive rollout extrapolates side humans’ positions forward and vetoes a forward that would put the agent in a future contact, even when the human is not yet in the front cone at decision time.

8 Evolutionary PDDL planner: algorithm and results↩︎

8.1 EvoPlan algorithm↩︎

EvoPlan combines an outer task loop driven by belief growth in the simulator with an inner evolutionary loop that proposes and repairs PDDL plans. The outer loop alternates between exploring to expand the belief and calling the inner loop on the resulting PDDL problem. The inner loop mutates an LLM-proposed plan against feedback from a symbolic validator cascade. When the goal vocabulary disagrees with the action-model vocabulary (misalignment), a one-time LLM call derives a predicate-symbol map \(\mu\) that is cached and reused. The algorithm consumes a fixed PDDL domain \(D\) provided as input.

The notation used in Algorithm 5 is summarised first. Symbols are the variables that flow through the procedures; routines are the named subprocedures (their bodies are described informally rather than expanded). For clarity, Algorithm 5 serves as the formal description of EvoPlan, and the accompanying Tables of Symbols and Routines provide a convenient reference for notation and procedures.

8.1.0.1 Symbols (state and inputs).

8.1.0.2 Routines (subprocedure semantics).

8.1.0.3 Worked example.

Algorithm 5 run on Blocksworld Mystery instance p0009 (action names renamed to deceptive English; goal: stack yellow-on-pink-on-orange) converges in four iterations. Each row of the box pairs the candidate plan with the validator feedback that drives the next mutation.

The pattern – precondition fail, goal-miss over-correction, partial repair with spurious tail, then a clean trim to the optimum – is typical: the validator artifact converts “which clause failed” into the next prompt’s repair target.

8.2 Closed-world Blocksworld results↩︎

This section evaluates EvoPlan on the closed-world benchmarks of the NL-PDDL suite [4], where the planning component is isolated from perception and exploration. The only LLM call in the loop is plan proposal/repair; validity is decided by VAL and Fast Downward [7], [20].

8.2.0.1 Benchmark variants.

Following [4], we use the standard Blocksworld domain [6] (Plain) and three surface-form variants that defeat lexical priors: Mystery (predicates and actions renamed to misleading English words), Randomized (renamed to gibberish), and Misalignment (action model in renamed terms, goal in plain vocabulary). On Misalignment we insert a one-time LLM entailment step that maps the goal predicates onto the misaligned domain; the evolutionary loop runs unchanged thereafter.

8.2.0.2 Headline result.

Table 6 reports SR per variant. Direct LLM planners collapse on the renamed variants (\(0\%\) on Mystery/Randomized). EvoPlan recovers near-symbolic performance: both backbones match FD on Plain; gpt-oss-120b matches FD on Randomized; and both backbones exceed NL-PDDL on every variant. On Misalignment (FD \(= 0\%\)), EvoPlan reaches \(98\)–\(100\%\) through the entailment pre-step.

8.2.0.3 Mystery as the difficulty floor.

Mystery is the hardest variant for Qwen3-32B and exposes a backbone-specific limit: the deceptive vocabulary inflates the model’s reasoning trace, and clearing NL-PDDL’s \(70\%\) requires raising the per-call reasoning budget. On gpt-oss-120b the same variant is reached at a lower budget, indicating that the bottleneck is per-call reasoning depth rather than the number of iterations. Across all variants, most tasks converge within \(1\)–\(3\) iterations and per-call prompts carry no few-shot exemplars.

8.2.0.4 Reporting conventions.

The benchmark is the NL-PDDL Blocksworld suite [4]: Plain plus the three surface-form variants Mystery, Randomized, and Misalignment. Tokens-to-solve are computed as the cumulative LLM tokens up to the iteration that first emits a VAL-valid plan; unsolved tasks count their full iteration budget. Direct-LLM, NL-PDDL, and Fast Downward [20] numbers are reproduced from [4]. NL-PDDL’s token cells are dashed on Plain/Mystery/Randomized because its FOL regression planner is fully symbolic and invokes the LLM only for one-time commonsense entailment when the goal and action-model vocabularies disagree; on Misalignment that entailment call is reflected in its token cell. EvoPlananalogously inserts a one-time LLM entailment pre-step before the evolutionary loop on Misalignment.

3pt

8.2.0.5 Token cost.

EvoPlan’s tokens-to-solve are higher than NL-PDDL’s on the shared-vocabulary variants. This is structural rather than incidental: NL-PDDL is a fully symbolic FOL regression planner that calls the LLM only for one-time vocabulary entailment when the goal and domain disagree, while EvoPlan uses the LLM as its plan proposer at every iteration with the validator providing repair feedback. The per-iteration LLM cost is the price of a few capabilities that the symbolic planner does not offer: the proposer tolerates renamed action-model vocabularies without per-variant entailment engineering, solves tasks whose optimal plans exceed the regression planner’s fixed depth, runs against any input PDDL domain \(D\) without action-schema mining, and is backbone-agnostic, so quality follows the public LLM ecosystem. On problems where symbolic regression succeeds outright, EvoPlan is the more expensive choice; on problems where it does not (deep plans, surface-form renaming, vocabulary misalignment without manual entailment layers), the same budget yields a working plan within an unchanged loop. The cost therefore grows with task difficulty rather than with method complexity.

8.3 Closed-world ALFWorld results↩︎

Beyond the synthetic Blocksworld variants, we evaluate on the realistic closed-world ALFWorld domain with the canonical alfred PDDL action model and the \(N{=}134\) valid_unseen tasks of [4]. Each instance encodes the full ground-truth scene as the initial state, with existentially-typed goals; this isolates the symbolic planner from perception and exploration, which are tested separately under the open-world setting (Sec. 5.2). Table 7 reports aggregate SR. The closed-world figure (\(90.3\%\) for Qwen3-32B) and the open-world figure (\(98.5\%\), Sec. 5.2) measure different protocols and are not directly comparable: the former isolates symbolic search, the latter measures the integrated explore–plan–act loop.

6pt

8.4 Same-backbone planner ablation↩︎

We isolate the evolutionary loop’s contribution by holding the backbone (Qwen3-32B), the prompt template, and the per-task budget fixed across two arms that differ only in the search loop: single-shot LLM+VAL (\(k{=}1\)) versus the full feedback-conditioned evolutionary loop. Closed-world Blocksworld Plain is the discriminating benchmark because Qwen3-32B’s single-shot SR there (\(86.7\%\)) is well below the full-EvoPlan figure (\(99.7\%\)), so any lift is attributable to the loop alone.

Single-shot Qwen3-32B already beats every direct-LLM baseline and the NL-PDDL symbolic floor on Plain, confirming the backbone is strong. Adding the evolutionary loop with descriptive feedback lifts SR by \(13\) pp at roughly \(1.5\times\) the token budget. The lift comes from the harder instances where the first proposal fails type-checking or omits a precondition: the validator artifact names the failed action, and the next iteration produces a targeted repair rather than another untargeted guess. Most tasks converge within \(1\)–\(3\) iterations (App. 8.2).

9 Constrained execution loop: runtime and integration↩︎

9.1 Evolutionary planning loop pseudocode↩︎

The runtime planner maintains a database of candidate plans and their evaluator feedback. The contract referenced inside the loop is the global \(\Phi_{\mathrm{mob}}\) mined in App. 7; the loop does not introduce per-skill contracts.

def evolve_plan(task, world, D, Phi_mob):
    population = seed_candidates(task, world, D)
    verified_prefix = []
    while budget_remaining():
        parent = sample(population)
        child = llm_mutate(parent, feedback=parent.feedback)
        if not pddl_syntax_ok(child):
            population.add(child, score=-inf, feedback="format error")
            continue
        val_report = validate_pddl(child, world)
        if not val_report.success:
            population.add(child, score=val_report.score, feedback=val_report.message)
            continue
        stl_report = check_phi_mob(child, world, Phi_mob)
        score = aggregate(val_report, stl_report)
        population.add(child, score=score, feedback=all_reports)
        if child.is_goal_reaching and stl_report.feasible:
            return child
    return best_safe_prefix(population)

9.2 Runtime execution pseudocode↩︎

Once a candidate plan is selected, each PDDL action is dispatched action-by-action: Nav2 grounds the action into a waypoint sequence, the sequence is checked against \(\Phi_{\mathrm{mob}}\), and execution proceeds only if the check succeeds. Symbolic effects come from the fixed PDDL domain \(D\) supplied as input; no per-skill effect certification is performed.

def execute_action(a, world, Phi_mob):
    if not symbolic_preconditions_hold(a, world):
        return emit_failure("precondition-failed")
    waypoints = nav2_plan_route(a.target, world, costmap=world.costmap)
    rho = stl_robustness(waypoints, Phi_mob)
    if rho < 0:
        return emit_failure(failure_fact_from(rho, waypoints))
    dispatch(waypoints)
    return assert_effects(a.effects)  # from PDDL domain D

9.3 Failure facts↩︎

Failure facts are the interface between the continuous executor and the symbolic planner. The two emitted by the runs in this paper are route-blocked(route2) (Nav2 returns no admissible global path or the planned route violates \(\Phi_{\mathrm{mob}}\) along its full length) and no-safe-approach(robot1,human1) (the only admissible routes pass within the learned clearance floor of an observed pedestrian). The interface is extensible to additional facts (e.g.low-battery, terrain-risk-high, human-location-uncertain); these are not used by the current experiments. Emitted facts are added to the next PDDL problem instance so the planner can choose alternate actions rather than repeatedly attempting the failed one.

9.4 Nav2 navigation interface↩︎

The runtime bridge converts the evolved STL-constrained plan into actual robot motion through Nav2. Each PDDL move action is dispatched as a navigation goal to Nav2’s behaviour-tree navigator; the global planner produces a route over the static costmap and the local planner refines it into a waypoint sequence over a short horizon. The grounded \(\Phi_{\mathrm{mob}}\) atoms are evaluated on this sequence before the controller executes it: hard safety clauses (clearance, speed, time-to-collision) gate execution, deadline clauses bound the route length, and soft preferences are aggregated into a robustness margin that is reported back to the evolutionary planner.

9.5 Crowd-density ablation in Gazebo↩︎

Sec. 5.3 reports the constrained execution loop at a single nominal crowd setting. To show how the loop responds as crowd size grows, we sweep the number of walking pedestrians in the factory scene from \(0\) to \(50\) (\(\rho \in [0,\,0.041]\,\text{m}^{-2}\)) while holding the five missions, the mined \(\Phi_{\mathrm{mob}}\), and the Nav2 stack fixed. Each setting is averaged over multiple seeded runs. Figure 6 reports four metrics that summarise how the human-aware behaviour of the loop changes with crowd density.

At low density (\(10\) pedestrians, \(\rho \approx 0.008\)) the loop preserves a \(\sim 1\) m minimum clearance and produces no collisions, with personal-zone exposure under \(1\%\) of ticks. As density rises beyond \(\rho \approx 0.016\), the closest approach drops sharply into the intimate band: the local planner has no admissible corridor that respects the \(1.2\) m personal floor, so the robot trades clearance margin to keep making progress. The intimate-zone occupancy in panel (a) nonetheless remains under \(2\%\) of ticks even at the densest setting, because the loop only briefly touches the intimate threshold when slipping past a pedestrian. Cumulative personal-space intrusion (\(P_{\mathrm{int}}\)) grows monotonically with density, reflecting the steady accumulation of small shortfalls below \(1.2\) m rather than a few catastrophic intrusions. Collisions in panel (d) appear once density exceeds \(\rho \approx 0.016\) and rise non-monotonically with population: at \(50\) pedestrians the loop averages \(\sim 2.5\) collisions per run, which is the operating regime where Nav2’s reactive local planner cannot resolve the dense cluster within the shield’s robustness budget.

9.5.0.1 What the sweep shows.

The loop degrades gracefully rather than collapsing: success-relevant metrics (clearance, intimate occupancy, collisions) move smoothly with density and do not exhibit a step-change failure. Personal-space discipline is preserved at the population densities a single mobile robot is realistically expected to encounter (\(\rho \le 0.02\), roughly one person per \(50\,\text{m}^2\)). Beyond that, the constraint is increasingly violated in a controlled way: \(P_{\mathrm{int}}\) grows but the intimate-zone-occupancy ceiling holds. The non-monotonic collision count in panel (d) reflects sensitivity to the specific pedestrian routes drawn at each density rather than method-level non-determinism.

10 Extended related work↩︎

10.0.0.1 LLM and VLM planning.

Early embodied LLM systems showed that language models can sequence high-level robot actions, but purely generative plans are difficult to verify. LLM+P and related approaches use formal planners as back ends, while VLMFP extends this idea to visual inputs by generating PDDL problem and domain files and iteratively aligning symbolic execution with simulated visual outcomes [3]. Our work shares the view that foundation models are most reliable when paired with external evaluators, but it shifts the evaluation target from only symbolic PDDL files to a hybrid PDDL plan plus a global STL constraint \(\Phi_{\mathrm{mob}}\).

10.0.0.2 Open-world symbolic planning.

NL-PDDL addresses incomplete knowledge and goal-action language mismatch by representing predicates in natural language and performing regression planning with LLM-based entailment [4]. This is complementary to our system. NL-PDDL expands the expressivity and accessibility of symbolic planning; our approach focuses on mining a global mobility constraint from trajectories and monitoring it on a robot.

10.0.0.3 Safety-aware PDDL and verifier feedback.

SafeGen-LLM constructs PDDL3 benchmarks with explicit safety constraints and trains LLMs using rewards derived from formal verification [8]. The reward categories in that work, such as format error, precondition violation, safety violation, goal not satisfied, and success, inspire our evaluator cascade. Our setting differs in that safety constraints are not only PDDL3 plan constraints; they are STL formulas over measured robot/environment traces.

10.0.0.4 Multi-robot and grounded collaboration.

PIP-LLM combines PDDL team-level plans with integer-programming robot assignment [5]. SPINE-HT grounds LLM-generated subtasks in heterogeneous robot capabilities and adapts subtasks from online feedback in unstructured environments [13]. These systems motivate our emphasis on grounding and feedback. The present paper focuses on a single Jackal-style deployment, but the same global \(\Phi_{\mathrm{mob}}\) shield and evolutionary planner can be extended to multi-robot missions by adding role assignment, communication, and shared-resource constraints.

10.0.0.5 Learning temporal logic.

Several works learn temporal-logic structures or parameters from data. The closest project reference learns STL predicates from trajectory data using expression optimization and conformal prediction to obtain finite-sample correctness guarantees [11]. Our constraint-mining phase uses a similar grammar-and-evaluator view, but the learned formula is a single global mobility constraint applied uniformly across every PDDL action at runtime.

10.0.0.6 Semantic safety and constitutions.

Robot constitutions and semantic safety benchmarks provide high-level rules and datasets for embodied safety [14]. Such rules are valuable for selecting or rejecting candidate instructions. Our STL constraint serves a different layer: after a task is judged appropriate, the executed robot trace must still maintain concrete measurable constraints.

References↩︎

---

1. Student at Westwood High School; work done as an intern at Texas A&M University.↩︎