Robust Path Planning (NuSMV, w/loops)¶

Description of the Case Study¶

We study robust path planning (RP) on a grid world, following . An agent must travel from a start cell to a goal cell while a set of adversaries moves under constrained dynamics (e.g., only clockwise). A path is robust if the agent can complete the mission regardless of how the adversaries move within their constraints.

This benchmark fits an \(\exists_{\text{agent}}\,\forall_{\text{adv}}\) setting: we search for one agent strategy such that all adversary behaviors fail to intercept it. Using HyperQB, we encode conformance as a SIMAE-style relation between an agent trace and an adversary trace family and check the HyperLTL condition below. We provide a satisfiable instance (a robust path exists) and an unsatisfiable one (no robust path).

The NuSMV model(s)¶

MODULE main
VAR
  b_state : 1..10;
ASSIGN
  init(b_state) := 1;
  next(b_state) :=
    case
      b_state = 1  : 2;
      b_state = 2  : {2,3};
      b_state = 3  : {1,3,4};
      b_state = 4  : {1,4,5};
      b_state = 5  : {5,6};
      b_state = 6  : {6,7};
      b_state = 7  : {7,8};
      b_state = 8  : {8,9};
      b_state = 9  : 10;
      b_state = 10 : 10;
      TRUE         : b_state;
    esac;

MODULE main
VAR
  a_state : 1..9;
ASSIGN
  init(a_state) := 1;
  next(a_state) :=
    case
      a_state = 1 : {2,4};
      a_state = 2 : {3,5};
      a_state = 3 : 6;
      a_state = 4 : {5,7};
      a_state = 5 : {6,8};
      a_state = 6 : 9;
      a_state = 7 : 8;
      a_state = 8 : 9;
      a_state = 9 : 9;
      TRUE         : a_state;
    esac;

MODULE main
VAR
  a_state : 1..9;
ASSIGN
  init(a_state) := 1;
  next(a_state) :=
    case
      a_state = 1 : 2;
      a_state = 2 : 3;
      a_state = 3 : 4;
      a_state = 4 : 5;
      a_state = 5 : 6;
      a_state = 6 : 7;
      a_state = 7 : 8;
      a_state = 8 : 9;
      a_state = 9 : 9;  
      TRUE         : a_state;
    esac;

The HyperLTL formula(s)¶

We require that the agent never occupies the same cell as the adversaries, for all adversary behaviors; optionally we can also require eventual reachability of the goal.

\[\begin{aligned} \varphi_{\mathrm{RP}} \;=\; \exists \pi_{\text{agent}}.\ \forall \pi_{\text{adv}}.\ \mathbf{G}\,\big(\mathit{pos}_{\pi_{\text{agent}}} \neq \mathit{pos}_{\pi_{\text{adv}}}\big). \end{aligned}\]

Exists P . Forall Q .  G((a_state[P]=9)|(a_state[P]=1)|~(a_state[P]=b_state[Q]))

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.