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

• URL: http://arxiv.org/abs/2606.30820v2
• Date: Sun, 05 Jul 2026 18:15:16 GMT
• Title: Robustness-Based Synthesis for Time Window Temporal Logic Specifications via Mixed-Integer Linear Programming
• Abstract summary: Time Window Temporal Logic (TWTL) is a rich specification language for cyber-physical systems.<n>We consider the problem of synthesizing control inputs for discrete-time linear systems subject to TWTL task specifications.
• Score: 2.3559161556025887
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Time Window Temporal Logic (TWTL) is a rich specification language for cyber-physical systems that can compactly express sequential tasks with explicit timing constraints. In this paper, we consider the problem of synthesizing control inputs for discrete-time linear systems subject to TWTL task specifications. Building on the quantitative semantics (robustness) recently introduced for TWTL in [1], we encode the robust satisfaction of a TWTL formula as a set of Mixed-Integer Linear constraints and pose synthesis as a Mixed Integer Linear Program (MILP) that maximizes the robustness degree. We prove that any feasible solution with positive objective value guarantees Boolean satisfaction of the specification. We address two synthesis settings: an \emph{open-loop} formulation that optimizes the full control sequence from the initial state, and a \emph{closed-loop} receding-horizon Model Predictive Controller (MPC) formulation that re-solves the MILP at each step using the current measured state. A key feature of our MPC formulation is a \emph{task-adaptive horizon} that exploits the TWTL Deterministic Finite Automaton (DFA) to determine the active sub-task at each step, limiting the prediction horizon to the remaining window of the current task rather than the full formula horizon, this makes each re-solve significantly cheaper than the initial open-loop solve.

Related papers

• Constrained Decoding for Diffusion Language Models via Efficient Inference over Finite Automata [57.27430779838529]
  We present an exact and tractable algorithm for sampling from the constrained mean-field posterior under any constraint expressible as a finite automaton.<n>The approach guarantees constraint satisfaction by construction, supports both greedy and sampling-based decoding, and is compatible with parallel and block-wise decoding.<n> Empirical evaluations on Dream-7B and LLaDA-8 show substantial accuracy gains across various tasks.
  arXiv  Detail & Related papers  (2026-07-08T05:48:57Z)
• Signal Temporal Logic Motion Planning via Graphs of Convex Sets [8.443328067924298]
  This paper investigates continuous-time motion planning under Signal Temporal Logic (STL) specifications.<n>We propose a framework that combines timed-automata reasoning with graphs of convex sets.<n> Numerical experiments on low-dimensional benchmarks, a $3$-Drotor, a $30$-DoF humanoid, and a hardware experiment on a UR-3 robot arm demonstrate that the proposed method efficiently solves complex STL motion-planning problems.
  arXiv  Detail & Related papers  (2026-05-22T05:19:43Z)
• SGA-MCTS: Decoupling Planning from Execution via Training-Free Atomic Experience Retrieval [74.1918709002557]
  We introduce textbfSGA-MCTS, a framework that casts LLM planning as non-parametric retrieval.<n>Online, a retrieval-augmented agent employs a hybrid symbolic-semantic mechanism to fetch relevant State-Goal-Action atoms.<n>By effectively amortizing the heavy computational cost of search, SGA-MCTS achieves System 2 reasoning depth at System 1 inference speeds, rendering autonomous planning both scalable and real-time feasible.
  arXiv  Detail & Related papers  (2026-04-16T07:22:36Z)
• MAny: Merge Anything for Multimodal Continual Instruction Tuning [52.50936513604062]
  textbfMAny (textbfMAny) is a framework that merges task-specific knowledge through textbfCross-modal textbfProjection textbfMerging.<n>textbfLow-rank textbfParameter textbfMerging (textbfLPM)
  arXiv  Detail & Related papers  (2026-04-15T15:57:23Z)
• RRT$^η$: Sampling-based Motion Planning and Control from STL Specifications using Arithmetic-Geometric Mean Robustness [7.121834057343983]
  We propose RRT$$, a sampling-based planning framework that integrates robustness measures across time points and subformulae.<n>We demonstrate superior performance over traditional STL robustness-based planners in multi-constraint scenarios with limited guidance signals.
  arXiv  Detail & Related papers  (2026-02-18T19:45:43Z)
• QTIS: A QAOA-Based Quantum Time Interval Scheduler [0.22940141855172033]
  The proposed method integrates an ancilla-assisted quantum circuit to dynamically detect and penalize overlapping tasks.<n>Results confirm the efficiency of QTIS in scheduling tasks with fixed temporal windows while minimizing conflicts.
  arXiv  Detail & Related papers  (2025-11-19T16:29:14Z)
• Dependency-Aware Task Offloading in Multi-UAV Assisted Collaborative Mobile Edge Computing [53.88774113545582]
  This paper presents a novel multi-unmanned aerial vehicle (UAV) assisted collaborative mobile edge computing (MEC) framework.<n>It aims to minimize the system cost, and thus realize an improved trade-off between task consumption and energy consumption.<n>We show that the proposed scheme can significantly reduce the system cost, and thus realize an improved trade-off between task consumption and energy consumption.
  arXiv  Detail & Related papers  (2025-10-23T02:55:40Z)
• Unlocking Symbol-Level Precoding Efficiency Through Tensor Equivariant Neural Network [84.22115118596741]
  We propose an end-to-end deep learning (DL) framework with low inference complexity for symbol-level precoding.<n>We show that the proposed framework captures substantial performance gains of optimal SLP, while achieving an approximately 80-times speedup over conventional methods.
  arXiv  Detail & Related papers  (2025-10-02T15:15:50Z)
• Stochastic Approximation with Delayed Updates: Finite-Time Rates under Markovian Sampling [73.5602474095954]
  We study the non-asymptotic performance of approximation schemes with delayed updates under Markovian sampling. Our theoretical findings shed light on the finite-time effects of delays for a broad class of algorithms.
  arXiv  Detail & Related papers  (2024-02-19T03:08:02Z)
• Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic [4.60607942851373]
  We consider the problem of automatically synthesizing formal specifications from system executions. Most of the classical approaches for synthesizing temporal logic formulas aim at minimizing the size of the formula. We formalize this notion and devise a learning algorithm that synthesizes concise formulas having bounded lookahead.
  arXiv  Detail & Related papers  (2023-10-26T14:13:15Z)
• Combining Deep Learning and Optimization for Security-Constrained Optimal Power Flow [94.24763814458686]
  Security-constrained optimal power flow (SCOPF) is fundamental in power systems. Modeling of APR within the SCOPF problem results in complex large-scale mixed-integer programs. This paper proposes a novel approach that combines deep learning and robust optimization techniques.
  arXiv  Detail & Related papers  (2020-07-14T12:38:21Z)
• Stochastic Finite State Control of POMDPs with LTL Specifications [14.163899014007647]
  Partially observable Markov decision processes (POMDPs) provide a modeling framework for autonomous decision making under uncertainty. This paper considers the quantitative problem of synthesizing sub-optimal finite state controllers (sFSCs) for POMDPs. We propose a bounded policy algorithm, leading to a controlled growth in sFSC size and an any time algorithm, where the performance of the controller improves with successive iterations.
  arXiv  Detail & Related papers  (2020-01-21T18:10:47Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.