A Geometric Decision Procedure for STL Feasibility and Repair

arXiv:2610.00199 · eess.SY, cs.RO, cs.SY · Submitted 2026-09-19 · Read on arXiv

Listen

Radio episode about this paper

Transcript

Introduction to the show: ident: Robotics Radio. Generated commentary on the latest robotics and control papers.

Rosa: Today's paper: "The Geometry of Time".

Dev: Signal Temporal Logic (STL) control synthesis frequently encounters physical infeasibility due to actuator limits or flawed task deadlines,

Rosa: First, who's behind it and why it matters.

Title and authors: Rosa: So we're looking at "The Geometry of Time: Horizon-Independent Feasibility and Repair for STL." It sounds like they're tackling a really tricky problem where standard methods get bogged down by how far into the future you look.

Dev: Yeah, that title suggests they found a way to check if a control task is possible without having to discretize the entire temporal horizon, which usually blows up the computation.

Taro: I'm curious how this approach handles situations where the system itself might misbehave or encounter unexpected events during execution.

Rosa: Exactly, Taro, because when we think about real-world deployment on a physical robot, we always have to wonder if these theoretical checks hold up outside of the clean simulation environment they likely used.

Dev: I worry about the loop rate here; if this check is too slow or introduces too much latency into a real-time system, it defeats the purpose of making it practical for control loops.

Taro: That's a fair point, Dev, because if the robot is supposed to react to something unexpected, we need assurance that this feasibility test doesn't just give us a false sense of security in the messy real world.

Rosa: Well, the core idea seems to be translating those explicit temporal logic constraints into a continuous spatial problem evaluated right at time zero, which sounds much more efficient than traditional methods.

Dev: That mapping process is key; if they can map temporal windows directly onto spatial boundaries, that bypasses the exponential complexity of discretizing time steps.

Taro: And I'm interested in the mechanism they use to handle those conflicting constraints when a specification turns out to be physically impossible to meet.

Rosa: That's where their methodology gets interesting; they seem to use a Farkas dual certificate when infeasibility is detected, which helps isolate exactly which constraints are causing the problem.

Dev: Isolating the conflict is smart, but then what happens after they find that gap? Do they just stop there, or do they offer a way to fix it?

Taro: If the specification fails because of actuator limits or deadlines conflicting with system dynamics, I'd want a clear path to recovery so we can adjust the plan rather than just knowing it's impossible.

The paper's summary: Rosa: So, summarizing what we know about "The Geometry of Time: Horizon-Independent Feasibility and Repair for STL," they are proposing a geometric decision procedure that checks physical feasibility without depending on the length of the temporal horizon.

Dev: They do this by taking those explicit temporal logic constraints and transforming them into continuous spatial backward reachable sets that are all evaluated at time zero, which sounds like a massive simplification from standard optimization techniques.

Taro: That transformation involves inverting the Bhat–Bernstein settling-time integral to map those temporal windows into continuous spatial boundaries, effectively turning time limits into geometric shapes.

Rosa: And when the system finds that a specification is infeasible, they don't just report a failure; instead, they extract a Farkas dual certificate to pinpoint the conflicting constraints and identify the largest geometric spatial gap.

Dev: That gap is important because it seems like a precise measurement of how much the current constraints are missing from being physically realizable, which is useful for diagnosing the failure mode.

Taro: They then take that maximal geometric spatial gap and analytically invert the system’s dynamic expansion to map it into an exact, closed-form temporal delay that can be applied to fix the boundary deficit.

Rosa: That final repair value provides a direct temporal adjustment, like increasing the horizon by a specific amount, which allows a planner or author to directly broaden deadlines for physical realizability.

Dev: It sounds like they've moved from just detecting failure to actually prescribing how to make it work by giving an exact delay correction instead of vague relaxation.

The paper's improvements: Rosa: The main improvement they highlight is the independence from temporal discretization; this means the feasibility check only needs a single matrix-vector inequality evaluation, which is Ax(zero) beff, and it doesn't care about the temporal horizon length at all.

Dev: That's huge for us because it means we don't have to worry about exponential computational growth as we try to model longer time horizons in discrete steps; it keeps the complexity low, around O(nd).

Taro: The claim that this procedure is independent of formula nesting depth is also something I find compelling, especially since modern planning often involves deeply nested temporal requirements from complex natural language inputs.

Rosa: Yes, they show that their geometric semantics are composed inductively using compositional translation rules that map logical operators to higher-order functionals, which handles those complex nested structures efficiently.

Dev: And the fact that the optional diagnostic spatial witness generation only takes O(LP) time to extract the dual vector y is a big deal for any real-time system we're designing.

Taro: So, instead of having to run heavy optimization solvers repeatedly, we can get a quick verification in constant time regarding the core feasibility check, which is much better for fast decision loops.

Rosa: And finally, they offer a closed-form temporal repair value T* that is computable in a constant number of arithmetic operations independent of the temporal horizon T eff.

Dev: That’s what I was hoping for; getting an exact, closed-form delay correction instead of just relying on numerical slack variables means we get mathematically rigorous results for fixing the problem.

Conclusion: Rosa: To wrap up our discussion on "The Geometry of Time: Horizon-Independent Feasibility and Repair for STL," the main implication is that we have a method that can check synthesis feasibility completely independently of how long the time horizon is or how complicated the logic gets.

Dev: This geometric decision procedure gives us a way to get an exact temporal repair value T* when things are infeasible, which lets us directly adjust deadlines for physical systems based on what they actually need.

Taro: For autonomy, this means we can rapidly diagnose conflicting constraints and get a precise measure of the spatial gap to understand exactly where our planning failed in a complex scenario.

Rosa: It feels like we've gained a powerful tool for pre-computation screening before running more expensive solvers, which should speed up the overall development cycle significantly.

Dev: I think this capability to provide that exact repair mechanism is what moves us closer to deploying robust, real-time controllers where we can guarantee physical realizability under tight constraints.

Taro: The ability to get a closed-form temporal delay for recovery makes debugging specification errors much more precise and less reliant on iterative tuning.

Rosa: This paper's focus on making feasibility checks horizon-independent is a really significant step toward building more scalable formal methods for complex control synthesis.

Department of Electrical, Computer, and Software Engineering, University of Auckland

eess.SY, cs.RO, cs.SY

Submitted: 2026-09-19

Updated: 2026-10-06

Comments: 11 pages, 2 figures

License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/

Importance score: 93/100

The gist: Signal Temporal Logic (STL) control synthesis frequently encounters physical infeasibility due to actuator limits or flawed task deadlines, and this paper presents a geometric decision procedure that

Key concepts

Geometric Semantics
This concept maps complex STL logic formulas into a continuous spatial field called a level-set function. This function translates logical requirements like 'eventually' or 'until' into geometric shapes in space, making the feasibility check purely about whether a starting point falls within the valid region of this shape.
Level-Set Inversion
The method uses an analytical inversion technique to map temporal windows (like time intervals) into continuous spatial boundaries. This allows the complex temporal constraints to be represented as simple spatial inequalities, simplifying the overall feasibility problem significantly.
Farkas Dual Certificate
When a specification is found to be infeasible, this certificate is extracted. It isolates exactly which constraints are conflicting and identifies the largest geometric gap between them. This pinpointing helps determine the precise deficit that needs to be corrected.
Temporal Repair Value ($ΔT^*$)
This value represents the exact temporal delay needed to restore physical realizability. It is calculated by mapping the identified spatial gap directly into a time delay using system dynamics inversion, providing a concrete, actionable fix for designers.

Terminology

Summary

Signal Temporal Logic (STL) control synthesis frequently encounters physical infeasibility due to actuator limits or flawed task deadlines, and this paper presents a geometric decision procedure that evaluates physical feasibility completely independently of the temporal horizon length.

How it works

The method operates by transforming explicit temporal logic constraints into continuous spatial backward reachable sets evaluated at time zero. This transformation is achieved by analytically inverting the Bhat–Bernstein settling-time integral to map temporal windows into continuous spatial boundaries, which reduces 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.

Geometric Semantics and Level-Set Inversion

The core of the approach involves defining a differentiable spatial level-set function, denoted as JψK: R d → R, that maps an arbitrary Signal Temporal Logic (STL) formula ψ into a continuous spatial field. The valid continuous initial state set Xfeasible is then defined by the non-negative zero-superlevel set: Xfeasible ≜ x(0) ∈ R d, JψK(x(0)) ≥ 0. This geometric semantics is composed inductively using compositional translation rules (Equation 10) that map logical operators to higher-order functionals. Specifically, temporal operators F[a,b] and G[a,b] are mapped into the Bhat–Bernstein drift bound equations (Equations 11 and 14), which define geometric capture basins (Sb−a(f)) for liveness and contracted safety buffers (Bb−a(f)) for safety.

Polyhedral Compilation and Local Evaluation

The recursive map evaluated at the initial state, JψK(x(0)) ≥ 0, is formally compiled into a local polyhedral system Ax(0) ≤ beff. This compilation is achieved by evaluating the spatial gradients of the continuous geometric semantics JψK at the nominal operating point x∗ = x(0), which yields a first-order Taylor expansion (Equation 18). The resulting matrix A and vector beff are constructed by stacking transformed gradient vectors row-wise, where temporal inversions analytically modify the scalar boundary hi into an effective temporal bound beff,i(a, b). This process ensures that the check is algebraically equivalent to evaluating the continuous geometric semantics at time zero.

Witness Generation and Temporal Repair

When a specification is infeasible, the procedure extracts a Farkas dual certificate to isolate conflicting constraints and identifies the maximum geometric spatial gap (r). This scalar spatial deficit r is then analytically mapped into an exact, closed-form temporal delay ∆T∗ using the inverted Bhat–Bernstein integral (Equation 7): ∆T∗ = r / vmax. This repair value provides an exact scalar delay that a task planner or specification author can apply directly to broaden temporal deadlines, such as increasing the horizon T F by +∆T∗.

Complexity and Scalability Guarantees

The primary structural advantage is the independence from temporal discretization. The feasibility check reduces strictly to a single matrix-vector inequality evaluation Ax(0) ≤ beff, which requires O(nd) arithmetic operations and is independent of the temporal horizon Teff (Lemma 3). Furthermore, the optional diagnostic spatial witness generation requires O(LP) time to extract the dual vector y, and the closed-form temporal repair is computable in a constant number of arithmetic operations independent of Teff (Lemma 5). This establishes that the procedure is horizon-independent and provides massive speedups over state-of-the-art optimization encodings.

Summary of Key Findings

  1. The geometric decision procedure evaluates synthesis feasibility completely independently of the temporal horizon length and formula nesting depth.

  2. When infeasible, it returns a Farkas dual certificate identifying the minimal conflicting subset and a closed-form temporal repair value ∆T∗ that restores physical realizability.

  3. 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.

  4. The procedure is strictly sound (Theorem 2) and complete within a quantifiable geometric margin ε (Theorem 3), meaning false negatives are only possible if the true optimal trajectory falls within the narrow temporal boundary margin of thickness ε.

  5. The complexity is O(nd) for verification, independent of Teff, confirming its tractability for long-horizon specifications.

  6. The repair mechanism provides a definitive temporal fix rather than settling for spatial relaxation by translating the spatial deficit directly into an exact closed-form temporal delay using the fractional dynamics inversion.

Improvements for AI systems

Here are the specific improvements that can be made to AI systems based on the scientific paper, along with what those improved systems can achieve:

The proposed geometric decision procedure offers several transformative capabilities for AI systems, particularly in areas requiring formal verification, temporal reasoning, and real-time control synthesis.

  1. The core improvement is the replacement of computationally expensive Mixed-Integer Linear Program (MILP) based feasibility checks with a rapid, horizon-independent geometric check that operates via a single matrix-vector inequality evaluation at time zero.

  2. The system gains the ability to provide exact, closed-form temporal repairs to infeasible specifications, rather than just suggesting impossible state shifts or relying on numerical optimization slack variables.

  3. The AI can be deployed for offline pre-computation screening of complex control/task planning problems before executing expensive solvers (like MILP), dramatically reducing computational time and enabling real-time deployment.

  4. The system achieves scalability that is independent of the temporal horizon length or the depth of nested logical formulas, neutralizing the exponential blowup traditionally associated with discrete time modeling in STL synthesis.

Specific Capabilities of the Improved AI System:

  1. A robot or autonomous agent can generate and verify complex, nested temporal specifications (e.g., Reach Goal X within 2 seconds, then stay there for at least 8 seconds) without the verification process slowing down exponentially as the time horizon or formula complexity increases.

  2. The AI can receive a specification that is physically infeasible (e.g., requesting travel faster than actuator limits), and instead of failing silently or suggesting an impossible fix, it will output an exact, mathematically derived temporal delay (e.g., Increase the deadline by exactly 1.50 seconds) to restore feasibility.

  3. The AI can perform high-speed diagnostics on control policies or task plans by identifying the minimal conflicting constraint and quantifying the precise spatial violation (the spatial gap), which is essential for debugging LLM-generated specifications or flawed planning outputs in robotics and autonomous systems.

  4. The system can act as a lightweight, real-time safety gate within Receding Horizon Control (RHC) loops, executing the feasibility check in sub-millisecond time (< 0.1 ms), allowing for immediate decision-making under strict hardware constraints (e.g., on embedded systems or drones).

  5. The system can provide mathematically rigorous guarantees of correctness (Soundness and Bounded Completeness), meaning that any feasible result it returns is provably achievable by an admissible control input, eliminating the uncertainty inherent in numerical optimization relaxations.

Sources

Related papers