Reactive Synthesis

The formal specification defines the desired, infinite-horizon behavior of the system. It is written in a temporal logic like Linear Temporal Logic (LTL) or Signal Temporal Logic (STL). This logic expresses constraints over time, such as:

• Safety: "The robot must never enter the hazardous zone." (Globally not P)
• Liveness: "The robot must eventually reach the goal." (Eventually P)
• Fairness: "If the robot requests a resource infinitely often, it is granted infinitely often." The specification acts as the high-level requirements from which the controller is synthesized.

A formal model of the uncontrollable, dynamic world with which the synthesized controller must interact. It is typically represented as a finite-state transition system that defines:

• Environment Variables: Inputs the controller can observe but not dictate (e.g., sensor readings, user requests).
• Possible Transitions: How the environment state can change independently.
• Adversarial Assumptions: The synthesis algorithm often treats the environment as a hostile adversary that will behave within its modeled constraints to try and violate the specification. This guarantees robustness.

The output of synthesis is a finite-state controller or winning strategy. This is a deterministic program (often represented as a Mealy/Moore machine) that:

• Observes the current state of the environment.
• Decides the values of controllable system variables (e.g., actuator commands).
• Guarantees that for any admissible sequence of environment actions, the temporal logic specification is satisfied over the infinite execution. The controller is correct-by-construction.

The synthesis problem is framed as a turn-based, infinite-duration game between two players:

1. Environment (Opponent): Chooses values for uncontrollable input variables.
2. Controller (System): Responds by choosing values for controllable output variables. The game graph is constructed from the product of the environment model and the specification automaton. Synthesis solves this game to compute a winning strategy for the controller player, ensuring the specification is met against all possible environment moves.

The primary algorithmic method. The temporal logic specification is first compiled into an equivalent ω-automaton, most commonly a Büchi automaton or a Parity automaton, which accepts infinite sequences that satisfy the spec. The synthesis problem then reduces to solving a graph game on the product of this automaton and the environment model. The solution involves:

• Emptiness Checking and Solving Parity Games.
• Algorithms like recursive fixed-point computations (e.g., using μ-calculus).

Realizability is the decision problem: does a controller satisfying the specification exist for the given environment? If yes, the specification is realizable. Synthesis algorithms then construct that controller. Key algorithmic paradigms include:

• Symbolic Synthesis: Uses Binary Decision Diagrams (BDDs) or SAT/SMT solvers to represent and manipulate the huge state space symbolically.
• Bounded Synthesis: Searches for a controller up to a given size bound.
• GR(1) Synthesis: A highly efficient fragment of LTL (General Reactivity of Rank 1) used for robotics and hardware control.

Linear Temporal Logic (LTL) is a formal system used to specify the desired behavior of reactive systems over infinite sequences of states. It is the dominant specification language for reactive synthesis.

• Core Operators: Uses temporal operators like G (globally/always), F (eventually), X (next), and U (until) to express liveness and safety properties.
• Example Specification: G(request -> F(response)) means "it is always the case that a request eventually leads to a response."
• Role in Synthesis: The synthesis algorithm's goal is to construct a finite-state machine (controller) whose execution traces satisfy the given LTL formula.

A finite-state controller is the executable program output by a reactive synthesis algorithm. It is a finite-state machine (FSM) that dictates how a system should react to environmental inputs.

• Structure: Consists of a finite set of states, transitions between states (triggered by environment inputs), and outputs (system actions).
• Guarantee: The synthesized controller is correct-by-construction, meaning all possible infinite sequences of interactions with its environment are guaranteed to satisfy the temporal logic specification.
• Application: Used to implement protocol handlers, embedded system logic, and robot planners where formal correctness is critical.

A reactive system is a computational entity that maintains an ongoing interaction with its environment, responding to external inputs in real-time. This contrasts with transformational systems that compute a single output from a single input.

• Key Characteristics: Non-terminating, input-driven, and concurrent with its environment.
• Examples: Air traffic control software, network protocol implementations, autonomous vehicle perception-and-actuation loops, and user interface controllers.
• Synthesis Target: Reactive synthesis automates the creation of the core decision logic for such systems from a high-level temporal specification.

Church's Synthesis Problem, posed by Alonzo Church in 1957, is the foundational theoretical problem that reactive synthesis aims to solve. It asks: given a logical specification of a relation between input and output sequences, can a finite-state machine (a strategy) be constructed that realizes this relation?

• Formal Origin: Established the link between logic, automata theory, and controller design.
• Two-Player Game View: Often framed as a game between the Environment (controlling inputs) and the System (controlling outputs). Synthesis is the process of finding a winning strategy for the System.
• Modern Impact: The problem's solvability and complexity (2EXPTIME-complete for LTL) define the limits and research directions of automated synthesis.

A Büchi automaton is a type of finite automaton that accepts infinite words, making it essential for modeling and verifying properties of non-terminating reactive systems.

• Key Mechanism: Accepts an infinite input sequence if it visits an accepting state infinitely often.
• Synthesis Pipeline: In reactive synthesis, the LTL specification is first converted into an equivalent deterministic parity automaton (a generalization of a Büchi automaton). This automaton is then used to formulate a two-player game which, if won by the system player, yields a finite-state controller.
• Role: Serves as the bridge between logical specifications and game-theoretic algorithms for controller construction.

Assume-guarantee synthesis is an advanced form of reactive synthesis where the specification is divided into assumptions about the expected behavior of the environment and guarantees that the system must provide if those assumptions hold.

• Specification Format: Uses an implication, e.g., (Assumption) -> (Guarantee), often written in LTL.
• Practical Benefit: Allows for more realistic and robust controllers by explicitly modeling environmental constraints. The synthesized system is only required to work correctly in environments that satisfy the assumptions.
• Example: G(sensor_operational -> F(obstacle_avoided)) means "if the sensor is always operational, then eventually avoid obstacles."