Minimum-Violation LTL Planning

Reproducing: Tumova et al., "Minimum-Violation LTL Planning with Conflicting Specifications", ACC 2013

When robot specs conflict, instead of failing, this planner finds the path that satisfies the highest-priority rules and minimally violates the rest.

Try it: drag the reward sliders to swap priorities — watch the planned path change.

Scenario

Loading...

Spec Priorities (higher reward = harder to violate)

Never cross double line (danger zone)

0 200

Periodically visit pickup zone A

0 200

Periodically visit dropoff zone B

0 200

Eventually reach the goal

0 200

Generate animation (GIF)

How it works:

Each spec φᵢ becomes a Büchi automaton
Product automaton = grid × aut₁ × aut₂ × ...
SCCs with accepting states for each spec are found
Max-reward SCC → lasso path reconstructed

🔵 Prefix path 🔴 Repeating cycle 🟣 Start 🟠 Robot

Planned Path