STL2vec: Signal Temporal Logic Embeddings for Control Synthesis With Recurrent Neural Networks

Recently, formal methods have attracted much attention in control to address complex and temporal objectives such as periodic, sequential, or reactive tasks, going beyond the traditional control objectives like stability and tracking. Temporal logics such as linear temporal logic (LTL)[1], metric temporal logic (MTL)[2], and signal temporal logic (STL)[3] allow us to write down formal descriptions for these specifications.

In this paper, we focus on dealing with the STL specifications, which can specify the temporal properties of real-valued signals. One of the notable advantages of using the STL specifications in control is that we have access to the quantitative semantics, called robustness, which measures how much a signal satisfies the STL specification. The robustness has been used for control purposes in many existing works [4, 5, 6, 7, 8, 9, 10]. The authors of [4, 5, 6] proposed a scheme of encoding STL constraints or robustness of the STL specifications by mixed-integer linear constraints, and these are utilized to employ model predictive control (MPC). To alleviate the computational burden of mixed-integer programming, the works [7, 8, 9, 10] proposed the concept of smooth robustness, allowing us to solve the maximization problem of the robustness based on gradient-based algorithms.

Aiming to further improve the scalability and meet real-time requirements, neural network (NN) based feedback controller was employed for STL tasks [11, 12, 13, 14, 15]. Although the learning procedure itself may be time-consuming, once this computation can be done offline, applying the resulting controller online becomes much faster than directly solving the optimization problem at each time step. In [11], the parameters of the feed-forward NN were trained to maximize the robustness of the STL specifications. Reinforcement learning algorithms such as deep Q-learning (DQN) and learning from demonstrations (Lfd) were used for learning the NN controller in [12] and [13] respectively. The works of [14, 15] used a recurrent neural network (RNN) [16] instead of a feed-forward NN, which is more suitable for control with STL specifications since the satisfaction of an STL formula depends on a state trajectory (not just the current state). In [14, 15], RNN parameters were trained using imitation learning and model-based reinforcement, respectively.

However, the afore-cited previous works can deal with only one STL specification (i.e., the NN controller is trained for only one prescribed STL specification), and did not explicitly deal with multiple STL specifications. In particular, it may be more desirable and flexible in practice that the user is able to choose an STL specification freely from multiple STL specifications, such as the case where a surveillance task in a certain region (building, park, etc.) changes from day to day. A naive approach to achieve this would be to learn a set of NN controllers independently for all the candidate STL specifications, although this would be expensive in terms of memory consumption and computational resources if the number of the STL specifications is large (i.e., the number of the parameters to be learned could increase as the number of the candidate STL specifications increases). Hence, we here consider learning a single NN controller, in which not only the states of the system but also a chosen STL specification are regarded as inputs to the NN. We in particular focus on learning an RNN controller since as previously mentioned, it is suitable for dealing with history dependent nature of the STL specifications. The above formulation leads us to the following question to be answered, which has not been investigated in previous works of literature:

How should we encode the STL specifications by vectors, so that they are readable to the RNN?

Naively, we could assign any unique numbers or one-hot vectors to all the STL specifications and use them as the inputs to the RNN. Although these approaches are easy to implement, information about the similarities in the specifications cannot be encoded with these schemes. Thus, the underlying function to be learned can be unreasonably complex as the number of candidate STL specifications increases, which leads to increased computation time for training as well as a critical failure in control execution.

Motivated by the above issue, we propose a novel scheme for constructing a vector representation of STL specifications, called STL2vec, which captures similarities between the STL specifications. The vectors for the specifications will be trained based on Word2vec [17, 18] which is a technique widely known in natural language processing. Then, the parameters for the RNN are trained by taking the vectors obtained by STL2vec and state trajectory as the inputs (to the RNN) and defining a loss function by the average of negative robustness scores for all the candidate STL specifications.

The main contributions of this work are summarized as follows. First, we propose a method for obtaining vector representations of STL specifications that capture their similarities in terms of control policy. Although STL2vec is constructed based on the concept of word2vec, which is a technique that maps a word of the natural language onto the vector space, how to generate a dataset to learn appropriate vector representations for STL specifications in control synthesis is not a trivial problem. We address the details on how to construct dataset to train appropriate STL2vec in Section V. Second, by using the vectors generated by STL2vec, we train the controller that can deal with multiple STL specifications with one RNN model. Naively, if one aims to train the NN controller to deal with multiple specifications by simply applying existing NN-based control synthesis methods such as [11, 12, 13, 14, 15], one needs to ready NN models as many as the number of the STL specifications, which leads to large memory consumption and computational resources (for details, see Section V-C). Moreover, the proposed method has the potential to accelerate the training as will be seen in the case study of Section VI. Although there exist other methods that make the NN controller flexible such as [14] and [19], which can handle (unknown) obstacles by using control barrier function, these methods are restricted to the specification of only collision avoidance and thus are not intended to deal with multiple temporal logic specifications. The proposed method in this paper allows us to overcome such limitations; it allows the user to have a flexibility of selecting an STL specification freely from multiple ones, and this will be achieved by constructing STL2vec.

Let us now formulate a problem that we seek to solve throughout the paper. First, let $\Phi=\{\phi_{1},\phi_{2},\ldots,\phi_{M}\}$ denote a set of $M$ candidate STL specifications. We assume that the STL specification can be freely chosen from the $M$ candidate specifications by the user before the control execution. Once the STL specification is chosen by the user, say $\phi_{i}\in\Phi$, the system (1) is then controlled aiming to satisfy $\phi_{i}$. We also assume for simplicity that the chosen STL specification is fixed during control execution (as detailed below).

In this paper, we aim to learn a feedback controller that maximizes the robustness of the STL specification. Note that the satisfaction and the robustness of an STL specification are defined over the trajectory of the system (1), and that the STL specification is freely chosen from $\Phi$. Hence, we should design a control policy that depends not only on the past and present states, but also on the STL specification, i.e., we need to obtain a control policy of the form $u_{t}=\pi(x_{0:t},\phi_{i};W)$, where $x_{0:t}=x_{0},x_{1},\dots,x_{t}$ is the trajectory of the system (1), $\phi_{i}$ is the STL specification that is chosen from $\Phi$, and $W$ denotes a set of parameters to be learned to characterize the control policy $\pi$. More formally, the problem considered in this paper is defined as follows:

In Problem 1, we look for a set of the parameters of the control policy $W$ that maximizes the sum of the expectation of the robustness score with respect to the distribution of initial states over all $M$ candidate STL specifications. Since the control policy depends on the past and present states, or it is history dependent, in this paper we use a recurrent neural network (RNN) to learn the control policy $\pi$ (see, [14, 15]). RNN is a type of a neural network that has a feedback architecture. A basic structure of the RNN is illustrated in Fig. 1. As shown in Fig. 1, RNN keeps processing the sequential information via internal hidden state $h$. The update rule of the hidden state and derivation of the output at time $t$ are as follows:

where $g_{W_{1}}$ and $l_{W_{2}}$ are the functions parameterized by weights $W_{1}$ and $W_{2}$, respectively, and $s_{t}$ denotes the input that is fed to the RNN. Hence, the set of the RNN parameters is given by $\{W_{1},W_{2}\}$. As discussed in [11], we can restrict the output of the RNN (i.e., the control input $u_{t}$) within the lower bound $u_{\mathrm{min}}$ and the upper bound $u_{\mathrm{max}}$ by defining each element $i$ $(i=1,\dots,m)$ of the function $l_{W_{2}}$ as follows:

where the subscript $i$ denote $i$-th element of the vector. Using (6), we can generate control inputs satisfying $u_{t}\in\mathcal{U}$. A detailed definition of $s_{t}$ in (5) as well as a concrete procedure to learn $W_{1},W_{2}$ are elaborated in Section V.

Indeed, solving Problem 1 is not trivial and challenging in the following sense. Since the control policy depends on an STL specification $\phi_{i}$, we should consider how to transform each STL specification $\phi_{i}\in\Phi$ into a corresponding vector, so that it can be fed to the RNN as the inputs together with the state trajectory $x_{1:t}$. Intuitively, it may be desirable that we can provide similar inputs to the RNN if the two STL specifications are close to each other in terms of their control policies. For example, consider a simple case with $x\in\mathbb{R}$ and the STL candidate specifications

Intuitively, control policies to satisfy $\phi_{1}$ and $\phi_{2}$ may be almost the same (as we aim to control the system to the same region with almost the same time intervals), while the control policies to satisfy $\phi_{1}$ and $\phi_{3}$ may be quite different (as we aim to control the system to different regions). In addition, if we could find a control policy to satisfy $\phi_{3}$, this control policy also leads to the satisfaction of $\phi_{4}$. Hence, it is convenient that we could provide a certain mapping, where $\phi_{1}$ and $\phi_{2}$ are mapped onto the vector points that are close to each other but far from those corresponding to $\phi_{3}$ and $\phi_{4}$. In addition, $\phi_{3}$ and $\phi_{4}$ are mapped onto the same vector points if a control policy to satisfy $\phi_{3}$ could be found.

Motivated by the above intuition, in this paper we propose a novel scheme for constructing a vector representation of the STL specifications, which is referred to as STL2vec. The proposed approach is inspired by the notion of Word2vec [17], a vector representation of words that has been proposed in machine learning literature and widely utilized for natural language processing. A concrete procedure of the proposed approach is elaborated in Section V.

Before providing the proposed approach, we summarize the basic concept of Word2vec. As we will see in the next section, the concept of Word2vec is a key ingredient to introduce STL2vec and how to train for it. The main objective of Word2vec is to group the vectors of similar or related words (for example, the words ”man” and ”boy” are mapped onto similar points in the vector space). As such, we can let the computer perform mathematical operations on words to detect their similarities. The mapping from each word to the vector is represented via an NN, i.e., the input for the NN is a word, and its output is a corresponding vector. One of the common techniques to train the NN is the skip-gram[17]. The structure of the skip-gram is shown in Fig. 2. As shown in Fig. 2, the skip-gram has a shallow three-layer NN. The input to the NN is an $M$-dimensional one-hot vector, i.e., only one single element is 1 and the other elements are all zero, where $M$ indicates a total number of words in the corpus (typically with $M>10^{6}$). Here, each word is assigned by a unique one-hot vector (for example, ”man” is labeled by $[1,0,0,\ldots,0]^{\mathsf{T}}$, and ”boy” is labeled by $[0,1,0,\ldots,0]^{\mathsf{T}}$, etc.), so that each word in the corpus is readable to the NN. The outputs of the NN are the collection of $P$ ($M$-dimensional) vectors whose each element represents the probability of the corresponding word in the corpus (training data for the output layer will be explained later in this section), where $P$ is a user-defined parameter. The mapping from the input layer to the hidden layer is given by a matrix $W_{\mathrm{in}}\in\mathbb{R}^{M\times N}$, where $N$ is a user-defined parameter that indicates the dimension of the word vector. The mapping from the hidden layer to each output layer is given by another matrix $W_{\mathrm{out}}\in\mathbb{R}^{N\times M}$. Here, we note that the matrix $W_{\mathrm{out}}$ is the same for all the output layers.

The weight parameters $W_{\mathrm{in}},W_{\mathrm{out}}$ are trained from a large number of sentences, such as those in the news report (see, e.g. [17]). For example, suppose $P=2$ and we have a sentence: ”I want to eat an orange every morning”. Then, we regard the training input as a certain word in this sentence and the training output as the set of $P=2$ words around it. For example, the word ”eat” is regarded as the training input, and the set of $P=2$ words around it, i.e., {to, an} is regarded as the training outputs. Generating the training dataset as above is motivated by the insight that the meaning of a word is established by the surrounding words.

Using the dataset constructed above, we train the skip-gram model. First, we pass the one-hot encoded input data to the input layer and perform the forward computation. As an output layer and loss function, we use softmax and cross-entropy loss, respectively. Then, we update the weights $W_{\mathrm{in}}$ and $W_{\mathrm{out}}$ using the gradients obtained by back-propagation computation (for details, see [17]). After the training, the vector representation of each word in the corpus is given through the projection of the weight matrix $W_{\mathrm{in}}$ (hence, we drop the matrix $W_{\mathrm{out}}$ in the skip-gram model). That is, for each word $w$ in the corpus, the corresponding vector representation is given by $z_{w}=W_{\mathrm{in}}e_{w}\in\mathbb{R}^{N}$, where $e_{w}\in\mathbb{R}^{M}$ denotes the one-hot vector of the word $w$.

In this section, we describe the solution approach to Problem 1. The proposed approach consists of the two steps: (i) train a vector representation of the STL specifications, namely STL2vec, whose input is the STL specification $\phi_{i}\in\Phi$ and output is the $N$-dimensional vector; (ii) train the RNN, whose inputs are the state trajectory $x_{0:t}$ and the vector representation of the STL specification $z_{\phi_{i}}$, and the output is the control input $u_{t}$. The illustration of the two steps are shown in Fig. 3. Since STL2vec will be trained based on the skip-gram, the parameter to be learned in Step (i) is $W_{\mathrm{in}}$ (recall in Section IV that we neglect $W_{\mathrm{out}}$). Also, recall that the parameters to be learned for RNN in Step (ii) is $\{W_{1},W_{2}\}$ (see Section III). Hence, the overall parameters to be learned for the control policy $\pi$ is $W=\{W_{\mathrm{in}},W_{1},W_{2}\}$.

The proposed approach is beneficial in the following sense. By constructing STL2vec, we can obtain a vector representation that exhibits similarities between the STL specifications. This allows us to accelerate both efficiency and performance of the RNN controller in contrast to some naive approaches, such as integer or one-hot encoding i.e. simply assigning arbitrary numbers or one-hot vectors to the STL specifications (e.g., $\phi_{1}$ is assigned by 1, $\phi_{2}$ is assigned by 2, and so on) and use these numbers as the inputs to the RNN; for details, see an experimental result in Section VI. Moreover, the proposed approach is more beneficial than the approach of learning RNN controllers one by one for each STL formula in terms of computational memory; for details, see Section V-C and Section VI. The concrete procedures of the above two steps are given in the following subsections.

We show the efficacy of the proposed method through the example of a path planning problem of a vehicle in 2D space. We used PyTorch package [22] for the implementation of RNN, IPOPT in CasADi [23] to solve optimization (10), and STLCG [20] for the computation regarding STL robustness. We used Windows 10 with a 2.80 GHz Core i7 CPU and 32 GB of RAM for all the experiments discussed in this section. Throughout this section, we consider the following nonlinear, discrete-time nonholonomic system: $q_{x,t+1}=q_{x,t}+v_{t}\sin{\theta_{t}}$, $q_{y,t+1}=q_{y,t}+v_{t}\cos{\theta_{t}}$, $\theta_{t+1}=\theta_{t}+\omega_{t}$, where $q_{x,t}$, $q_{y,t}$ represent position of the vehicle, $\theta_{t}$ is the heading angle, $v_{t}$ and $\omega_{t}$ are velocity and angular velocity, respectively. The state $x_{t}$ and control input $u_{t}$ are defined as $x_{t}=[q_{x,t},q_{y,t},\theta_{t}]^{\top}$ and $u_{t}=[v_{t},\omega_{t}]^{\top}$, respectively. As illustrated in Figure 4, we consider 4 regions in a 2D space: $\mathrm{Reg}\ 1=[3,5]\times[7,9]$, $\mathrm{Reg}\ 2=[3,5]\times[3,5]$, $\mathrm{Reg}\ 3=[7,9]\times[3,5]$, $\mathrm{Reg}\ 4=[7,9]\times[7,9]$, and the set of initial states $\mathcal{X}_{0}=[0,0.7]\times[0,0.7]$ (blue-edged color region). In addition, we consider 4 sub-regions in each region, which are labeled by indices as shown in Figure 4. In the following, we denote $j$-th sub-region $(j=1,2,3,4)$ in region $i$ $(i=1,2,3,4)$ as $\mathrm{Reg}\ (i,j)$.

The STL candidate specifications are shown in Table I. Here, the specifications are considered for all $i,i_{1},i_{2},i_{3}\in\{1,\ldots,4\}$ ($i_{1}>i_{2}$, $i_{3}\neq 1$, $i_{1}\neq i_{3}$) and $j,j_{1},j_{2},j_{3}\in\{1,\ldots,4\}$. The total number of the STL candidate specifications is given by $369$.