LTL with Team Semantics

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:

\[\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).\]

Team scenarios as HyperQB is able to correctly verify and synthesize the two traces in the team (i.e., \(\pi_{A}\) and \(\pi_{B}\)), correctly

Benchmarks

The Model(s)

--TEAMLTL
--(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);

Formula

exists A. exists B. forall C.
G(GOALA[A] <-> GOALA[C]) \/ G(GOALB[B] <-> GOALB[C])