Uncertainty-Aware Signal Temporal Logic Inference

Abstract

Temporal logic inference is the process of extracting formal descriptions of system behaviors from data in the form of temporal logic formulas. The existing temporal logic inference methods mostly neglect uncertainties in the data, which results in the limited applicability of such methods in real-world deployments. In this paper, we first investigate the uncertainties associated with trajectories of a system and represent such uncertainties in the form of interval trajectories. We then propose two uncertainty-aware signal temporal logic (STL) inference approaches to classify the undesired behaviors and desired behaviors of a system. Instead of classifying finitely many trajectories, we classify infinitely many trajectories within the interval trajectories. In the first approach, we incorporate robust semantics of STL formulas with respect to an interval trajectory to quantify the margin at which an STL formula is satisfied or violated by the interval trajectory. The second approach relies on the first learning algorithm and exploits the decision trees to infer STL formulas to classify behaviors of a given system. The proposed approaches also work for non-separable data by optimizing the worst-case robustness margin in inferring an STL formula. Finally, we evaluate the performance of the proposed algorithms and present the obtained numerical results, where the proposed algorithms show reduction in the computation time by up to the factor of 95 on average, while the worst-case robustness margins are improved by up to 330% in comparison with the sampling-based baseline algorithms.

Appendices

Appendix 1 Supplementary Mathematical Materials

1.1 1.1 Proof of Theorem 1

Proof

For two given disjoint intervals, $[\underline{a},\overline{a}]$ and $[\underline{b},\overline{b}]$, we know that $\underline{a}\le \overline{a}$ and $\underline{b}\le \overline{b}$. If $\overline{a}<\underline{b}$, then we define $[\underline{a},\overline{a}]<[\underline{b},\overline{b}]$; or if $\overline{b}<\underline{a}$, then $[\underline{a},\overline{a}]>[\underline{b},\overline{b}]$.

For two interval trajectories, $[\underline{\zeta },\overline{\zeta }]^i$ with label $l_i=+1$ and $[\underline{\zeta },\overline{\zeta }]^{\tilde{i}}$ with label $l_{\tilde{i}}=-1$, if there exists one time-step $t_j$ and one dimension k such that $[\underline{\zeta }_j^k,\overline{\zeta }_j^k]^{\tilde{i}}\cap [\underline{\zeta }_j^k,\overline{\zeta }_j^k]^i=\emptyset$; then, either $[\underline{\zeta }_j^k,\overline{\zeta }_j^k]^i>[\underline{\zeta }_j^k,\overline{\zeta }_j^k]^{\tilde{i}}$ or $[\underline{\zeta }_j^k,\overline{\zeta }_j^k]^i<[\underline{\zeta }_j^k,\overline{\zeta }_j^k]^{\tilde{i}}$. Without loss of generality, we take $[\underline{\zeta }_j^k,\overline{\zeta }_j^k]^i>[\underline{\zeta }_j^k,\overline{\zeta }_j^k]^{\tilde{i}}$. Moreover, we know that $\overline{\zeta }_j^k\in [\underline{\zeta }_j^k,\overline{\zeta }_j^k]^{\tilde{i}}$ and $\underline{\zeta }_j^k\in [\underline{\zeta }_j^k,\overline{\zeta }_j^k]^{{i}}$ are real numbers. If we represent $\overline{\zeta }_j^k\in [\underline{\zeta }_j^k,\overline{\zeta }_j^k]^{\tilde{i}}$ by $\tilde{d}$, and represent $\underline{\zeta }_j^k\in [\underline{\zeta }_j^k,\overline{\zeta }_j^k]^{{i}}$ by d, we know for any two real numbers $\{d,\tilde{d}~|~ d>\tilde{d}\}$, there is a real value $\delta =\frac{\tilde{d}+d}{2}$ such that $d>\frac{\tilde{d}+d}{2}>\tilde{d}$. Then, we can conclude that $[\underline{\zeta }_j^k,\overline{\zeta }_j^k]^{i}>\delta$. Therefore, there exists at least one STL formula in the form of $\mathbf {F}_{[t_j,t_{j+1})}(x^k>\delta )$ that perfectly classifies the two interval trajectories.   $\square$

1.2 1.2 Proof of Theorem 2

Proof

Given a labeled set of interval trajectories $\mathcal {D} _{unc}=\{([\underline{\zeta },\overline{\zeta }]^i,l_i)\}^{N_D}_{i=1}$, we represent interval trajectories with label $l_{{i}}=+1$ by $[\underline{\zeta },\overline{\zeta }]^i$ and represent interval trajectories with label $l_{{i'}}=-1$ by $[\underline{\zeta },\overline{\zeta }]^{{i'}}$.

By relying on Theorem 1, if all the pairs of interval trajectories $[\underline{\zeta },\overline{\zeta }]^i$ and $[\underline{\zeta },\overline{\zeta }]^{i'}$ are separable, then a formula $\varphi _{ii'}$ can be found that is strongly satisfied by interval trajectories $[\underline{\zeta },\overline{\zeta }]^i$ with the label $l_i=+1$ and is strongly violated by interval trajectories $[\underline{\zeta },\overline{\zeta }]^{i'}$. This formula can be in the form of $\varphi :=\bigvee _{([\underline{\zeta },\overline{\zeta }]^i, +1) \in \mathcal {D} _{unc}} \bigwedge _{([\underline{\zeta },\overline{\zeta }]^{i'}, -1) \in \mathcal {D} _{unc}}\varphi _{ii'}$. This formula can strongly classify the two sets of interval trajectories since $\varphi$ is strongly satisfied by all $[\underline{\zeta },\overline{\zeta }]^i$ and strongly violated by all $[\underline{\zeta },\overline{\zeta }]^{i'}$.   $\square$

1.3 1.3 Proof of Lemma 1

Proof

This statement can be proven by induction over robustness semantics and Definitions 1 and 2. Equations (5) and (6) are true on the formulas of size one (the predicates $\pi$) when $t_j \le T$, i.e., when the trajectory is sufficiently long enough. We now prove that Eqs. (5) and (6) hold on longer STL formulas, i.e., assuming they hold for a formula of size n, that they hold for a formula of size $n+1$. For example, we present the induction for the “not” operator and the weak view (similar induction can be done for the strong view, and for the other operators): we assume that Eq. (5) holds for formula $\varphi$ (Eq. (22)), and we deduce that Eq. (6) holds for formula $\lnot \varphi$ (Eq. (24)). We use the semantic rules to transform Eq. (22) into Eq. (23), and Eq. (24) is the contrapositive of Eq. (23).

$$\begin{aligned} r(\zeta ,\varphi ,t_j) > 0&\implies (\zeta ,t_j)\models _{S}\varphi \implies r(\zeta ,\varphi ,t_j) \ge 0 \end{aligned}$$

(22)

$$\begin{aligned} r(\zeta ,\lnot \varphi ,t_j) < 0&\implies (\zeta ,t_j)\not \models _{W}\lnot \varphi \implies r(\zeta ,\lnot \varphi ,t_j) \le 0 \end{aligned}$$

(23)

(24)

   $\square$

1.4 1.4 Proof of Theorem 3

Proof

We consider here only the interval trajectories $[\underline{\zeta },\overline{\zeta }]^i$ such that $l_i=+1$. If $F( \mathcal {D} _{unc},\varphi ) > 0$ holds, then by definition (Eqs. (4) and (3)) we have $\underline{r}([\underline{\zeta },\overline{\zeta }]^i,\varphi ,t_0) > 0$; using Eq. (1), we deduce $\forall {\zeta \in [\underline{\zeta },\overline{\zeta }]^i}, r(\zeta ,\varphi ,t_0) > 0$; using Lemma 1, we finally deduce $\forall {\zeta \in [\underline{\zeta },\overline{\zeta }]^i}, (\zeta ,t_0)\models _{S}\varphi$. We can prove the same way that for every $[\underline{\zeta },\overline{\zeta }]^i$ such that $l_i=-1$, if $F( \mathcal {D} _{unc},\varphi ) > 0$ holds, then $\forall {\zeta \in [\underline{\zeta },\overline{\zeta }]^i}, (\zeta ,t_0)\models _{S}\lnot \varphi$. This means that if $F( \mathcal {D} _{unc},\varphi ) > 0$ holds, then $\varphi$ perfectly classifies $\mathcal {D} _{unc}$. We can prove in a similar way that if $\varphi$ perfectly classifies $\mathcal {D} _{unc}$, then $F( \mathcal {D} _{unc},\varphi ) \ge 0$.   $\square$

Appendix 2 Baseline Algorithms

Random Sampling over Interval Trajectories: We present two other algorithms, TLI-RS and TLI-RS-DT, that we use as baseline algorithms. For both of the baseline algorithms, we first randomly sample finitely many trajectories within each labeled interval trajectory from $\mathcal {D} _{unc}$ and these labeled sampled trajectories $\mathcal {D}$ are input to the baseline algorithms. Algorithm 3 and Algorithm 4 present the detailed procedures for the two baseline algorithms TLI-RS and TLI-RS-DT, respectively.

Baseline Temporal Logic Inference Algorithm (TLI-RS): Algorithm 3 shows the procedure of TLI-RS after the random sampling of $\mathcal {D} _{unc}$ into $\mathcal {D}$. This algorithm is inspired by [44] and presents similarities with Algorithm 1 in its structure. We cover the key differences of Algorithm 3 here.

We define propositional formulas $\varPhi ^{n}_{\zeta }$ for each trajectory $\zeta$ that tracks the valuation of the STL formula encoded by $\varPhi ^{DAG}_{n}$ on $\zeta$. These formulas are built using variables $y_{i,j}^{\zeta }$, where $i\in \{1,\ldots ,n\}$ and $j\in \{1,\ldots ,|\zeta |-1\}$, that corresponds to the value of $(\zeta ,t_j)\models _{S}\varphi _i$ ($\varphi _i$ is the STL formula rooted at Node i).

We now define the constraint that ensure consistency with the sample $\varPhi ^{ \mathcal {D} }_{n}$:

$$\begin{aligned} \varPhi ^{ \mathcal {D} }_{n} = \bigwedge \limits _{(\zeta , l)\in Z } \varPhi ^{n}_{\zeta } \wedge \bigwedge \limits _{(\zeta ,+1)\in \mathcal {D} } y_{n,0}^{\zeta } \wedge \bigwedge \limits _{(\zeta ,-1)\in \mathcal {D} } \lnot y_{n,0}^{\zeta } \end{aligned}$$

Each of the $y_{n,0}^{\zeta }$ and $\lnot y_{n,0}^{\zeta }$ are soft constraints (for sake of simplicity, each one is attributed a weight of 1); all the other constraints are hard constraints.

The previously defined soft constraints aim at correctly classifying a maximum number of trajectories in $\mathcal {D}$. We introduce a new stopping criterion that is triggered when the percentage of correctly classified trajectories exceeds a given threshold $\kappa \in [0,1]$. With $\kappa = 1$ and $N=+\infty$, and assuming that $\mathcal {D}$ is separable, Algorithm 3 terminates and return a formula $\varphi$ that perfectly classifies $\mathcal {D}$. However, due to the nature of random sampling, it is not ensured that $\varphi$ perfectly classifies $\mathcal {D} _{unc}$.

Decision Tree Variant of TLI-RS (TLI-RS-DT): Algorithm 4 shows the procedure of TLI-RS-DT after the random sampling of $\mathcal {D} _{unc}$ into $\mathcal {D}$. This algorithm is inspired by [44] and presents similarities with Algorithm 2 in its structure. Note that we split at line 2 $\mathcal {D}$ into strong satisfied and weakly violated samples as in Eqs. (25) and (26):

(25)

(26)

Appendix 3 Supplementary Numerical Evaluation Results

1.1 3.1 Numerical Results of Sampling-Based Baseline Algorithm TLI-RS

In Tables 2 and 3, the inferred formulas by TLI-RS with corresponding worst-case robustness margins can be seen for $\mathcal {D}_{50}$ and $\mathcal {D}_{200}$, respectively.

Table 2. The inferred STL formulas by TLI-RS for $\mathcal {D}_{50}$, and the corresponding worst-case robustness margins for each of the 10 generated datasets.

Table 3. The inferred STL formulas by TLI-RS for $\mathcal {D}_{200}$, and the corresponding worst-case robustness margins for each of the 10 generated datasets.

We used the same $N$ values for each dataset in the scenarios of Tables 1, 2 and 3 (including TLI-UA for interval trajectories, TLI-RS for $\mathcal {D}_{50}$, and TLI-RS for $\mathcal {D}_{200}$). By comparing the derived worst-case robustness margins for the 10 randomly generated datasets, it can be concluded that TLI-UA infer STL formulas with higher worst-case robustness margins. This trend is consistent in both the separable datasets (datasets 1 to 5) and the non-separable datasets (datasets 6 to 10). Finally, a comparison between Tables 1, 2, and 3 reveals that using TLI-UA improves the worst-case robustness margins by 330% on average in comparison with the worst-case robustness margins in Table 2 ($\mathcal {D}_{50}$), and by 98% on average in comparison with the worst-case robustness margins in Table 3 ($\mathcal {D}_{200}$).

Fig. 6.

The illustration of the Pusher-robot in the simulation environment with the two components denoted as the forearm and the upper arm, where the goal of the Pusher-robot is to interact with a ball and a wall with four different strategies.

Table 4. The inferred STL formulas by TLI-UA, in the Pusher-robot scenario, for strategies 1 to 4, and the corresponding worst-case robustness margins for the change in the speed of the ball when performing the current strategy.

1.2 3.2 Strategy Inference of Pusher-Robot Scenario

In this case study, we infer uncertainty-aware STL formulas to describe the behavior of the interval trajectories of a Pusher-robot with the goal of interacting with a ball and a wall. The interval trajectories are generated by policies learned from reinforcement learning (RL) using model-based reinforcement learning (MBRL) algorithm [45]. The intervals represent the uncertainties associated with the policies and the environment. This Pusher-robot consists of two components denoted as the “forearm” and the “upper arm” (Figure 6). In this paper, we investigate four different strategies of this Pusher-robot: 1) Tap the ball toward the wall. 2) Tap the ball, rotate around, and stop the ball. 3) Tap the ball, stop the ball with the upper arm. 4) Bounce the ball off the wall. We infer an STL formula for each strategy versus the other three strategies based on the change of the speed (m/s) of the ball during performing the current strategy which is denoted by $x^1$. For the dataset, $P_{unc}$ includes the interval trajectories of the current strategy, and $N_{unc}$ includes the interval trajectories of the other three strategies. The inferred STL formulas are presented in Table 4. If $x^1<0$, the contact (the contact between the robot and the wall or contact between the ball and the ball) absorbs the momentum of the ball, and if $x^1>0$, then the contact adds momentum to the ball.

The interpretations of the inferred STL formulas for the strategies, respectively from 1 to 4, are: 1) The change in the speed of the ball is greater than –0.232 m/s, until some time from time-step 2 to time-step 4, the change in the speed of the ball is greater than –0.232 m/s (transition from losing momentum to gaining momentum). 2) The change in the speed of the ball is greater than 0.21 m/s , until some time from time-step 0 to time-step 3, the change of the speed of the ball is always greater than 0.21 m/s (gaining momentum from time-step 0 to time-step 3). 3) Some time from time-step 1 to time-step 4, the change of the speed of the ball is always greater than 0.266 m/s and gaining momentum. 4) The change in the speed of the ball is greater than 0.231 m/s, until some time from time-step 4 to time-step 5, the change in the speed of the ball is greater than 0.231 m/s (gaining momentum).