Modularized Control Synthesis for Complex Signal Temporal Logic Specifications

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.