Reactive Synthesis
Definition
Reactive synthesis is the automatic construction of a strategy or controller that satisfies a temporal specification while interacting indefinitely with an environment.
Why It Matters
It is the offline, specification-first cousin of shielding and runtime enforcement. Instead of checking or correcting a finished controller, synthesis asks whether a correct controller exists and constructs one when possible.
Formalism / Key Objects
- Variables are partitioned into uncontrollable environment inputs
Xand controllable system outputsY. - A strategy is a history-dependent function
- A temporal specification
phiis realizable when there exists such a strategy so that every environment input sequence yields a trace satisfyingphi. - General LTL synthesis is commonly reduced to automata and infinite-duration games, with 2EXPTIME-complete worst-case complexity.
- Restricted fragments such as Safety LTL, GR(1), or Safety-and-Emerson-Lei can expose more symbolic or specialized algorithms.
- Safety LTL Automata and Games and Emerson-Lei Game Solving store the reusable automata/game-solving details for the current safety/co-safety synthesis cluster.
Connections
- Linear Temporal Logic is the standard trace language for many reactive-synthesis problems.
- Safety Games solve the safety-only case by computing a controller winning region.
- Emerson-Lei Objectives support richer liveness conditions while retaining symbolic game-solving structure.
- Shield Synthesis synthesizes a runtime correction layer rather than a full controller from scratch.
- Invariant Synthesis searches for reusable formulas that certify or guide strategies.
Common Confusions
- Realizability asks whether a controller exists against all environment moves; satisfiability only asks whether some trace satisfies the formula.
- Reactive synthesis assumes a boundary between controllable and uncontrollable variables.
- Safety synthesis is not the same as full LTL synthesis; liveness conditions usually require richer game objectives.