PaperlayerView exact revision on arXiv

Source-linked AI summary

CSymPlan: Certified Symbolic Planning and Control for High-DOF Manipulators

Aditya Narendra, Ashok Kumar Saini, Mahathi Anand, Mahmoud Khaled, Fares J. Abu-Dakka, Abdalla Swikir

arXiv:2608.22983v1cs.ROeess.SY

TL;DR

Conventional plan–then–track manipulation can produce unsafe references under execution uncertainty and tight clearances. CSymPlan synthesizes certified symbolic reach-avoid feedback policies offline for fixed workspaces or online for changing tasks and perceived obstacles, using an operational-space abstraction with torque-level refinement. In representative simulation and Franka FR3 experiments, it reports zero safety violations and avoids executing uncertified commands.

  • Problem

    Conventional planning and low-level tracking can leave collision-free references unsafe under tracking errors, actuator limits, unmodeled dynamics, and sensing errors.

  • Method

    CSymPlan synthesizes certified symbolic reach-avoid feedback policies over an operational-space abstraction and refines their actions through torque control, offline or online via pFaces.

  • Results

    94% task success, 0% safety violations, and 100% safe resolution are reported across the representative online Isaac Sim benchmark.

  • Takeaways & Limitations

    The framework connects formal reach-avoid guarantees with real robotic execution in cluttered and changing workspaces without executing uncertified commands.

Abstract

from arXiv · show

Robot manipulators are commonly engineered around a decoupled motion-generation stack: a planner computes a collision-free path and a lower-level controller tracks the resulting reference. This separation is computationally convenient, but it can produce references that are difficult to execute under actuator limits, tracking error, model mismatch, and small obstacle clearances. We present CSymPlan, a certified symbolic planning and control framework for high-DOF manipulators with two complementary implementations: an offline implementation that precomputes certified reach-avoid feedback policies for known workspaces; and an online implementation that synthesizes or updates symbolic policies at runtime from changing task and perception information using parallelization. The offline implementation reduces the manipulator dynamics to a sampled perturbed double-integrator model in operational space through feedback linearization, treats torque-realization errors, modeling inaccuracies, and measurement uncertainty as bounded disturbances, and refines the synthesized symbolic policy to the Franka FR3 through a quantization--lookup--torque realization pipeline. The online implementation uses the same abstraction and refinement interface, but replaces the precomputed policy table with a runtime pFaces request--synthesis--execution loop. In randomized simulated benchmarks and perception-driven Franka FR3 experiments, both implementations complete reach-avoid tasks with zero safety violations; whenever no certified action exists, the robot holds, replans, or stops safely instead of executing an uncertified command.

I. INTRODUCTION

CSymPlan addresses the execution gap in conventional plan–then–track manipulation by synthesizing certified feedback policies over finite abstractions of closed-loop task-space dynamics. It combines offline and online implementations to support known and changing workspaces while targeting scalable high-DOF control.

  • Conventional planners can produce paths that become unsafe under tracking errors, actuator saturation, unmodeled dynamics, or sensing errors.
  • CSymPlan synthesizes symbolic feedback policies whose abstract successors remain in a certified winning set for reachability and safety specifications.
  • Operational-space feedback linearization reduces high-DOF manipulators to a tractable Cartesian double-integrator abstraction while retaining torque-level refinement.
  • Offline CSymPlan precomputes policies for fixed workspaces, obstacle sets, and goals, whereas online CSymPlan refreshes policies for runtime-changing tasks and perceived obstacles.
  • The framework evaluates reach-avoid manipulation across simulation and Franka FR3 experiments using success, safety, timing, path, smoothness, and effort measures.
  • Unlike task-and-motion planning, symbolic control uses symbols for regions of continuous state and input spaces and synthesizes feedback policies over those regions.

C. Sampled perturbed control systems

The paper models sampled perturbed dynamics as set-valued transitions and specifies controller behavior through invariance, reachability, and reach-avoid properties. A finite abstraction and feedback-refinement relation transfer these guarantees to the concrete system.

  • A sampled perturbed control system is represented by state set X, input set U, and set-valued transition map F under sampling period s.
  • Invariance requires the closed-loop system to remain in the safe set, while reachability requires reaching the goal within a finite horizon.
  • Reach-avoid specifications combine safety throughout execution with eventual goal attainment from the initial set.
  • A controller satisfies a specification when all of its closed-loop behaviors are contained in the specification set.
  • Symbolic synthesis constructs a finite abstraction that over-approximates the sampled perturbed system and connects it to concrete states through quantization.
  • Feedback refinement requires abstract inputs to remain concrete-admissible and quantized concrete successors to remain within abstract successors.

IV. METHODOLOGY

Both CSymPlan implementations share a symbolic abstraction and refinement interface, differing mainly in when winning sets and admissible actions are computed. The method models task-space uncertainty conservatively and targets certified reach-avoid torque control.

  • The offline implementation precomputes a fixed symbolic controller, while the online implementation recomputes finite-horizon winning sets from current state, targets, and obstacles.
  • CSymPlan chooses a task-space command interpreted as desired end-effector acceleration and derives a perturbed double-integrator model.
  • Disturbance bounds include external-force residuals, modeling, discretization, measurement, and torque-realization errors.
  • The sampled model uses compact inputs selected to respect actuation limits, with disturbance and measurement bounds calibrated conservatively from representative torque-controlled motions.
  • Obstacle inflation defines a position-level safe set, with the safety margin covering tool geometry and uncertainty represented by the disturbance and measurement bounds.
  • Reach-avoid control is synthesized for workspace, obstacles, uncertainty bounds, initial states, and goal sets; waypoint tasks use separate policies switched after goal attainment and hold time.

V. IMPLEMENTATION

The offline implementation synthesizes a finite symbolic reach-avoid policy once, then executes it in real time by quantizing measured states, looking up actions, and refining Cartesian accelerations into torques.

  • The offline pipeline discretizes task-space states and admissible accelerations, over-approximates disturbed successors, and synthesizes reach-avoid controllers by fixed-point computation.
  • The resulting policy is exported as a binary decision diagram or lookup table for constant-time runtime evaluation.
  • At each servo tick, joint feedback is converted to a task-space state, quantized, and mapped to a symbolic virtual acceleration.
  • The selected Cartesian acceleration is realized through an operational-space wrench and joint torque command.
  • A fixed null-space PD term supports posture regulation, damping, and joint-limit avoidance during torque realization.

3) Offline guarantee boundary:

CSymPlan’s guarantee transfers from the symbolic controller to the physical manipulator only under explicit abstraction, refinement, disturbance, model, and safety-margin assumptions.

  • The certificate requires the abstract transition relation to over-approximate sampled perturbed successors and the refinement error to remain within the synthesized disturbance bound.
  • The guarantee also assumes conservative abstract safe and goal sets, an accurate workspace and obstacle model after safety inflation, and a sufficient end-effector margin.
  • If the quantized initial state lies in the computed winning set, every refined closed-loop execution satisfies the reach-avoid specification.
  • Hardware experiments provide empirical evidence that calibrated bounds were conservative enough for the stated assumptions in the reported setup.
  • Task-space abstraction is chosen for tractability, whereas joint-space abstraction would provide joint-level guarantees at substantially higher dimensionality for a 7-DOF arm.

2) Online reach-avoid synthesis:

Online CSymPlan recomputes finite-horizon symbolic reach-avoid policies for changing task and perception information while reusing a fixed abstraction and selecting only certified actions.

  • Each online request computes a finite-horizon reach-avoid fixed point over the shared abstract transition relation.
  • The resulting time-indexed controller returns admissible actions whose abstract successors remain inside the remaining winning sets.
  • If the current abstract state is outside the initial winning set, the engine returns no certified action and the robot holds while a modified request may be submitted.
  • When multiple certified actions exist, a one-step progress cost selects among them without expanding the certified action set.
  • The online architecture senses the environment, updates obstacle and uncertainty models, requests synthesis from pFaces, and refines returned commands through torque realization.

3) Online buffered execution:

Online execution separates lower-rate symbolic planning from high-frequency torque control by buffering certified command segments and rejecting stale commands.

  • A background planning thread contacts the online server below the servo rate and requests new policies when buffered certified time approaches its threshold.
  • Each buffered symbolic action is applied as a constant task-space acceleration over one symbolic sampling interval.
  • The online controller forms the realized acceleration and uses the same operational-space torque refinement as the offline implementation.
  • Before activation, each buffered command is checked against the current measured state and discarded if the certification condition fails.
  • If the buffer is empty, the robot holds the last certified reference while waiting for a new winning set and certified actions.

4) Online guarantee boundary:

The online implementation computes certified command segments from measured state, target, obstacle, and horizon information while reusing a fixed abstraction. Its guarantee is local to each accepted request and remains valid across replanning only under explicit state-matching and environment-validity conditions.

  • Guarantee scope: The online reach-avoid guarantee is local to the state, safe set, goal set, and horizon used in each server request.Proposition 1 applies per request rather than to one globally fixed certificate.
  • Online request synthesis: Online synthesis builds request-specific safe and goal sets, computes finite-horizon winning sets, and stores admissible symbolic actions before execution.The request uses measured state, target tube, obstacle set, and horizon with fixed grids, inputs, and transition relation.
  • Guarantee scope: Across replanning calls, the guarantee holds when accepted buffered commands satisfy the state-matching condition and the runtime obstacle model remains valid until the next update.The physical realization errors must remain within the disturbance, measurement, and torque-refinement bounds used by the abstraction.
  • Failure handling: When no winning action exists or the environment invalidates the safe set, the implementation holds, replans, widens the target tube within bounds, or stops safely.The guarantee excludes uncertified fallbacks and environmental changes occurring before a new certified request is accepted.
  • Online execution: The runtime loop asynchronously requests certified segments, buffers them, selects valid commands, and realizes references through the torque-controlled robot loop.Execution senses the robot state, checks buffer status, samples references from active certified commands, and applies torques subject to limits.

A. Offline evaluation

The offline evaluation tests a precomputed symbolic policy in fixed workspaces through hardware execution and randomized simulation against planning-and-control baselines. CSymPlan achieves 100% success with no recorded safety violations, while paying a larger one-time synthesis cost for constant-time runtime lookup.

  • Offline hardware evaluation: The offline policy is synthesized for fixed workspace, obstacles, and goals, then exported for runtime state estimation, quantization, lookup, and torque realization.The Franka FR3 control loop runs at 1 kHz with fixed low-level gains across trials.
  • Offline hardware evaluation: Five static Franka FR3 scenes use a reach-avoid criterion requiring goal entry and Nhold consecutive ticks while remaining safe throughout execution.Trials use increasing obstacle complexity, with boxes, cylinders, and meshes under shared execution and actuation limits.
  • Offline simulated benchmarking: The PyBullet benchmark compares CSymPlan with RRT, LQR-RRT⋆, MPPI, and Neural MPC under shared task, dynamics, safety, and torque-realization settings.Using the same low-level realization layer isolates the decision-layer comparison.
  • Offline hardware evaluation: Hardware metrics report end-effector tracking error, commanded joint-torque norm, and measured joint-velocity norm over N = 5 trials per scene.Figure 6 displays means and one-standard-deviation bands over normalized execution time.
  • Offline simulated benchmarking: 100% success with no recorded safety violations is achieved by CSymPlan across randomized trials.The offline metrics cover reliability, motion quality, and mean and 95th-percentile online computation time per control step.
  • Offline simulated benchmarking: 290 s of total offline computation trades against a constant-time runtime policy lookup after synthesis.The reported total comprises 75 s for abstraction construction and 215 s for fixed-point synthesis, compared with 6.2 s average offline RRT planning time.

B. Online evaluation

The online evaluation reuses a fixed symbolic abstraction while updating safe and target sets from task and perception information. It tests request–synthesis–execution under shelf, maze, moving-obstacle, high-speed, and real-world perception-driven tasks.

  • Online simulation: The online simulation stack constructs symbolic grids and the transition relation once, then updates only current safe and target sets during replanning.pFaces computes finite-horizon winning sets and admissible actions from each measured state and scene update.
  • Online simulation: Simulation covers shelf reach-avoid, three-dimensional maze, and moving-obstacle tasks with changing geometry and narrow or time-varying safe regions.The moving-obstacle family updates occupancy over time and evaluates online replanning when the safe set changes.
  • Online simulation: Online simulated evaluation measures success, safety violations, time-to-goal, path length, clearance, smoothness, torque effort, replanning calls, and synthesis latency.These metrics assess both motion quality and runtime synthesis behavior.
  • Online hardware: Real-robot experiments use a Franka FR3 with background pFaces requests, buffered symbolic accelerations, and servo-rate torque realization.The hardware stack computes the measured end-effector state in the Franka base frame before submitting synthesis requests.
  • Online hardware: Perception-driven obstacle updates use DNVblox at 10 Hz while the libfranka torque callback remains at the robot servo rate.Each request uses the latest inflated voxel-map obstacle snapshot.
  • Online hardware: Real-robot task families include high-speed reach, dynamic-obstacle reach-avoid, and dynamic maze execution.Dynamic-obstacle trials discard stale buffered commands when the measured state no longer matches the certified command start state.
  • Online hardware: Hardware evaluation records success, safety-stop reason, timing, tracking error, clearance, buffer underruns, synthesis latency, torque metrics, and joint velocity.The procedure checks the initial symbolic-domain and target-distance conditions before enabling motion.

3) Online benchmark baselines:

The online benchmark compares CSymPlan with optimization, sampling-based, geometric, reactive safety-filter, and learned controllers under shared task-space and torque interfaces. Evaluation distinguishes reaching the goal from certified safe resolution, including safe handling when no certified action remains.

  • The benchmark includes deterministic optimization, stochastic MPPI, RRT-Connect with trajectory tracking, CBF-QP, and Neural MPC.These represent online optimization, sampling-based control, decoupled planning and tracking, reactive safety filtering, and learned receding-horizon control.
  • All baselines share initial states, target sets, obstacle sets, control periods, actuation limits, and termination logic.
  • CSymPlan evaluates both task completion and certified safe resolution rather than treating every uncertified request as a safety violation.A certified action is guaranteed only when the current abstract state lies in the finite-horizon winning set for the current specifications and disturbance bounds.
  • The online evaluation also tracks time-to-goal, path length, minimum clearance, synthesis latency, replanning, stale segments, map age, and tracking quality.
  • 94% aggregate success, 0% safety violations, and 100% safe resolution are reported across three Isaac Sim task families and 50 trials per family.Remaining trials are safe stops or timeouts, primarily in narrow-maze and moving-obstacle settings where winning actions disappear or buffered commands become stale.

6) Online hardware task outcomes:

Perception-driven Franka FR3 experiments evaluate online CSymPlan across representative hardware tasks with DNVblox obstacle maps. The system maintains safety by rejecting stale commands and stopping safely when certified continuation is unavailable.

  • 27 of 30 Franka FR3 trials succeed, with 0 observed safety violations and 100% safe resolution.The three non-successful trials terminate as certified stops rather than collisions.
  • The controller rejects commands when the measured state no longer matches the certified segment start state and then triggers replanning.If synthesis cannot certify a continuation, it holds the last certified reference or terminates safely.
  • The Franka experiments use DNVblox perception, with map age reported as the elapsed time from voxel-map update to the pFaces request.
  • Hardware failures are certified stops caused by no winning action, stale-segment rejection, or failure to find a certified continuation in narrow passages.
  • The hardware comparison includes online CSymPlan and representative planning-and-control baselines under matched simulation conditions.Baselines may produce shorter or faster motions in open scenes but lack the same cell-wise reach-avoid certificate.
  • Across the hardware trials, 30 of 30 end in either success or certified safe stop.The reported mean pFaces latency is 153 ms and the 95th-percentile latency is 410 ms.

VII. CONCLUSION AND FUTURE WORK

CSymPlan replaces decoupled plan–then–track execution with certified symbolic feedback over a finite task-space abstraction, supporting both fixed-workspace and changing-environment manipulation. The framework connects formal reach-avoid guarantees to torque-controlled execution while identifying scalability, specification, joint-space, and perception boundaries for future work.

  • Conclusion: CSymPlan synthesizes feedback policies over a finite abstraction of closed-loop task-space dynamics and refines their actions into torque-level control on the Franka FR3.The abstraction uses a sampled perturbed double-integrator model, while execution proceeds through quantization, policy lookup, and torque realization.
  • Conclusion: The offline implementation provides constant-time runtime control for a fixed workspace, obstacle set, and goal, whereas the online implementation handles changing tasks and perception-driven obstacle maps through buffered certified command segments.Online synthesis is separated from the high-frequency torque loop and avoids rebuilding the full abstraction for each update.
  • Conclusion: Both implementations preserve a safe reach-avoid interface: uncertified continuations are rejected, and the robot holds, replans, or stops safely when no winning action exists.The safety claim is conditional on the stated abstraction, disturbance, perception, and refinement assumptions rather than universal task feasibility.
  • Scalable and structure-aware abstractions: The main computational bottleneck is constructing and solving the finite abstraction, whose state count grows with workspace dimension, velocity bounds, and grid resolution.Proposed remedies include adaptive, nonuniform, structure-aware abstractions and more aggressive parallelization, pruning, and caching.
  • Expressive specifications and hybrid certification: Future extensions could combine symbolic certification with non-symbolic planners and local funnels, while expanding specifications beyond reach-avoid tasks to temporal objectives.These directions aim to reduce the symbolic region requiring certification and represent ordered visits, dwell constraints, and other long-horizon objectives.
  • Certification scope and perception: The current abstraction is limited to translational end-effector position and velocity and does not directly cover orientation, joint limits, self-collision, payload-dependent dynamics, or contact modes.Perception-aware certification is also left for future work because current obstacle maps use inflated depth-derived occupied voxels without explicitly modeling map age, confidence, occlusion, or depth uncertainty.
Loading 2608.22983v1…