Source-linked AI summary
PanelShield: Verifiable Closed-Loop Safe Planning for Robotic Industrial Panel Operation
Guipeng Xin, Jiahe Xu, Chenhui Wan, Jie Liu, Youmin Hu, Zhongxu Hu
TL;DR
Industrial panel operation couples procedures with device states, while existing approaches lack both scalable auditability and computable, localizable feedback for correcting unsafe plans. PanelShield grounds manual procedures in constraints, combines LTL and Safety FSM verification with counterexample-guided repair, and improves high-complexity task success while reducing safety violations in simulation and real-world execution.
Problem
Industrial panel operation requires state-dependent procedures and strict constraints, but existing methods trade device-specific auditability for foundation-model plans that may omit checks or violate interlocks.
Method
PanelShield grounds manual procedures in computable constraints, combines LTL and Safety FSM verification, and uses structured counterexamples to guide local repair and re-verification.
Results
PanelShield largely preserves low-complexity performance while improving high-complexity task success and reducing violation rates in simulation and real-world robotic execution.
Takeaways & Limitations
PanelShield provides a verifiable closed-loop approach that generates procedure-compliant operation sequences and verifies critical steps through feedback during chained-task execution.
Takeaways & Limitations
Deployment to new panel families still requires expert-audited compilation of manual clauses into LTL/FSM templates, and verification depends on reliable symbolic states derived from perception.
Abstract
from arXiv · showhide
Industrial panel operation is knowledge-intensive and safety-critical. Beyond control recognition and action generation, execution must satisfy constraints in operation manuals and safety regulations. While foundation-model-based planners show strong semantic capability, they typically lack computable, localizable, and reproducible mechanisms for violation detection and repair. To address this, we propose PanelShield, a verifiable closed-loop safety planning framework for manual-guided industrial panel operation. The framework generates parameterized action primitive sequences from task-relevant manual evidence and applies dual formal verification with LTL and a Safety FSM to enforce cross-step temporal correctness and local transition legality. When violations occur, it outputs a structured counterexample with the earliest violating step and cause, enabling targeted repair and re-verification. We build a multi-level long-horizon planning benchmark covering three representative industrial device panels, and evaluate the framework in simulation and real-world robotic experiments. Results show that PanelShield improves complex safety-constrained task performance over foundation-model-only planning baselines while reducing the violation rate to 2.7%, with 4.1 s total latency. Real-world experiments demonstrate end-toend feasibility. Overall, PanelShield offers a verifiable approach to robotic panel operation that balances flexibility, safety, and auditability.
I. INTRODUCTION
Industrial panel operation couples device states with dispersed procedural and safety constraints, creating a gap between flexible foundation-model planning and verifiable execution. PanelShield addresses this gap with computable constraints, dual verification, and targeted closed-loop repair.
- Industrial panel operation requires state-dependent action orders, ranges, interlocks, preconditions, prohibitions, temporal dependencies, and thresholds from manuals and regulations.
- Foundation-model planners provide semantic flexibility and long-horizon reasoning but may violate interlocks, omit state checks, and lack step-level violation explanations.
- PanelShield generates parameterized action primitives from task-relevant manual evidence and constructs computable execution traces for verification.
- LTL checks global temporal correctness while a Safety FSM checks local transition legality, producing rule- and step-level counterexamples for targeted repair.
- The framework is validated on long-horizon benchmark tasks and a real robotic arm platform, with improved task success and reduced safety violations under acceptable latency.
B. Task-Level Safety for LLM Agents
Task-level safety requires converting procedural knowledge into computable representations rather than relying on textual reminders or implicit prompt constraints. PanelShield uses parameterized primitives, symbolic execution traces, and counterexample-guided repair to support decidable, localized checking.
- Task-Level Safety for LLM Agents: Industrial task-level safety depends on correct operation orders, satisfied preconditions, and procedural prohibitions, not only motion-level collision avoidance.
- Task-Level Safety for LLM Agents: Existing methods may detect unsafe plans without identifying which step violates which rule, while industrial procedures require both temporal and transition-legality checks.
- Evidence-Conditioned Planning: PanelShield converts task-relevant manual constraints into computable LTL/FSM rules and produces a final executable safe plan through closed-loop verification and repair.
- Evidence-Conditioned Planning: At each planning step, the system conditions on an instruction, device snapshot, and relevant manual evidence, then outputs a verified safe plan.
- Evidence-Conditioned Planning: Parameterized action primitives provide explicit step boundaries and primitive-specific parameters that anchor stable references to the earliest violating step.
- Evidence-Conditioned Planning: Symbolic abstraction and transition modeling support procedural checking and localization, while ambiguous observations trigger failed checks or reobservation rather than unsafe approval.
B. Dual Formal Checking
PanelShield separates procedural safety into global temporal properties and local transition legality. It applies complementary formal checks that return structured violation locations and causes for subsequent repair.
- Dual Formal Checking: Global temporal properties encode cross-step requirements such as satisfied preconditions and prohibitions activated by prior states.
- Dual Formal Checking: Local transition legality governs allowable actions and intermediate transitions under device modes and interlocks.
- Dual Formal Checking: The temporal checker labels symbolic configurations with propositions and evaluates compiled global constraints over the resulting proposition sequence.
- Dual Formal Checking: Temporal verification identifies the violated constraint and earliest violation index, localizing both the rule and approximate step.
- Dual Formal Checking: The Safety FSM checks each run step and reports the first illegal step with a human-readable cause such as a missing intermediate mode or interlock-forbidden action.
C. Counterexample-Guided Repair Loop
PanelShield turns verification failures into structured, step-localized counterexamples that guide minimal plan repairs. It repeats checking and repair until both formal checks pass or the iteration budget is reached.
- C. Counterexample-Guided Repair Loop: A structured counterexample converts temporal and automaton failures into actionable repair signals for constrained replanning.This shifts repair from unconstrained rewriting toward minimal local edits that improve convergence and plan stability.
- C. Counterexample-Guided Repair Loop: Each counterexample records the earliest violating step, violated rule, cause, supporting manual clause, and minimal edit direction.Supported edits include inserting checks or transitions, reordering steps, and replacing illegal primitives.
- C. Counterexample-Guided Repair Loop: The planner conditions the next candidate plan on the counterexample to perform targeted repair.The repair signal is passed into the next planning iteration rather than restarting from an unconstrained generation process.
- C. Counterexample-Guided Repair Loop: PanelShield repeats run construction, dual checking, counterexample generation, and repair until both checks return OK or the iteration budget is reached.The final output is the verified plan π⋆.
- C. Counterexample-Guided Repair Loop: The closed loop provides a localizable and reproducible error-correction mechanism for ordering errors, missing preconditions, and illegal transitions.Its stated purpose is to reduce high-risk execution errors associated with these procedural failures.
A. Benchmark Setup
The benchmark evaluates manual-guided panel planning across three representative industrial devices, three instruction-complexity levels, and simulation-to-real deployment settings. It measures task success, safety, repair behavior, and latency.
- A. Benchmark Setup: The benchmark covers VFD controllers, Power Management Systems, and Hydraulic Control Units.Each device category includes operation manuals, safety regulations, and technical specification documents.
- A. Benchmark Setup: Instructions span Level-1 single-step adjustments, Level-2 sequential operations, and Level-3 composite tasks with explicit safety constraints.The final benchmark contains 300 rigorously validated user instructions.
- A. Benchmark Setup: The study includes a counterexample-guided repair case paired with an expert-defined reference task plan sequence as ground truth.The referenced case illustrates the closed-loop repair setting used by PanelShield.
- A. Benchmark Setup: Real-world experiments use a motor drive controller simulator with a ROS 2 robotic system integrating perception, planning, and motion control.A RealSense D435i depth camera supports control detection and pose estimation.
- A. Benchmark Setup: Evaluation reports Success Rate, Violation Rate or Compliance Rate, average repair iterations, and runtime overhead, with real-world tests focusing on chained-task reasoning and execution time.These measures assess completion, safety, convergence, online usability, and end-to-end deployability.
1) Simulation Planning Baselines:
Simulation compares direct generation, prompt-based safety constraints, post-hoc judging, and PanelShield’s dual-checking repair process. PanelShield performs best on complex-task success and safety, including Level-3 tasks.
- 1) Simulation Planning Baselines:: The simulation compares LLM-only, Prompt-Safety, Post-hoc Judge, and PanelShield across industrial panel operation tasks.PanelShield combines LTL and Safety FSM checking with earliest-step and cause reporting for targeted repair.
- 1) Simulation Planning Baselines:: PanelShield achieves the best overall performance on complex-task success and safety.The supplied results identify this as the overall simulation finding.
- 1) Simulation Planning Baselines:: 43.0% Level-3 success is highest for PanelShield, exceeding LLM-only at 22.0%, Prompt-Safety at 33.0%, and Post-hoc Judge at 39.0%.The corresponding improvements are 21.0, 10.0, and 4.0 percentage points, respectively.
- 1) Simulation Planning Baselines:: 2.7% violation rate is lowest for PanelShield, compared with 8.3% for Prompt-Safety and 3.5% for Post-hoc Judge.The result is reported for the simulation baseline comparison.
- 1) Simulation Planning Baselines:: The simulation reports repair iterations and planning-time overhead as additional evaluation measures.The supplied table caption identifies these two quantities as the focus of Table I.
2) Repair Iterations and Planning Time Overhead:
PanelShield combines dual formal verification with localized counterexample-guided repair, reducing unnecessary plan rewriting while maintaining acceptable planning overhead.
- Repair iterations: Structured counterexamples identify the earliest violating step and cause, enabling local revisions instead of whole-plan rewrites.Post-hoc Judge often rewrites the whole plan because it lacks this localization.
- Planning time overhead: Although dual verification adds computation, lightweight checkers are faster than LLM-based judging and keep latency acceptable while improving safety.LLM-only and Prompt-Safety are fastest because they omit formal verification.
- Verification ablation: The full method achieves the lowest violation rates under both LTL and Safety FSM checking.Removing either verifier increases the burden on the other and raises violation rates.
- Verification ablation: Earliest-violation Step rises to 2.4 without LTL and 2.5 without FSM, indicating weaker early truncation of unsafe plans.The ablation compares the full method with removal of either verifier.
- Repair locality: Post-hoc Judge has a later earliest violation and the largest average repair edit size, whereas the full method yields the smallest average edit size.These results indicate holistic rewriting versus targeted local repair.
4) Real-World End-to-End Experiments:
Real-world experiments evaluate PanelShield on long-horizon chained tasks, where feedback-based state checks support procedure-compliant execution. The system demonstrates end-to-end feasibility with practical inference and execution times, while deployment remains bounded by several safety-related limitations.
- Execution efficiency: Inference time is 3.5–5.6 s and execution time is 4.2–10.7 s using GPT-4o as the planner.These measurements are reported for chained-task execution on an actual device.
- Chained-task execution: The real-world system decomposes “Switch source from PANEL to VFD, set speed, then start” into required steps and execution conditions.It also reuses operation parameters from the previous task and checks critical states at the subtask level.
- Feedback-based verification: Indicator lights and display values provide feedback for verifying critical steps during procedure-compliant chained-task execution.The case study reports stable execution on real devices.
- Limitations: New panel families require expert-audited compilation of manual clauses into LTL/FSM templates, limiting immediate scalability.The paper proposes automating evidence extraction while retaining human approval for safety rules.
- Limitations: Verification depends on the reliability of symbolic states derived from perception, requiring conservative handling of noisy or uncertain observations.The paper identifies confidence thresholds, repeated observation, and fail-safe stops as needed safeguards.