File size: 1,970 Bytes
ba4f7c6 20ad86b ba4f7c6 4fe2273 ba4f7c6 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 | ---
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)
|