GR(1)

Generalized Reactivity(1)

Also known as:

• generalized Streett[1]

summary

GR(1) specifications define 2-player games with transition requirements (safety) and liveness conditions assigned to each player. If the adversary satisfies its liveness conditions, then the controlled player must satify its liveness conditions. In terms of temporal operators, the canonical pattern for GR(1) is $$\bigwedge\square\Diamond \implies \bigwedge\square\Diamond$$ where the implication has a special interpretation to ensure causal controllers.

results

• First defined in [1]

references (chronological order)

1. Bridging the gap between fair simulation and trace inclusion (2005)
2. Synthesis of Reactive(1) designs (2012)