Robustness-Based Synthesis for Time Window Temporal Logic Specifications via Mixed-Integer Linear Programming

Technical Summary: Robustness-Based Synthesis for Time Window Temporal Logic Specifications via Mixed-Integer Linear Programming

Problem Statement
The paper addresses the control synthesis problem for discrete-time linear systems subject to Time Window Temporal Logic (TWTL) specifications. TWTL is a specification language designed for cyber-physical systems that compactly expresses sequential tasks with explicit timing constraints (e.g., "dwell in region A for 4 units, then visit region B within 10 units"). While previous work established TWTL for monitoring and sampling-based planning, a deterministic synthesis procedure that optimizes for robustness—a quantitative measure of how well a trajectory satisfies a specification—was missing. The authors aim to synthesize control inputs that not only satisfy the Boolean TWTL formula but also maximize the margin of satisfaction (robustness), thereby increasing resilience to disturbances and noise.

Methodology
The proposed methodology encodes the quantitative semantics (robustness) of TWTL into a Mixed-Integer Linear Program (MILP).

1. Robustness Encoding: Building on the quantitative semantics introduced in prior work [1], the authors define a robustness value $\rho$ for TWTL formulas. They translate the recursive definition of $\rho$ (involving min/max operations over time windows) into a set of linear constraints using "Big-M" formulations and binary variables.

   • Operators: The encoding handles TWTL-specific operators: Hold ($H_d$), Within ($[\cdot]_{[a,b]}$), and Concatenation ($\cdot$).
   • Binary Variables: Logical operations (disjunction, within, concatenation) are encoded using binary variables. The authors note that the number of binary variables is a critical performance metric.

2. Synthesis Formulations: Two synthesis problems are formulated:

   • Open-Loop: A single optimization from the initial state $x_0$ to find a control sequence $u^*$ that maximizes $\rho$.
   • Closed-Loop (MPC): A Model Predictive Control framework that re-solves the MILP at each time step $t$ using the current measured state $x_t$ and the current state of the TWTL Deterministic Finite Automaton (DFA).

3. Task-Adaptive Horizon & Warm-Start: A key innovation in the MPC formulation is the task-adaptive horizon.

   • Instead of using the full formula horizon $T$ (which can be large) for every re-solve, the horizon $H_t$ is dynamically limited to the remaining time window of the current active sub-task identified by the DFA state.
   • The authors utilize a warm-start strategy. Since the MILP constraint matrices depend on the DFA state (which is finite and independent of time bounds) rather than the specific state values, they precompute matrices for each DFA state offline. Online, they only update the right-hand side (state values) and bounds, significantly reducing computational overhead.

Key Contributions
The paper makes four primary contributions:

1. MILP Encoding: It provides the first recursive Big-M MILP encoding for TWTL robustness, proving that any feasible solution with a positive objective value guarantees Boolean satisfaction of the specification (Theorem 4.1).
2. Synthesis Frameworks: It formulates both an open-loop controller and a closed-loop MPC controller. The MPC formulation introduces a task-adaptive horizon that exploits the TWTL DFA structure to bound the prediction horizon by the remaining window of the current task ($\max b_i$) rather than the total formula horizon $T$.
3. Efficiency Strategy: It proposes a warm-start strategy that reduces the per-step online cost of MPC to linear in the system state dimension ($O(n)$) for updates, plus the cost of re-solving a progressively smaller MILP.
4. Comparative Efficiency: It demonstrates that direct TWTL encoding is more efficient than translating TWTL to Signal Temporal Logic (STL) for MILP synthesis, particularly as the number of sequential sub-tasks increases.

Results
The authors validate their approach through numerical experiments on a 2D double-integrator system navigating a workspace with obstacles and sequential region visits.

• Robustness Relevance: Comparisons show that paths optimized for robustness are qualitatively and quantitatively more resilient to disturbances than those satisfying only Boolean constraints.
• Open-Loop vs. Closed-Loop: In the presence of disturbances, the open-loop controller fails to complete the task, whereas the closed-loop MPC successfully adapts and replans.
• Performance Comparison:
  • TWTL vs. STL: For specifications with four or more sub-tasks, direct TWTL encoding outperforms STL translation in solve time due to a reduction in binary variables.
  • Horizon Strategies: The proposed "Task-Adaptive" (DFA-based) horizon strategy significantly reduces the total solve time over a run compared to a fixed-horizon approach (analogous to prior STL MPC work), with the performance gap widening as the number of sequential goals increases.

Significance and Claims
The paper claims to provide the first robustness-maximizing MILP synthesis procedure for TWTL. Its significance lies in bridging the gap between high-level temporal logic specifications and robust, real-time control execution.

• Deterministic Guarantees: Unlike sampling-based planners that offer probabilistic completeness, this approach offers deterministic guarantees on robustness maximization.
• Scalability: By exploiting the TWTL DFA structure, the method avoids the computational explosion associated with large time horizons in traditional MPC formulations, making it suitable for complex sequential tasks.
• Practicality: The warm-start strategy and task-adaptive horizon make the approach computationally tractable for online implementation, addressing the "curse of dimensionality" often associated with MILP-based temporal logic control.

The authors conclude that while the current work focuses on the min-max robustness measure, future work will explore extending this to Arithmetic Geometric Mean (AGM) robustness and utilizing formula rewriting to further reduce binary variable counts.