eess.SYSep 19, 2026

A Geometric Decision Procedure for STL Feasibility and Repair

Authors: Avinash Malik

Organizations: Department of Electrical, Computer, and Software Engineering, University of Auckland, 20 Symonds Street, Auckland, 1042, New Zealand.

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

Abstract

Signal Temporal Logic control synthesis frequently encounters physical infeasibility due to actuator limits or flawed task deadlines. Standard optimization methods model time by discretizing the horizon, which leads to exponential computational growth and prevents the extraction of continuous temporal adjustments. This paper presents a geometric decision procedure that evaluates physical feasibility completely independently of the temporal horizon length. The method operates by transforming explicit temporal logic constraints into continuous spatial backward reachable sets evaluated at time zero. It analytically inverts the Bhat-Bernstein settling-time integral to map temporal windows into continuous spatial boundaries, reducing the feasibility check to a local matrix and vector inclusion evaluation. When a specification is infeasible, the procedure extracts a Farkas dual certificate to isolate conflicting constraints and identifies the maximum geometric spatial gap. It then analytically inverts the system's dynamic expansion to map this largest geometric gap into an exact, closed-form temporal delay, precisely fixing the boundary deficit to restore physical realizability. We formally prove the strict soundness, mathematically bounded completeness, and horizon-independent scalability of this procedure. Experimental evaluations on six-dimensional drone kinematics demonstrate sub-millisecond execution times, massive speedups over state-of-the-art optimization encodings, and computational immunity to deeply nested logical formulas.

Figures & tables

MetricMILP FrameworkProposed Geometric Method
Diagnostic OutputIIS / Spatial SlackFarkas Dual: [0.0, 0.0, 1.0]T[0.0,\,0.0,\,1.0]^{T}
Spatial Deficit / Slack4.17 m4.17 m
Repair ActionManual / State ShiftΔT∗=1.31\Delta T^{*}=1.31 s
Repaired Horizon TF′T_{F}^{\prime}N/A (Structural limit)4.31 s
Execution Time20.21 ms0.0351 ms
Table 1 . Diagnostic output from MILP vs Geometric Method
Figure 1 . Experimental evaluation results covering trajectory repair, horizon scalability, and syntactic complexity.
Figure 2 . Empirical verification of soundness and completeness across 10,00010{,}000 Monte Carlo runs with a uniform sampling distribution over the 6D initial state space.

Explore similar work

CardsList
Sep 8, 2026cs.LO

Fast Constraint Extraction for Corrective Control under STL Specifications via Logical Dependency Tracking

Ensuring the satisfaction of Signal Temporal Logic (STL) specifications under uncertainty is challenging, as reachability-based monitoring provides guarantees but does not indicate how to restore satisfaction when it becomes indeterminate. A key difficulty is identifying which uncertain components actually affect global satisfaction, especially for nested formulas. This paper introduces a logical dependency tracking framework that propagates uncertainty through the STL structure and captures the causal contribution of reachable sets to satisfaction. By associating markers to uncertain predicates and propagating them via three-valued semantics, we extract in milliseconds a compact Disjunctive Normal Form (DNF) of sufficient constraints, avoiding combinatorial enumeration. As an application, we formulate control correction as a minimum-effort optimization problem. Using zonotopic reachability, the derived constraints are enforced via linear programming, yielding corrections that guarantee STL satisfaction under bounded uncertainty and provide certified probabilistic bounds in the stochastic case. We demonstrate the approach on a nonlinear system with nested STL specifications, showing that dependency tracking enables efficient and formally guaranteed correction. The tracking implementation is available at https://github.com/Antoine-Bst/STL-Three-Valued-Clause-Filtering/.

Antoine Besset, Joris Tillet, Chuchu Fan +1

u2IS, ENSTA, Institut Polytechnique de Paris, France · Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG, France · REALM, AeroAstro, Massachusetts Institute of Technology, Cambridge, USA

Signal Temporal LogicReachabilityConstraint SatisfactionUncertain
AskPDF
Jul 21, 2026eess.SY

STL-GCS: A Planner-Controller Framework for Signal Temporal Logic via Graphs of Time-varying Convex Sets

We present a unified trajectory planning and control framework for the satisfaction of Signal Temporal Logic (STL) specifications defined over convex predicates. At the planning layer, STL tasks are encoded as time-varying convex sets in configuration space, specifically designed so that forward invariance of the system with respect to these sets implies satisfaction of the specification with a prescribed robustness margin. This representation is then lifted to the joint time--configuration space and combined with the Graphs of Convex Sets (GCS) framework, yielding a shortest-path formulation of the planning problem over convex spatio-temporal sets. Trajectories are parameterized by B-splines, which enable continuous-time enforcement of STL satisfaction, collision avoidance, and smoothness constraints. At the control layer, the same time-varying sets used for planning are exploited to design a feedback controller that tracks the planned trajectory while prioritizing satisfaction of the STL specification during execution in the presence of tracking errors and model mismatch. We validate the proposed approach in simulation and in real-world experiments on space robotic platforms.

Nicola De Carli, Gregorio Marchesini, Dimos V. Dimarogonas

Signal Temporal LogicConvex SetsSpatiotemporal
AskPDF
May 5, 2026cs.RO

Feasibility-aware Hybrid Control for Motion Planning under Signal Temporal Logics

In this work, a novel method for planar task and motion planning based on hybrid modeling is proposed. By virtue of a discrete variable which models local constraint satisfaction and enables local feasibility analysis, the proposed control architecture unifies planning with control design. Concurrently, control barrier functions are designed on a transformed disk version of the original nonconvex and geometrically complex robotic workspace, thus amending the issue of deadlocks. Simulations of the proposed method indicate effective handling of multiple overlapping spatio-temporal tasks even in the face of input saturation.

Panagiotis Rousseas, Dimos V. Dimarogonas

∗KTH Royal Institute of Technology, School of Electrical Engineering and Computer Science, Division of Decision and Control Systems

Motion PlanningControl Barrier FunctionsSignal Temporal Logic
AskPDF