A newer version of the Gradio SDK is available: 6.14.0
metadata
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
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