Deep magic, but basic ideas

• Encode state transitions as Ordered Binary Decision Diagrams
• Given planning domain Σ= (S, A, ϒ) where nodeterministic ϒ: S x A → 2^S
• Generate sets of plans {π ={(s,a)} | s ∈ S, a ∈ A(s), ∀ s, ∃! (s,a) ∈ π}
• Take goal Ψ and model check for paths to goal.
• Action 0: Pre: ∼X₁ ∧ ∼X₂, Effect: ∼X₁
• Action 1: Pre: X₁, Effect: (X₁ ∧ ∼ X₂ → ∼X₁) ∧ (X₁ ∧ X₂ → X₁)