| --- |
| title: Minimum-Violation LTL Planning |
| emoji: 🤖 |
| colorFrom: blue |
| colorTo: red |
| sdk: gradio |
| sdk_version: "5.25.0" |
| app_file: app.py |
| pinned: false |
| license: mit |
| short_description: Interactive minimum-violation LTL planner (ACC 2013) |
| --- |
| |
| # Minimum-Violation LTL Planning |
|
|
| Interactive reproduction of: |
|
|
| > Tumova, Reyes-Castro, Karaman, Frazzoli, Rus — **"Minimum-Violation LTL Planning with Conflicting Specifications"** — ACC 2013. [arXiv:1303.3679](https://arxiv.org/abs/1303.3679) |
|
|
| ## What it demonstrates |
|
|
| When a robot's logical specifications conflict (e.g. "always avoid the danger zone" vs "reach the goal through the danger zone"), a standard planner simply fails. This algorithm instead finds the plan that **satisfies the highest-priority specs** and minimally violates the rest. |
|
|
| **Core idea:** |
| - Each spec φᵢ has a reward rᵢ (higher = harder to violate) |
| - Build the product automaton: grid × Büchi(φ₁) × Büchi(φ₂) × ... |
| - Find the max-reward strongly connected component (SCC) reachable from the start |
| - Reconstruct a lasso path (prefix + repeating cycle) through that SCC |
|
|
| **Try it:** drag the reward sliders to swap priorities — the planned path changes to satisfy whichever spec now has the highest weight. |
|
|
| ## Specs supported |
|
|
| | Formula | Meaning | |
| |---|---| |
| | `G(!p)` | Safety: never visit region p | |
| | `GF(p)` | Recurrence: visit p infinitely often | |
| | `F(p)` | Reachability: eventually reach p | |
| | `G(p)` | Invariance: always stay in p | |
|
|
| ## Implementation |
|
|
| Pure Python, no external tools: |
| - **Büchi automata** implemented directly for each formula pattern |
| - **Product automaton** built lazily via BFS |
| - **SCC detection** via Tarjan's algorithm |
| - **Lasso reconstruction** via BFS within the winning SCC |
| - **Visualization** via matplotlib → PIL → Gradio |
|
|
| ## Related work (Jana Tumova's group) |
|
|
| - [KTH RPL Planiacs](https://github.com/KTH-RPL-Planiacs) |
| - [Jana Tumova's homepage](https://sites.google.com/view/janatumova/home) |
|
|
