Modularized Control Synthesis for Complex Signal Temporal Logic Specifications

Specifications in Signal Temporal Logic (STL) can quantify requirements on real-valued signals. In this paper, we are concerned with discrete-time signals $\mathbf{x}_{[\,0,\,L\,]}\!:=\!x_{0}x_{1}\cdots x_{L}$, where $L\!\in\!\mathbb{N}^{+}$ denotes the length of the signal and $x_{k}\!\in\!\mathbb{R}^{n}$ is the value of the signal at time $k\!\in\!\{0,1,\cdots,L\}$. With $\mathbf{x}_{[\,k_{1},k_{2}\,]}:=x_{k_{1}}x_{k_{1}+1}\ldots x_{k_{2}}$, we denote a segment of $\mathbf{x}$ or equivalently $\mathbf{x}_{[\,0,\,L\,]}$ with timing points $0\!\leq\!k_{1}\!\leq\!k_{2}\!\leq\!L$. The syntax of STL is recursively defined as

where $\varphi_{1},\varphi_{2}$ are STL formulas, $\lnot$, $\wedge$ are operators negation and conjunction, $\mu$ is a predicate that evaluates a predicate function $\eta:\mathbb{R}^{n}\rightarrow\{\,\top,\,\bot\,\}$ by $\displaystyle\mu=\left\{\begin{array}[]{ll}\top&\mathrm{if}~{}\eta(x_{k})\geq 0\\ \bot&\mathrm{if}~{}\eta(x_{k})<0\end{array}\right.$, for discrete time $k$, and $\mathsf{U}_{[\,a,\,b\,]}$ is the until operator bounded with time interval $[\,a,\,b\,]$, where $a,b\in\mathbb{N}$ and $a\leq b$.

The semantics of STL are given as follows. We denote the satisfaction of $\varphi$ at time $k$ by $\mathbf{x}$ as $(\mathbf{x},k)\vDash\varphi$. Furthermore, we have that $(\mathbf{x},k)\vDash\mu\leftrightarrow\eta(x_{k})\geq 0$; $(\mathbf{x},k)\vDash\lnot\varphi\leftrightarrow\lnot((\mathbf{x},k)\vDash\varphi)$; $(\mathbf{x},k)\vDash\varphi_{1}\wedge\varphi_{2}\leftrightarrow(\mathbf{x},k)\vDash\varphi_{1}$ and $(\mathbf{x},k)\vDash\phi_{2}$; $(\mathbf{x},k)\vDash\varphi_{1}\mathsf{U}_{[\,a,\,b\,]}\varphi_{2}$ $\leftrightarrow$ $\exists\,k^{\prime}\in[\,k+a,\,k+b\,]$, such that $(x,k^{\prime})\vDash\varphi_{2}$, and $(x,k^{\prime\prime})\vDash\varphi_{1}$ holds for all $k^{\prime\prime}\in[\,k,\,k^{\prime}\,]$. Besides, additional operators disjunction, eventually, and always are, respectively, defined as $\varphi_{1}\vee\varphi_{2}=\lnot\left(\lnot\varphi_{1}\wedge\lnot\varphi_{2}\right)$, $\mathsf{F}_{[\,a,\,b\,]}\varphi=\top\mathsf{U}_{[\,a,\,b\,]}\varphi$, and $\mathsf{G}_{[\,a,\,b\,]}\varphi=\lnot\mathsf{F}_{[\,a,\,b\,]}\lnot\varphi$. When $k\!=\!0$, we also write $(\mathbf{x},0)\vDash\varphi$ as $\mathbf{x}\vDash\varphi$. The length [17] of an STL, $\mathcal{L}(\varphi)$, is recursively defined as $\mathcal{L}(\mu)=0$, $\mathcal{L}(\lnot\varphi)=\mathcal{L}(\varphi)$, $\mathcal{L}(\varphi_{1}\wedge\varphi_{2})=\max\{\mathcal{L}(\varphi_{1}),\mathcal{L}(\varphi_{2})\}$, $\mathcal{L}(\varphi_{1}\mathsf{U}_{[\,a,\,b\,]}\varphi_{2})=b+\max\{\mathcal{L}(\varphi_{1}),\mathcal{L}(\varphi_{2})\}$, which represents the maximum time it takes to determine the truth of the formula $\varphi$.

STL formulas are used to specify the requirements of a signal of a dynamic system. In this paper, we consider the following discrete-time dynamic system,

where $x_{k}\in\mathbb{R}^{n}$ and $u_{k}\in\mathbb{U}$ are the state and the control input of the system at time $k$, where $\mathbb{U}\subseteq\mathbb{R}^{m}$ is the admissible control set, and $f:\mathbb{R}^{n}\times\mathbb{U}\rightarrow\mathbb{R}^{n}$ is a smooth vector field. Then, the control problem of the system can be formulated as the following optimization problem,

where $L\!\in\!\mathbb{N}^{+}$ is the control horizon, $\mathbf{u}\!=\!u_{0}u_{1}$ $\cdots$ $u_{L-1}$ and $\mathbf{x}\!=\!x_{0}x_{1}\cdots x_{L}$ are the open-loop control and state signals, $\varphi$ is an STL formula with $\mathcal{L}(\varphi)\!=\!L$ to specify the requirements on the state signal $\mathbf{x}$, and $\rho(\mathbf{x},\varphi)$ is the robustness of the satisfaction as defined in [18, 19], with $\varrho(\mathbf{x},\varphi)\!>\!0\!\leftrightarrow\!\mathbf{x}\!\vDash\!\varphi$. Eq. (3) renders an open-loop control problem and can be solved using MICP [7] with an input interface $(x_{0},\,L,\,\varphi)$.

Solving problem (3) using MICP usually introduces heavy computational load due to the large number of integer variables brought up by the logical and temporal operators in the specification $\varphi$ [7]. Usually, longer formulas introduce substantially more integer variables than shorter ones. In the worst case, a specification $\varphi$ may contain $N\in\mathbb{N}^{+}$ $\mathsf{G}$ or $\mathsf{F}$ subformulas with the same length $L\!=\!\mathcal{L}(\varphi)$. This requires $NL$ binary variables to determine the logical satisfaction of the complete specification, which leads to an exponential complexity $O(2^{NL})$. Therefore, the computational complexity of the synthesis problem is greatly dependent on the number and the lengths of subformulas.

In this paper, we intend to reduce the complexity of a synthesis problem (3) by separating a long specification $\varphi$ into shorter subformulas which can be solved by smaller optimization problems. Examples of such separation include the following principle for an until operator $\varphi\!=\!\varphi_{1}\mathsf{U}_{(\,a,\,b\,)}\varphi_{2}$ with a separating point $\kappa\!\in\!\mathbb{N}^{+}$, $a\!<\!\kappa\!<\!b$ [14],

where the temporal operators $\mathsf{F}$ and $\mathsf{G}$ in (4) have shorter intervals compared to the original interval $(\,a,\,b\,)$. This form is referred to as syntactic separation since it ensures syntactic equivalence [14, 15], i.e., both sides have the same set of satisfying signals.

In this sense, we aim to decompose the overall synthesis problem into several subproblems with shorter horizons and fewer specifications, inspiring the modularized synthesis of the original specification. More precisely, we focus on the following fragment of complex formulas,

where $\mathsf{G}_{[\,a^{s}_{i},\,b^{s}_{i}\,]}\gamma^{s}_{i}$, $\mathsf{G}_{[\,a^{p}_{j},\,b^{p}_{j}\,]}\mathsf{F}_{[\,0,\,c^{p}_{j}\,]}\gamma^{p}_{j}$, and $\mathsf{F}_{[\,a^{t},\,b^{t}\,]}\mathsf{G}_{[\,0,\,c^{t}\,]}\gamma^{t}$ are the safety, progress, and target subformulas, for $i\!\in\!\{1,2,\cdots,n_{s}\}$ and $j\!\in\!\{1,2,\cdots,n_{p}\}$, $n_{s},n_{p}\!\in\!\mathbb{N}^{+}$, $\gamma^{s}_{i}$, $\gamma^{p}_{j}$, and $\gamma^{t}$ are the boolean formulas that only contain predicates connected with logical operators $\lnot$, $\wedge$, and $\vee$, and $[\,a^{s}_{i},\,b^{s}_{i}\,]$, $[\,a^{p}_{j},\,b^{p}_{j}\,]$, and $[\,a^{t},\,b^{t}\,]$ are the non-empty syntactic intervals of the subformulas. We also refer to $[\,a^{s}_{i},\,b^{s}_{i}\,]$, $[\,a^{p}_{j},\,b^{p}_{j}\!+\!c^{p}_{j}\,]$, and $[\,a^{t},\,b^{t}\!+\!c^{t}\,]$ which represent the complete coverage of the subformulas as their complete intervals, making a clear distinguishment with the syntactic intervals.

Similar to the popularly used GR(1) specifications [20], the fragment $\varphi$ defined above is a complex STL formula composed of three components representing meaningful specifications for practical tasks. The safety part consists of a series of always subformulas specifying the conditions that should always hold. This could include for example safety rules applicable to the system. The progress component contains the always subformulas with eventual operators embedded to represent the tasks that should be performed regularly, such as the monitoring routines. The target component describes the task that should be achieved within a strict deadline. An always formula is embedded to ensure the holding of the target condition for a minimum time.

Specifications in the form of eq. (5) already have a natural division in subformulas for individual subtasks. However, modularized synthesis also requires the division of the subformulas in time. Given a set of ordered timing points $\kappa_{1}\!<\!\kappa_{2}<\!\cdots\!<\!\kappa_{l}$, $\kappa_{z}\!\in\!\mathbb{N}$, $z\!\in\!\{1,2,\cdots,l\}$, $l\!\in\!\mathbb{N}$, we intend to split the specification $\varphi$ into subformulas $\varphi_{z}$ with shorter lengths. Then, modularized synthesis expects to efficiently solve the synthesis problem for $\varphi$ through a sequence of synthesis problems for its subformulas $\varphi_{z}$. To achieve this, the overlapping between the timing intervals of the subformulas should be eliminated to decouple the dependence of different timings. In the next section, we will show that the decoupling of the safety subformulas can be achieved by syntactic separation while ensuring the syntactic equivalence between the separated specification and the original one. However, the progress and the target subformulas are challenging to decouple since the timing overlapping cannot be eliminated by merely using syntactic separation. This has not been well investigated by existing work. We will also show that these subformulas can be decoupled using the complete specification split which ensures soundness but introduces conservativeness. Our work is the first to decompose such STL formulas for modularized synthesis in the literature.

The syntactic separation form of a complex specification in eq. (5) is defined as follows.

Consider the following specifications with the same length $6$: $\varphi_{1}\!=\!\mathsf{G}_{[\,0,\,4\,]}\gamma_{0}\!\wedge\!\mathsf{G}_{[\,2,\,6\,]}\gamma_{1}$, $\varphi_{2}\!=\!\mathsf{G}_{[\,0,\,2\,]}\mathsf{F}_{[\,0,\,1\,]}\gamma_{0}\!\wedge\!\mathsf{G}_{[\,2,\,6\,]}\gamma_{1}$, $\varphi_{3}\!=$ $\mathsf{G}_{[\,0,\,4\,]}\gamma_{0}\!\wedge\!\mathsf{F}_{[\,0,\,4\,]}\!\mathsf{G}_{[\,0,\,2\,]}\gamma_{1}$, and $\varphi_{4}\!=\!\mathsf{G}_{[\,0,\,2\,]}\!\mathsf{F}_{[\,0,\,1\,]}\gamma_{0}\!\wedge\!\mathsf{F}_{[\,3,\,5\,]}\!\mathsf{G}_{[\,1,\,1\,]}\gamma_{1}$, where $\gamma_{0}$, $\gamma_{1}$ are boolean formulas. Consider splitting points $\kappa_{0}\!=\!0$, $\kappa_{1}\!=\!2$, $\kappa_{2}\!=\!6$, according to Definition 1, only $\varphi_{2}$ and $\varphi_{4}$ are in a form that is syntactically separated by $\kappa_{0}$, $\kappa_{1}$, $\kappa_{2}$. Formulas $\varphi_{1}$, $\varphi_{3}$ are not since $\kappa_{1}$ splits the intervals $[\,0,\,4\,]$.

We are interested in translating the specification $\varphi$ (5) into the separated form of (6) using syntactic separation. In this way, the individual numbers of the safety and progress specifications for each timing interval $z\in\{1,2,\cdots,l\}$, denoted as $n_{s,z}$, $n_{p,z}$, can be substantially smaller than those of the corresponding safety and progress specifications, i.e., $n_{s}$, $n_{p}$. The following syntactic separation principles can be used to transform (5) into (6) with syntactic equivalence guaranteed.

Lemmas 2 and 3 provide complementary properties to previous work on syntactic separation [14, 15]. Note that they apply to all STL formulas as introduced in Sec. II-A, but not only the fragment in eq. (5). Most important is theorem 1 which allows separating a subformula into the logical combination of shorter subformulas with an arbitrary number of timing points. Such separation as eq. (6) does not change the syntax of the specification. i.e., for any signal $\mathbf{x}_{[\,0,\,L\,]}$ with $L\!=\!\mathcal{L}(\varphi)$, $\mathbf{x}\!\vDash\!\varphi\!\leftrightarrow\!\mathbf{x}\!\vDash\!\bigwedge_{z=1}^{l}\phi_{z}\wedge\bigvee_{z=1}^{l}\phi^{t}_{z}$. Nevertheless, syntactic timing separation only splits up the syntactic interval of a subformula, which does not eliminate the overlapping between the complete intervals of the subformulas. This is not sufficient for the modularized synthesis of specifications. In the following, we will give an alternative sufficient form of separation that is no longer equivalent to the original specification but ensures the separation of the complete intervals of the subformulas. This form is more conservative than the original specification but ensures the soundness of the solution and allows for modularized solutions to the synthesis problem.

Before we give the complete splitting form of specification (5), we first explain why eliminating the overlapping of the complete intervals of subformulas is important to modularized model checking which is the foundation of modularized synthesis to be explained in the following. Consider an STL specification $\varphi$ and a signal prefix $\mathbf{x}$ with the same length. For a given series of timing points $\kappa_{0},\kappa_{1},\cdots,\kappa_{l}$, modularized model checking investigates under what conditions and what subformulas $\tilde{\varphi}_{1}$, $\tilde{\varphi}_{2}$, $\cdots$, $\tilde{\varphi}_{l}$, where $\mathcal{L}(\bar{\varphi}_{z})\!=\!\kappa_{z}\!-\!\kappa_{z-1}$ for all $z\!\in\!\{1,2,\cdots,l\}$, it ensures that

In such a way, we can split the model checking of the original signal $\mathbf{x}$ and specification $\varphi$ into $l$-steps of model checking for shorter signals $\mathbf{x}_{[\,\kappa_{z-1},\kappa_{z}\,]}\vDash\bar{\varphi}_{z}$ and specifications $\bar{\varphi}_{z}$. This is only feasible when the coverage or the complete interval of the subformulas $\bar{\varphi}_{z}$ is confined within the corresponding interval $[\,\kappa_{z-1},\kappa_{z}\,]$ such that it does not overlap with those of other subformulas. Otherwise, the model checking for the left side of (9) can not be performed independently for each $z\!\in\!\{1,2,\cdots,l\}$ due to the coupled timing dependence.

Based on this consideration, we give the complete specification split form for formula $\varphi$ in eq. (5) as

where, for any $z\!\in\!\{1,2,\cdots,l\}$,

where $\hat{n}_{p,z}$ for any $z\!\in\!\{1,2,\cdots,l\}$, is the number of $j\!\in\!\{1,2,\cdots,n_{p,z}\}$ such that $b^{p}_{z,j}+c^{p}_{z,j}>\kappa_{z}$, i.e., the number of progress formulas that exceed the interval $[\,\kappa_{z-1},\,\kappa_{z}\,]$, and $\tau_{z,r}\!\in\![\,0,\,c^{p}_{z,r}\,]$ for any $r\!\in\!\{1,2,\cdots,\hat{n}_{p,z}\}$, is a heuristic value to be determined beforehand. It can be verified that $\mathcal{L}(\bar{\varphi})\!=\!\kappa_{l}\!=\!\mathcal{L}(\varphi)$. Then, we have the following two theorems to address the relation between the complete split form $\bar{\varphi}$ in eq. (10) and the syntactic separation form $\varphi$ in eq. (6).

Theorem 2 has solved the main problem of modularized model checking for specification $\varphi$ given in eq. (5) by eliminating the overlapping between the complete intervals of its subformulas, as addressed by lemma 4. From a practical perspective, the overlapping means that the timing coupling between different subtasks specifies that these subtasks need to be executed in parallel. In this sense, theorems (2) provide a solution to decouple such dependence by imposing additional specifications to the subtasks, such that they can be solved independently in sequence. The soundness of the complete interval split is ensured by lemma 5. The timing points that mark the solving sequence can be predetermined according to practical requirements.

Given the complete specification split form $\bar{\varphi}$ in eq. (10) for modularized model checking, we can further investigate the modularized synthesis by incorporating the constraints brought up by the dynamic systems (2). For this, we develop algorithm 1 for modularized synthesis of a split specification. In algorithm 1, opt() is a function of the optimization problem in eq. (3) with interface $(x_{0},\,L,\,\varphi)$, and FEASIBLE is a binary variable to indicate whether problem (3) is feasible. Algorithm 1 allows us to perform synthesis for the dynamic system (2) with specification $\bar{\varphi}$ in a modularized way, i.e., by solving a sequence of smaller synthesis problems in a timing order $\kappa_{1}$, $\kappa_{2}$, $\cdots$, $\kappa_{l}$. For each time $\kappa_{z}$, $z\!\in\!\{1,2,\cdots,l\}$, the synthesis subproblem requires substantially fewer integers than the original problem since it involves much shorter and fewer specifications.

Complexity Analysis: As addressed in Sec. II-C, the complexity of directly synthesizing the original specification $\varphi$ in eq. 5 is $O(2^{NL})$, where $L\!=\!\mathcal{L}(\varphi)$ is the length of $\varphi$ and $N:=\max_{x\in\{1,2,\cdot,l\}}(n_{s}+n_{p}+1)$ is the total number of subformulas. For its complete split form $\bar{\varphi}$ in eq. (10), assume that the longest subformula has a length $\bar{L}\!=\!\max_{z\in\{1,2,\cdots,l\}}(\kappa_{z}-\kappa_{z-1})$, the complexity of algorithm 1 is $O(l\cdot 2^{\bar{N}\bar{L}})$, where $\bar{N}\!:=\!\max_{z\in\{1,2,\cdots,l\}}(n_{s,z}\!+\!n_{p,z}\!+\!\hat{n}_{p,z}\!+\!\hat{n}_{p,z-1})$ denotes the maximum number of subformulas in one synthesis module $z\in\{1,2,\cdots,l\}$. As addressed in Sec. III-A and Sec. III-B, from syntactic separation we can expect $n_{s,z}\ll n_{s}$ and $\hat{n}_{p,z}<n_{p,z}\ll n_{p}$ for any $z\!\in\{1,2,\cdots,l\}$, which leads to $\bar{N}\ll N$. Moreover, we can also ensure $\bar{L}\ll L$ by properly selecting the timing points $\kappa_{0}$, $\kappa_{1}$, $\cdots$, $\kappa_{l}$. Thus, with $2^{\bar{N}\bar{L}}\ll 2^{NL}$, modularized synthesis can substantially reduce the complexity of the synthesis problem for long and complex specifications and improve its efficiency.

Limitations: Nevertheless, a limitation of algorithm 1 is that it only ensures soundness but not optimality nor completeness to the original problem. This means that if it generates a feasible solution $\mathbf{x}$, it is certainly a feasible solution to the synthesis problem of the original specification, i.e., $\mathbf{x}\!\vDash\!\varphi$ (soundness). However, it might not be the optimal solution in terms of the robustness $\varrho(\mathbf{x},\varphi)$, i.e., local optimality does not necessarily lead to global optimality. Moreover, if algorithm 1 is not feasible, it does not mean that the original synthesis problem $\mathbf{x}\!\vDash\!\varphi$ is also infeasible (completeness). However, this is already sufficient for most practical robotic tasks. It is also worth noting that algorithm 1 might not be feasible for an arbitrary initial system condition $x_{0}$. For a system (3) and a specification $\bar{\varphi}$ in eq. (10), the initial condition $x_{0}$ that ensures the feasibility of $\mathbf{x}\!\vDash\!\varphi$ belongs to a set which is referred to as the largest satisfaction region [21]. How to utilize the feasible sets to improve the feasibility of a synthesis problem is also partially discussed in a recent work [16]. We are not providing further discussions on this since it is out of the scope of this paper.

For 1), from the definition of STL syntax, we know, for an arbitrary STL formula $\varphi$, $\mathsf{F}_{\{\kappa\}}\varphi=\top\mathsf{U}_{\{\kappa\}}\varphi$ indicates that there must exist $k\in\{\kappa\}$, such that $(x,k)\vDash\varphi$, which means $(x,\kappa)\vDash\varphi$. Then, from $\mathsf{G}_{\{\kappa\}}\varphi=\lnot\mathsf{F}_{\{\kappa\}}\lnot\varphi$ and lemma 1, we know $\mathsf{G}_{\{\kappa\}}\varphi\leftrightarrow\lnot\left(\lnot\mathsf{F}_{\{\kappa\}}\varphi\right)=\mathsf{F}_{\{\kappa\}}\varphi$.

For 2), according to lemma 1, we have $\mathsf{F}_{\{\kappa\}}(\varphi_{1}\!\vee\!\varphi_{2})=\lnot\mathsf{F}_{\{\kappa\}}(\lnot\varphi_{1}\!\wedge\!\lnot\varphi_{2})\!=\!\lnot(\mathsf{F}_{\{\kappa\}}\lnot\varphi_{1}\wedge\mathsf{F}_{\{\kappa\}}\lnot\varphi_{2})$. Then, using lemma 1, we obtain $\mathsf{F}_{\{\kappa\}}(\varphi_{1}\!\vee\!\varphi_{2})=\lnot(\lnot\mathsf{F}_{\{\kappa\}}\varphi_{1}\!\wedge\!\lnot\mathsf{F}_{\{\kappa\}}\varphi_{2})=\mathsf{F}_{\{\kappa\}}\varphi_{1}\vee\mathsf{F}_{\{\kappa\}}\varphi_{2}$, which also holds for $\mathsf{G}$, i.e., $\mathsf{G}_{\{\kappa\}}(\varphi_{1}\vee\varphi_{2})=\mathsf{G}_{\{\kappa\}}\varphi_{1}\vee\mathsf{G}_{\{\kappa\}}\varphi_{2}$, according to 1) of this lemma.

For 3), for $\kappa<a$, we have

Applying lemma 1 to $\mathsf{F}_{\{\kappa\}}\mathsf{G}_{(\,a,\,b\,)}\varphi$, we have $\mathsf{F}_{\{\kappa\}}\mathsf{G}_{(\,a,\,b\,)}\varphi=\mathsf{F}_{\{\kappa\}}\left(\lnot\mathsf{F}_{(\,a,\,b\,)}\lnot\varphi\right)=\lnot\mathsf{F}_{\{\kappa\}}\!\left(\mathsf{F}_{(\,a,\,b\,)}\lnot\varphi\right)$. Considering (12), we have $\mathsf{F}_{\{\kappa\}}\mathsf{G}_{(\,a,\,b\,)}\varphi=\lnot\mathsf{F}_{(\,\kappa+a,\,\kappa+b\,)}\lnot\varphi=\mathsf{G}_{(\,\kappa+a,\,\kappa+b\,)}\varphi$. According to condition 1), we know,