LTL with Team Semantics (NuSMV)

Description of the Case Study

TeamLTL [VHF+20] can be presented as HyperLTL formulas by avoiding explicit references to traces (details in [VHF+20]). Since our focus is on HyperLTL, we only borrow the example with team scenarios from [VHF+20].

Consider an unknown input that affects the system behavior. To specify that executions either agree on \(a\) or \(b\) depending on the input, one can write the following HyperLTL formula:

The NuSMV model(s)

--(adopted from: Jonni Virtema, Jana Hofmann, Bernd Finkbeiner, Juha Kontinen, and Fan Yang. Linear-time temporal logic with team semantics: Expressivity and complexity. arXiv preprint arXiv:2010.03311, 2020)
MODULE main
VAR
  x_axis: 0..3;
  y_axis: 0..3;
  action: 0..4;
ASSIGN
  -- Initial Conditions
  init(x_axis):= 0;
  init(y_axis):= 0;
  init(action):= {0,1,2,3,4};

  -- Transition Relations
  next(x_axis) :=
    case
      (action=4): x_axis;
      ((action=0) | (action=1)): x_axis;
      ((action=2) & (x_axis=0)): x_axis;
      ((action=3) & (x_axis=3)): x_axis;
      ((action=2) & (x_axis!=0)): (x_axis - 1); -- action2: move left
      ((action=3) & (x_axis!=3)): (x_axis + 1); -- action3: move right
      TRUE: x_axis;
    esac;

  next(y_axis) :=
    case
      (action=4): y_axis;
      ((action=2) | (action=3)): y_axis;
      ((action=0) & (y_axis=0)): y_axis;
      ((action=1) & (y_axis=3)): y_axis;
      ((action=0) & (y_axis!=0)): (y_axis - 1); -- action 0: move down
      ((action=1) & (y_axis!=3)): (y_axis + 1); -- action 1: move up
      TRUE: y_axis;
    esac;

  next(action) := {0, 1, 2, 3};

DEFINE
  STARTED := !((x_axis=0) & (y_axis=0));
  gOALA := (x_axis=0) & (y_axis=3);
  gOALB := (x_axis=3) & (y_axis=0);

The HyperLTL formula(s)

Team semantics introduces existential witnesses for collective agreement. The HyperLTL encoding selects two traces that fix the values of propositions a and b; every other trace must agree with at least one of them forever.

\[\varphi_{\text{team}} = \exists \pi_A. \exists \pi_B. \forall \pi. \Box \left( a_{\pi_A} \leftrightarrow a_{\pi} \right) \lor \left( b_{\pi_B} \leftrightarrow b_{\pi} \right)\]
Exists A . Exists B . Forall C .
G(gOALA[A] = gOALA[C]) | G(gOALB[B] = gOALB[C])

References