Plan Synthesis: Wolf–Goat–Cabbage (NuSMV, w/loops)

Description of the Case Study

We consider plan synthesis (PS) in the classic wolf–goat–cabbage puzzle, following . A farmer must ferry three items across a river, carrying only one at a time. Certain configurations are unsafe (wolf with goat, goat with cabbage) if left unattended. The goal is to synthesize a single plan that always avoids all local requirement violations.

This is an \(\exists_{\text{big}}\,\forall_{\text{small}}\) problem: we search for one big plan that, for every small requirement automaton (encapsulating local violations), maintains safety. We provide a satisfiable instance (a robust plan exists) and an unsatisfiable one (a broken plan step that inevitably violates a requirement).

The NuSMV model(s)

Plan (big) — correctRequirements (small)Plan (big) — buggy

MODULE main
VAR
  a_state : 0..16;

ASSIGN
  init(a_state) := 0;
  next(a_state) :=
    case
      a_state = 0  : {1, 8, 9};
      a_state = 1  : 2;
      a_state = 2  : 3;
      a_state = 3  : 4;
      a_state = 4  : {5, 14};
      a_state = 5  : 6;
      a_state = 6  : 7;
      a_state = 7  : 0;
      a_state = 8  : 10;
      a_state = 9  : 4;
      a_state = 10 : 11;
      a_state = 11 : 12;
      a_state = 12 : 13;
      a_state = 13 : 0;
      a_state = 14 : 15;
      a_state = 15 : {16, 3};
      a_state = 16 : 0;
      TRUE         : a_state; -- totalize (remove if you want a strict graph)
    esac;

-- Violation atoms (match y_labels 1..4)
DEFINE
  bad_gc    := (a_state = 8);   -- L=GC,R=FW
  bad_fw_gc := (a_state = 15);  -- L=FW,R=GC
  bad_gw    := (a_state = 9);   -- L=GW,R=FC
  bad_fc    := (a_state = 12);  -- L=FC,R=GW
  safeA     := !(bad_gc | bad_fw_gc | bad_gw | bad_fc);

The HyperLTL formula(s)

The paper formulates plan synthesis as ensuring that the plan’s action never matches any violation of the requirement automaton, at all times:

\[\varphi_{\mathrm{PS}} \;=\; \exists \pi_{\text{big}}.\ \forall \pi_{\text{small}}'.\ \mathbf{G}\,\big(\mathit{action}_{\pi_{\text{big}}} \not\leftrightarrow \mathit{violation}_{\pi_{\text{small}}'}\big).\]

In our concrete encoding, the big model exposes four violation atoms

\(\mathit{bad\_gc},\ \mathit{bad\_fw\_gc},\ \mathit{bad\_gw},\ \mathit{bad\_fc}\)

and the small model exposes matching labels

\(\mathit{gc},\ \mathit{fw\_gc},\ \mathit{gw},\ \mathit{fc}\).

A pointwise version of \(\varphi_{\mathrm{PS}}\) is:

\[\begin{split}\begin{aligned} \varphi_{\mathrm{PS}} \;=\; \exists \pi_{\text{big}}.\ \forall \pi_{\text{small}}'.\ \mathbf{G}\big(&\neg(\mathit{bad\_gc}_{\pi_{\text{big}}} \land \mathit{gc}_{\pi_{\text{small}}'}) \ \land \\ &\neg(\mathit{bad\_fw\_gc}_{\pi_{\text{big}}} \land \mathit{fw\_gc}_{\pi_{\text{small}}'}) \ \land \\ &\neg(\mathit{bad\_gw}_{\pi_{\text{big}}} \land \mathit{gw}_{\pi_{\text{small}}'}) \ \land \\ &\neg(\mathit{bad\_fc}_{\pi_{\text{big}}} \land \mathit{fc}_{\pi_{\text{small}}'})\big). \end{aligned}\end{split}\]

Formula

Exists A . Forall B . G((gc[B] | fw_gc[B] | gw[B] | fc[B]) -> (~bad_gc[A] & ~bad_fw_gc[A] & ~bad_gw[A] & ~bad_fc[A]))

References

Filiot, Emmanuel; Lagarde, Guillaume; Laroussinie, François; Markey, Nicolas; Raskin, Jean-François; and Sankur, Ocan. “Efficient Loop Conditions for Bounded Model Checking Hyperproperties.” arXiv:2301.06209, 2023.