A research arc on Signal Temporal Logic — from a tractable optimization engine, to its first real industrial deployment, to a layered architecture that keeps it sound.
The Arc — Three Questions
Signal Temporal Logic (STL) is expressive enough to describe what a control system should do, in language close to how engineers actually speak. The open question has never been expressiveness — it has been whether that expressiveness survives contact with the real world: real-time computation, real industrial rules, and real continuous-time hardware.
These three works answer that question in sequence. Each one removes the obstacle the previous one exposed.
From tractable logic, to a real deployment, to a trustworthy architecture.
The arc. Each work removes the obstacle the previous one exposed — an efficient engine, then a real deployment, then a sound architecture around it.
STL is expressive, but its native mixed-integer encoding does not scale to long horizons. STLCCP recasts the synthesis problem by exploiting three structural properties of STL — monotonicity of the robustness function, its hierarchical tree structure, and the correspondence between conjunction/disjunction and convexity/concavity. The result is a difference-of-convex program solved as a sequence of convex quadratic programs, augmented by a tree-weighted penalty CCP and a tailored mellowmin smoothing. STL becomes a computationally viable engine for control over long horizons.
Structure-aware decomposition. The robustness tree maps conjunction to convex and disjunction to concave terms, yielding a difference-of-convex program solved as sequential QPs.
The first real-world, large-scale implementation of complex STL. Natural-language operating rules of the French sub-transmission grid — battery cycling, multi-level overload tolerance, flow-limit changes — are formalized as recurring, infinite-horizon specifications, then transformed step-by-step into finite-horizon receding-horizon problems that stay robust to disturbances and actuator delays via memory constraints and constraint tightening. Crucially the scheme is runtime verifiable: each subformula's robustness value is a live certificate that pinpoints which requirement is violated, and by how much.
Infinite to finite, with a live certificate. Recurring NL rules become a finite-horizon RHC problem carrying past memory; the per-subformula robustness ρφ reports satisfaction at every step.
But a single discrete-time optimizer cannot, by itself, guarantee what happens between samples on real hardware — so the architecture itself has to be made sound.
arXiv:2605.04222 [eess.SY] · submitted to Automatica · 2026
A discrete-time STL/MPC planner alone cannot guarantee continuous-time safety in genuinely complex systems. This work formalizes the interaction between the high-level optimization layer and the low-level continuous controller as a heterogeneous assume-guarantee contract, importing the safety–liveness decomposition from computer science: safety is enforced by invariance at the continuous-time layer, liveness through refinement at the discrete-time layer, with the two coordinated by vertical refinement and timing-compatibility conditions and realized by an explicit reference governor. Validated on a battery–supercapacitor hybrid energy storage system.
Two layers, one contract. A reference governor bridges discrete planning and continuous execution; the ZOH makes the coupling sequential, so safety (invariance) and liveness (refinement) are certified independently, then composed.