Reproduce “Correct-by-Construction Behavior Tree Synthesis from Signal Temporal Logic Specifications with Application to Robotic Missions” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Jiaheng Dong, Jingyi Huang, Liang Han
This work introduces a formal framework for synthesizing correct-by-construction Behavior Trees (BTs) directly from Signal Temporal Logic (STL) specifications, enabling autonomous robots to satisfy complex missions with quantitative timing constraints. The method guarantees forward invariance and monotonic progress, demonstrating high satisfaction rates in simulations and successful execution on a physical quadrotor even with disturbances.
Key insights
- It is possible to formally synthesize modular and reactive Behavior Trees that guarantee satisfaction of quantitative timing constraints expressed in Signal Temporal Logic.
- The framework ensures both forward invariance (safety) and monotonic progress (liveness) for concurrently active tasks, even when facing environmental non-determinism, by staying within a pre-computed winning set.
- Decomposing complex STL specifications into hierarchical BT subtrees allows for interpretable, modular control while retaining formal guarantees over the entire mission.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.