key: cord-0198841-kx1ewf9k authors: Baharisangari, Nasim; Gaglione, Jean-Raphael; Neider, Daniel; Topcu, Ufuk; Xu, Zhe title: Uncertainty-Aware Signal Temporal Logic Inference date: 2021-05-24 journal: nan DOI: nan sha: 049c8dd3996d49d33b4e1009f7ce59fc1780fa42 doc_id: 198841 cord_uid: kx1ewf9k 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 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 tree 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 in inferring an STL formula. Finally, we evaluate the performance of the proposed algorithms in two case studies, where the proposed algorithms show reductions in the computation time by up to four orders of magnitude in comparison with the sampling-based baseline algorithms (for a dataset with 800 sampled trajectories in total). There is a growing emergence of the artificial intelligence (AI) in different fields, such as traffic prediction and transportation [1] [2] [3] , or image [4] and pattern recognition [5] [6] . Competency-awareness is an advantageous capability that can raise the accountability of AI systems [7] . For example, the AI systems should be able to explain their behaviors in an interpretable way. One option to represent system behaviors is to use formal languages such as linear temporal logic (LTL) [8] [9] . LTL resembles natural language which is interpretable by humans, and at the same time preserves the rigor of formal logics. However, LTL is used for analyzing discrete programs; hence, LTL falls short when coping with continuous systems such as mixed-signal circuits in cyber-physical systems (CPS) [10] [11] [10] . Signal temporal logic (STL) is an extension of LTL that tackles this issue. STL is a temporal logic defined over signals [12] [13] , and branches out LTL in two directions: on top of using atomic predicates, it deploys real-valued variables, and it is defined over time intervals [14] . Recently, inferring temporal properties of a system from its trajectories have been in the spotlight. We can derive such properties by inferring STL formulas. One way of computing such STL formulas is incorporating satisfibilty modulo theories (SMT) solvers such as Z3 theorem prover [15] . Such solvers can determine whether an STL formula is satisfiable or not, according to some theories such as arithmetic theory or bit-vector theory [16] [17] . Most of the frequently used algorithms for STL inference deploy customized templates for a solver to conform to. These pre-determined templates suffer from applying many limitations on the inference process. First, a template that complies with the behavior of the system is not easy to handcraft. Second, the templates can constrain the structure of an inferred formula; hence, the formulas not compatible with the template are removed from the search space [18] [19] [20] [21] . Moreover, the importance of uncertainties is well established in several fields such as machine learning (ML) application in weather forecast [22] , or deep learning application in facilitating statistical inference [23] . Failure to account for the uncertainties in any system can reduce the reliability of the output as predictions in AI systems [24] . Specifically, in AI, uncertainties happen due to different reasons including noise in data or overlap between classes of data [24] . Uncertainty quantification techniques in AI systems have been developed to address this matter [25] . Incorporating the quantified uncertainties in the process of inferring temporal properties can lead to higher credibility of the predictions. However, most of the current approaches of inferring temporal properties do not account for uncertainties in the inference process. In this paper, we propose two uncertainty-aware algorithms in the form of STL formulas for inferring the temporal properties of a system. In the proposed algorithms, the uncertainties associated with trajectories describing the evolution of a system is implemented in the form of interval trajectories. The second algorithm relies on the first one and uses decision tree to infer STL formulas. By taking uncertainties into consideration, instead of classifying finitely many trajectories to infer an STL formula that classifies the trajectories, we classify infinitely many trajectories within the interval trajectories (Section IV). See Figure 1 as an illustration. Besides, the uncertainty-aware algorithms quantify the margin at which an interval trajectory violates or satisfies an inferred STL formula by incorporating the robust semantics of uncertainty-aware STL formulas (Section III-B). In addition, we maximize worst-case robustness margin for increasing the robustness of the inferred STL formulas in the presence of uncertainties; thus, we can view our problem as an optimization problem with the objective of maximizing the worst-case robustness margin. Moreover, we introduce a framework in which we employ the optimized robustness to compute the optimal STL formula for non-separable datasets (Section V). We conduct experiments to evaluate the performance of the proposed learning algorithms. Our experimental results show that inferring STL formulas using interval trajectories reduces the computation time up to four orders of magnitudes in comparison with sampling-based baseline algorithms (for a dataset with 800 sampled trajectories in total) while the inferred formula by uncertainty-aware STL is For inferring an STL formula by sampling-based baseline algorithms, we sample finitely many trajectories from each interval trajectory to infer an STL formula to describe the behavior of the trajectories. (b) By uncertainty-aware STL inference, we infer an STL formula to describe the temporal properties of the infinitely many trajectories within the interval trajectories. In this example, the blue tubes represent the interval trajectories with the desired behavior, and the red tube represents the interval trajectory with the undesired behavior. By both the uncertainty-aware STL and sampling-based baseline algorithms, we infer the STL formula G [1, 5) [18] proposed a framework for learning temporal properties using LTL. Several other frameworks for inferring temporal properties such as [30] , [31] , [19] , [21] , [32] , etc have been proposed. In addition, various quantitative semantics have been introduced for temporal logics such as robust semantics. Danze et. al. [33] introduced robust semantics for STL formulas, and Lindemann et. al. [34] introduced predicate robustness. Fainekos et. al. [35] defined robust semantics for metric temporal logic (MTL). Kyriakis et. al. incorporated robust semantics to maximize the efficiency of his StTL inference framework [36] . On the other hand, using decision trees in STL inference have been noteworthy [37] [38] [19] [39] [31] . For example, Brunello et. al. [40] introduced Interval Temporal Logic Decision Trees, where the data is delivered to the decision tree in form of intervals. In this section, we set up definitions and notations used throughout this paper. Finite trajectories: We can describe the state of an underlying system by a vector x = [x 1 , x 2 , .., x n ], where n is a non-negative integer (the superscript i in x i refers to the i-th dimension). The domain of x is denoted by X = X 1 × X 2 × ... × X n , where each X i is a subset of R. The evolution of the underlying system within a finite time horizon is defined in the discrete time domain T = {t 0 , t 1 , ..., t J }, where J is a non-negative integer. We define a finite trajectory describing the evolution of the underlying system as a function ζ : T → X. We use ζ j x(t j ) to denote the value of ζ at time-step t j . Intervals and interval trajectories: An interval, denoted by [a, a], is defined as [a, a] := a ∈ R n a i ≤ a i ≤ a i , i = 1, .., n , where a, a ∈ R n , and a i ≤ a i holds true for all i. The superscript i refers to the i-th dimension. For the purpose of this work, we introduce interval trajectories. We define an interval trajectory [ζ , ζ ] as a set of trajectories such that for any ζ ∈ [ζ , ζ ], we have ζ j ∈ [ζ j , ζ j ] for all t j ∈ T [41] . We know that the time length of a trajectory ζ ∈ [ζ , ζ ] is equal to the time length of an interval trajectory [ζ , ζ ]; thus, we can denote the time length of an interval trajectory [ζ , ζ ] with |ζ|. We first briefly review the signal temporal logic (STL). We start with the Boolean semantics of STL. The domain B = {T rue, F alse} is the Boolean domain. Moreover, we introduce a set Π = {π 1 , π 2 , . . . , π n } which is a set of predefined atomic predicates. Each of these predicates can hold values True or False. The syntax of STL is defined recursively as follows. where stands for the Boolean constant True, π is an atomic predicate in the form of an inequality f (x) > 0 where f is some real-valued function. ¬ (negation), ∧ (conjunction), ∨ (disjunction) are standard Boolean connectives, and "U" is the temporal operator "until". We add syntactic sugar, and introduce the temporal operators "F" and "G" representing "eventually" and "always", respectively. I is a time interval of the form I = [a, b), where a < b, and they are non-negative integers. We call the set containing all the mentioned operators C = { , ∧, ∨, ¬, →, F, G, U}. We employ the Boolean semantics of an STL formula in strong and weak views. We denote the length of a trajectory ζ ∈ [ζ , ζ ] by T [42] . In the strong view, (ζ , t j ) |= S ϕ means that trajectory ζ ∈ [ζ , ζ ] strongly satisfies the formula ϕ at time-step t j . (ζ , t j ) |= S ϕ means that trajectory ζ ∈ [ζ , ζ ] strongly violates the formula ϕ at time-step t j . Similar interpretations hold true for the weak view (|= W means "satisfies weakly" and |= W means "violates weakly" ). By considering the Boolean semantics of STL formulas in strong and weak views, the strong satisfaction or violation of an STL formula ϕ by a trajectory at time-step t j implies the weak satisfaction or violation of the STL formula by the trajectory at time-step t j . Consequently, we can take either of the views for trajectories with label l i = +1 and trajectories with label l i = −1 for perfect classification [42] . In this paper, we choose to adopt the strong view for the problem formulations of Sections IV and V. Definition 1. The Boolean semantics of an STL formula ϕ, for a trajectory ζ ∈ [ζ , ζ ] with the time length of T at time-step t j in strong view is defined recursively as follows. Definition 2. The Boolean semantics of an STL formula ϕ, for a trajectory ζ ∈ [ζ , ζ ] with the time length of T at time-step t j in weak view is defined recursively as follows. (ζ , t j ) |= W π iff either of the 1) or 2) holds: Syntax DAG: Any STL formula can be represented as a syntax directed acyclic graph, i.e., syntax DAG. In a syntax DAG, the nodes are labeled with atomic predicates or temporal operators that form an STL formula [18] . For instance, Figure 2a shows the unique syntax DAG of the formula (π 1 U π 2 )∧G(π 1 ∨π 2 ), in which the subformula π 2 is shared. Figure 2b shows arrangement of the identifiers of each node in the syntax DAG (i ∈ {1, .., 7}). Size of an STL formula: If we present an STL formula by a syntax DAG, then each node corresponds to a subformula; thus, the size of an STL formula is equal to the number of the DAG nodes. We denote the size of an STL formula ϕ by |ϕ| [43] . Robust semantics quantifies the margin at which a certain trajectory satisfies or violates an STL formula ϕ at time-step t j . The robustness margin of a trajectory ζ with respect to an STL formula ϕ at time-step t j is given by r(ζ , ϕ, t j ), where r(ζ, ϕ, t j ) can be calculated recursively via the robust semantics [35] . We can define the robustness margin of an interval trajectory in two views: worst-case and best-case. The worst-case view chooses the trajectory with the minimum corresponding robustness within an interval trajectory (Eq. (1)). The bestcase view chooses the trajectory with maximum corresponding robustness within an interval trajectory (Eq. (2)); thus, we define the robustness margin of an interval trajectory in two views, as follows. In this section, we present the problem formulation of perfectly classifying interval trajectories. Then, we derive the sufficient conditions to solve the problem. The existing methods for inferring STL formulas mostly classify finitely many trajectories without considering the uncertainties. For the problem of classifying finitely many trajectories, we define the following. represents the desired behavior and l i = −1 represents the undesired behavior, an STL formula ϕ, evaluated at time t 0 , perfectly classifies the desired behaviors and the undesired behaviors if the following condition is satisfied. With Definition 3, the problem of STL inference for classifying finitely many trajectories is as follows. , compute an STL formula ϕ such that ϕ, which is evaluated at time t 0 , perfectly classifies the desired behaviors and undesired behaviors, and |ϕ| ≤ N , where N is a predetermined positive integer. Definition 3 cannot classify infinitely many trajectories; thus, by taking the uncertainties into consideration, and substituting trajectories with interval trajectories, we define the following. represents the desired behavior and l i = −1 represents the undesired behavior, an STL formula ϕ, which is evaluated at time t 0 , perfectly classifies the desired behaviors and the undesired behaviors if the following condition is satisfied. Now, we define a problem formulation of classifying infinitely many trajectories within the interval trajectories. , compute an STL formula ϕ, which is evaluated at time t 0 , perfectly classifies the desired behaviors and undesired behaviors, and |ϕ| ≤ N , where N is a predetermined positive integer. We need a sufficient condition that allows us to use Definition 4 to perfectly classify interval trajectories. Before deriving a such condition, we define separable interval trajectories as follows. Definition 5. We define that two interval trajectories [ζ , ζ ] and [ζ , ζ ] are separable if there exists at least one time-step t j and one dimension k such that the two intervals [ζ k j , ζ We define that two finite sets of interval trajectories Z and Z are separable if all pairs of interval trajectories By extension, we write that a labeled set of inter- Now, we provide a sufficient condition that allows us to use Definition 4 to classify two interval trajectories. then there exists at least one STL formula that perfectly classifies these two interval trajectories. Proof: See Appendix A-A Now that we have the sufficient condition for perfect classification of two interval trajectories, we provide the sufficient condition for the case of having multiple interval trajectories. One source of uncertainty in a dataset is overlap between the interval trajectories satisfying an STL formula ϕ and interval trajectories violating ϕ. This type of dataset is called non-separable dataset [44] . We deploy robust semantics to set up a method to infer STL formulas for non-separable dataset with two labeled classes. Therefore, we define that two interval trajectories are non-separable if they are not separable according to Definition 5. Similarly, we define a non-separable labeled dataset if it is not separable according to Definition 6. Given a set of N D labeled interval trajectories , we define in Eq. (3) a functionF that gives the worst-case robustness margin of an interval trajectory [ζ , ζ ] i with respect to ϕ or ¬ϕ if l i = +1 or l i = −1, respectively. We then construct in Eq. (4) our objective function F . If we consider the STL formula for perfect classification of D unc : would be the worst-case robustness margin of it. Hence, F represents the lower worst-case robustness margin amongst all the interval trajectories. Problem 3. Given a possibly non-separable set of labeled , compute an STL formula ϕ that maximizes F (D unc , ϕ) such that |ϕ| ≤ N , where N is a predetermined positive integer. To solve Problem 3, we compute an STL formula ϕ by maximizing F (D unc , ϕ), and we set an upper-bound on the size of the ϕ for interpretability. Figure 3 shows a simple illustrative example of how we useF ([ζ , ζ ] i , l i , ϕ) for computing such an STL formula. In this example, the inferred STL formula can be in the form of ϕ := x 1 > c, where x 1 is the state of a 1-dimensional trajectory. . The vertical axis represents the objective function F , as well as the underlying functionsF for each interval trajectory, and the horizontal axis represents c. In this example, the optimal value for F (D unc , ϕ) is −1 and is achieved at ϕ * = x 1 > c * and c * = 5. In this section, we propose and explain two uncertaintyaware algorithms for STL inference. The first uncertaintyaware algorithm is denoted as TLI-UA. The second algorithm relies on the first one and uses decision tree to infer STL formulas which is denoted as TLI-UA-DT. Satisfiabilty modulo theories (SMT) and OptSMT solvers: One of the common concepts involved in the process of inferring STL formulas is satisfiabilty. Satisfiabilty addresses the following problem statement: How can we assess whether a logical formula is satisfiable? Based on the type of the problem we deal with, we can exploit different solvers. For example, if the satisfiabilty problem is in the Boolean domain, we can use Boolean satisfiability (SAT) solvers; or if the satisfiability problem is in the continuous domain, we can use satisfiability modulo theories (SMT) solvers. In this paper, we consider trajectories in the real domain, as well as time-bounds of temporal operators as integers, thus we use SMT instead of SAT. SMT solvers, based on some theories including arithmetic theories or bit-vectors theory, determine whether an STL formula is satisfiable or not [16] . Another important concept involved is the incorporation of optimization procedures in a SMT problem. Optimization modulo theories (OMT) is an extension of SMT that allows finding models that optimizes a given objective function [45] . There exists several variants of OMT [46] , in particular OptSMT, where an explicit objective function is given, and MaxSMT, where soft constraints with different costs are assigned. Our proposed methods rely on OptSMT. OptSMT-based learning algorithm: In the proposed algorithms, the input to the algorithms is in the form of interval trajectories. This input contains the data whose behaviors we wish to infer STL formulas for, and consists of two possibly non-separable labeled sets P unc , N unc . We categorize P unc as the set containing interval trajectories with desired property (or behavior) and N unc as the set containing interval trajectories with the undesired property (or behavior). We represent the input as a set D unc = P unc ∪ N unc . We present an STL formula by a syntax DAG. The syntax DAG encodes the STL formula by propositional variables. The propositional variables are [18] : To facilitate the encoding, a unique identifier is assigned to each node of the DAG, which is denoted by i ∈ {1, 2, .., n}. Two mandatory properties of this identifier are: 1) The identifier of the root is n, and 2) the identifiers of the children of Node i are less than i. It should be noted that the node with identifier 1 is always labeled with an atomic predicate (π ∈ Π). In the listed variables, x i,λ is in charge of encoding a labeling system for the syntax DAG such that if a variable x i,λ becomes True, then Node i is labeled with λ. The variables l i,k and r i,k encode the left and right children of the inner nodes. If the variable l i,k is set to True, then k is the identifier of the left child of Node i. If the variable r i,k is set to True, then k is the identifier of the right child of Node i. Moreover, if Node i is labeled with an unary operator, the variables r i,k are ignored and, both of the variables l i,k and r i,k are ignored in the case that Node i is labeled with an atomic predicate. Moreover, the reason that identifier i ranges from 2 to n for variables l i,k and r i,k is that Node 1 is always labeled with an atomic predicate and cannot have children. Lastly, k ranging from 1 to i − 1 reflects the point of children of a node having identifiers smaller than their root node. It is crucial to guaranty that each node has exactly one right and one left child. This matter is enforced by Eqs. (5), (6) and (7) . In addition, Eq. (8) ensures that Node 1 is labeled with an atomic predicate. We introduce two sets of integer variables to the syntax DAG to add the time bounds on the temporal operators. These variables are denoted by a i and b i (where subscript i is the node identifier). These two variables are used to store the range of time-step indexes [j+a i , j+b i ) within which the STL formula ϕ i (valuation of formula ϕ at Node i) holds True when evaluated at time-step t j . In the proposed algorithms, only the temporal operators F, G, and U use these a i and b i . We add the following constraint to these variables in Eq. (9) . Let the propositional formula Φ DAG n be the conjunction of Eqs. (5) to (9) . Φ DAG n encodes the syntax DAG structural constraints for a yet unknown formula of size n. We can reconstruct a syntax DAG from a model v, i.e., a valuation of the propositional variables in Φ DAG n , as follows. 1) Label Node i with unique label λ such that v(x i,λ ) = 1 (if label is F, G, or U, assign time interval I = [v(a i ), v(b i )) to the operator), 2) set the node n as the root and finally, 3) arrange the nodes of the DAG according to v(l i,k ) and v(r i,k ). From this syntax DAG, we can derive an STL formula denoted by ϕ v . To implement the framework which is introduced in Section V in the proposed algorithms, we define two real-valued variables: y ζ i,j and y ζ i,j . These two variables are equivalent to the robustness margin at the worst-case and the best-case, respectively. In this section, the time length of an interval trajectory T is represented by |ζ |, and for the better explanation of the algorithm, we denote the index of the time-step as a position in an interval trajectory; hence, in y Specifically, y ζ i,j is used for implementing the robust semantics of negation of an STL formula Eq. (12) . To implement the semantics of the temporal operators and Boolean connectives, we apply the constraints shown in formulas Eqs. (13) to (16) . These constraints are inspired by bounded model checking [47] . It should be noted that these constraints are defined similarly for both y ζ i,j , y ζ i,j . Eq. (13) implements the semantics of the atomic predicates. Eq. (14) implements the semantics of negation. In that formula, if Node i is labeled with ¬ and node k is its left child, then y ζ i,j is the negation of y ζ k,j and its value is −y ζ k,j . Similarly, Eq. (15) implements the semantics of disjunction. In this case, if Node i is labeled with ∨, and node k is its left child and node k is its right child, then y ζ i,j is equal to the maximum value between y ζ k,j and y F [a,b) , G [a,b) , →, ∧, . 1≤i≤n π∈Π 1 N 9 return ϕv produces a formula of maximum size N . The second stopping criteria is triggered when the robustness margin threshold R ∈ R (given as a parameter) is reached. To solve Problem 3, one can set N to the predetermined positive integer described in this problem, and R = +∞ in order to ignore the second stopping criteria. With only the N as the stopping criteria, the loop of the algorithm could be ignored and we could directly start at n = N . In that case, Algorithm 1 returns one of the formula of size N that maximizes F (D unc , ϕ) (such formula is not unique). When a finite R is specified, Algorithm 1 returns an STL formula with size possibly less than N but with F (D unc , ϕ v ) ≥ R. This is particularly useful when the expected size of the STL formula is unknown and N = +∞. Decision Trees over STL Formulas: A decision tree over STL formulas is a tree-like structure where all nodes of the tree are labeled by STL formulas. While the leaf nodes of a decision tree are labeled by either True or False, the non-leaf nodes are labeled by (non-trivial) STL formulas which represent decisions for predicting the class of a trajectory. Each inner node leads to two subtrees connected by edges, where the left edge is represented with a solid edge and the right edge with a dashed one. Figure 4 depicts a decision tree over STL formulas. A decision tree τ over STL formula corresponds to an STL formula ϕ τ := ρ∈R ϕ∈ρ ϕ , where R is the set of paths that originate in the root node and end in a leaf node labeled with True, ϕ = ϕ if it appears before a solid edge in ρ ∈ R, and ϕ = ¬ϕ if it appears before a dashed edge in ρ ∈ R (see Figure 4 ). Decision Tree Variant of TLI-UA (TLI-UA-DT): We propose this second method for uncertainty aware STL inference based on decision trees, outlined by Algorithm 2. First, we infer an STL formula using TLI-UA (line 1). Given the inferred formula ϕ, we need a way to split D unc into two labeled sets D + unc and D − unc . Note that the set of [ζ , ζ ] i with label l i = +1 that strongly satisfies ϕ and the set of [ζ , ζ ]î with the label lî = −1 that strongly violates ϕ do not necessarily partition the D unc . As an alternative, we choose to split D unc with respect to an averaged robustness margin Algorithm 2: TLI-UA-DT return decision tree with root node ϕ and subtrees τ1, τ2 as in Eqs. (18) and (19) , in order to have a partition (line 2): Based on D + unc and D − unc , Algorithm 2 is applied recursively (lines 6 and 7), if Algorithm 2 does not terminate at lines 3 and 4. We define the stopping criteria, stop(D + unc , D − unc ), for Algorithm 2 as the following: This stopping criteria guarantees the termination of this method, as the sample size decreases at each split until no split is possible anymore. In this section, we evaluate the performance of the uncertainty-aware proposed algorithms. In the following, we compare TLI-UA with TLI-RS, and compare TLI-UA-DT with TLI-RS-DT. We implement all following four algorithms in a C++ toolbox 1 using Microsoft Z3 [15] : • For STL inference using TLI-RS and TLI-RS-DT, we randomly sample a certain number of trajectories from each interval trajectory in the dataset D unc . For STL inference using TLI-UA and TLI-UA-DT, we directly encode the interval trajectories to the OptSMT solver. To evaluate the performance of the uncertainty-aware proposed algorithms, we generate 10 datasets. Among these datasets, five datasets are non-separable, and five datasets are separable. In each dataset, both of the sets P unc and N unc contain up to three interval trajectories with the time length 1 https://github.com/cryhot/uaflie up to 10. We use these 10 datasets to infer STL formulas by exploiting algorithms TLI-UA and TLI-UA-DT. The inferred STL formulas by TLI-UA are listed in table I with the corresponding optimal worst-case robustness margins denoted by superscript *. Then, we sample 200 trajectories from each interval trajectory in each dataset to infer STL formulas from TLI-RS and TLI-RS-DT algorithms. First, we evaluate and compare the performance of TLI-UA and TLI-RS. We choose 1000 seconds for the timeout on each execution. For each individual dataset, we use the same values of parameter N for both TLI-UA and TLI-RS when inferring STL formulas for the datasets. The comparison of the execution time of these two algorithms can be seen in Figure 5a . The results show that the execution time of TLI-UA is at most 1/100 of the the execution time of TLI-RS (for a dataset with 800 sampled trajectories in total). Next, we compare TLI-UA-DT and TLI-RS-DT. We In this case-study, we infer uncertainty-aware STL formulas to describe the behavior of the interval trajectories of a Pusherrobot. The interval trajectories are generated by policies learned from reinforcement learning (RL) using model-based reinforcement learning (MBRL) algorithm [48] . The intervals represent the uncertainties associated with the policies and the formulas by TLI-UA (ϕ) environment. This robot consists of two components denoted as the "forearm" and the "upper arm" (Figure 7) . In this paper, we investigate four different strategies of this Pusherrobot: 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 II . If x 1 < 0, the contact (the contact between the robot and the wall or contact between the ball and the ball) absorbs 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 sometime 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 timestep 0 to time-step 3, the change of the speed of the ball is always greater than 0.21 m/s (gaining momentum from timestep 0 to time-step 3). 3) Some time from time-step 1 to timestep 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 sometime 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). In this paper, we proposed two uncertainty-aware STL inference algorithms. Our results showed that uncertaintyaware STL inference expedites the inference process in the presence of uncertainties. Exploiting uncertainty-aware STL inference to enhance RL is one future research direction (in a similar manner as in [49] ). Moreover, we aim to develop the proposed learning algorithms to uncertainty-aware graph temporal logic (GTL) inference, where we can infer spatial temporal properties from data with uncertainties [50] . The authors thank Dr. Rebecca Russell and the entire AL-PACA team for their collaboration. This material is based upon work supported by the Defense Advanced Research Projects Agency (DARPA) under Contract No. HR001120C0032. Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of DARPA. Improving Urban Traffic Speed Prediction Using Data Source Fusion and Deep Learning A deeplearning model for urban traffic flow prediction with traffic events mined from twitter Machine Learning-based traffic prediction models for Intelligent Transportation Systems Deep learningbased image recognition for autonomous driving Machine Learning: Algorithms, Real-World Applications and Research Directions Pattern Recognition and Machine Learning Motion Planning with Competency-Aware Transition Models for Underactuated Adaptive Hands Interpretable sequence classification via discrete optimization Limit state function identification using Support Vector Machines for discontinuous responses and disjoint failure domains Reactive synthesis from signal temporal logic specifications Bounded model checking of signal temporal logic properties using syntactic separation Parametric identification of temporal properties Monitoring temporal properties of continuous signals Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic Z3: An efficient smt solver Satisfiability modulo theories: An appetizer Handbook of model checking Learning Linear Temporal Properties A decision tree approach to data classification using signal temporal logic A Temporal Logic Inference Approach for Model Discrimination Temporal Logic Inference with Prior Information: An Application to Robot Arm Movements Machine learning based algorithms for uncertainty quantification in numerical weather prediction models Uncertainty Estimation in Deep Learning with application to Spoken Language Assessment Calibrating Uncertainty Models for Steering Angle Estimation A review of uncertainty quantification in deep learning: Techniques, applications and challenges Mining Requirements From Closed-Loop Control Models TeLEx: Passive STL learning using only positive examples Learning task specifications from demonstrations Temporal logic inference for classification and prediction from data Online Learning of Temporal Logic Formulae for Signal Classification Abnormal data classification using time-frequency temporal logic Time robustness in mtl and expressivity in hybrid system falsification Robust Satisfaction of Temporal Logic over Real-Valued Signals Robust control for signal temporal logic specifications using discrete average space robustness Robustness of temporal logic specifications for continuous-time signals Specification mining and robust design under uncertainty: A stochastic temporal logic approach Automated requirements-based generation of test cases for product families Data-driven statistical learning of temporal logic properties," in Formal Modeling and Analysis of Timed Systems Temporal Logic Based Monitoring of Assisted Ventilation in Intensive Care Patients Interval Temporal Logic Decision Tree Learning Robust Pandemic Control Synthesis with Formal Specifications: A Case Study on COVID-19 Pandemic Advisory Temporal Logic Inference and Controller Design for Semiautonomous Robots Temporal Logics Optimal SVM parameter selection for non-separable and unbalanced datasets On optimization modulo theories, maxsmt and sorting networks νz -an optimizing SMT solver Bounded Model Checking Deep Dynamics Models for Learning Dexterous Manipulation Joint inference of reward machines and policies for reinforcement learning Graph Temporal Logic Inference for Classification and Identification For two given disjoint intervals, [a, a] and [b, b], we know that a ≤ a and b ≤ b. If a < b, then we define [a, a] < [b, b]; or if b < a, then [a, a] > [b, b] .For two interval trajectories, [ζ , ζ ] i with label l i = +1 and [ζ , ζ ]ĩ with label lĩ = −1, if there exists one time-step t j and one dimension k such that [ζ k j , ζ Given a labeled set of interval trajectoriesBy relying on Theorem 1, if all the pairs of interval trajectories [ζ , ζ ] i and [ζ , ζ ] i are separable, then a formula ϕ ii can be found that is strongly satisfied by interval trajectories [ζ , ζ ] i with the label l i = +1 and is strongly violated by interval trajectories [ζ , ζ ] i . This formula can be in the form ofThis formula can strongly classify the two sets of interval trajectories since ϕ is strongly satisfied by all [ζ , ζ ] i and strongly violated by all [ζ , ζ ] i . Algorithm 3 and Algorithm 4 present the incomplete procedures for the two baseline algorithms TLI-RS and TLI-RS-DT, respectively. The complete procedures would include the following first step: construct D from finitely many randomly sampled trajectories within the interval trajectories D unc . Algorithm 3 presents similarities with Algorithm 1 in its structure. We cover the key differences of Algorithm 3 here.We define propositional formulas Φ n ζ for each trajectories ζ that tracks the valuation of the STL formula encoded by Φ DAG n on ζ . These formulas are built using variables y ζ i,j , where i ∈ {1, . . . , n} and j ∈ {1, . . . , |ζ| − 1}, that corresponds to the value of V (ϕ i , ζ , j) (ϕ i is the STL formula rooted at Node i).We now define the constraint that ensure consistency with Algorithm 3: TLIAssign weights to soft constraints