# Modularized Control Synthesis for Complex Signal Temporal Logic Specifications

arXiv: https://arxiv.org/abs/2303.17086 · HTML: https://mlsanity.com/paper/2303.17086/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 30 Mar 2023.

## Built on by (most cited first, 4 of 4)

- [Signal Temporal Logic Neural Predictive Control](https://mlsanity.com/paper/2309.05131/) (2023)
- [Temporal Logic Specification-Conditioned Decision Transformer for Offline Safe Reinforcement Learning](https://mlsanity.com/paper/2402.17217/) (2024)
- [VernaCopter: Disambiguated Natural-Language-Driven Robot via Formal Specifications](https://mlsanity.com/paper/2409.09536/) (2024)
- [Traffic-Rule-Compliant Trajectory Repair via Satisfiability Modulo Theories and Reachability Analysis](https://mlsanity.com/paper/2412.15837/) (2024)

## Abstract (arXiv)

The control synthesis of a dynamic system subject to a signal temporal logic (STL) specification is commonly formulated as a mixed-integer linear/convex programming (MILP/MICP) problem. Solving such a problem is computationally expensive when the specification is long and complex. In this paper, we propose a framework to transform a long and complex specification into separate forms in time, to be more specific, the logical combination of a series of short and simple subformulas with non-overlapping timing intervals. In this way, one can easily modularize the synthesis of a long specification by solving its short subformulas, which improves the efficiency of the control problem. We first propose a syntactic timing separation form for a type of complex specifications based on a group of separation principles. Then, we further propose a complete specification split form with subformulas completely separated in time. Based on this, we develop a modularized synthesis algorithm that ensures the soundness of the solution to the original synthesis problem. The efficacy of the methods is validated with a robot monitoring case study in simulation. Our work is promising to promote the efficiency of control synthesis for systems with complicated specifications.