Learning Linear Temporal Properties

We present two novel algorithms for learning formulas in Linear Temporal Logic (LTL) from examples. The first learning algorithm reduces the learning task to a series of satisfiability problems in propositional Boolean logic and produces a smallest LTL formula (in terms of the number of subformulas) that is consistent with the given data. Our second learning algorithm, on the other hand, combines the SAT-based learning algorithm with classical algorithms for learning decision trees. The result is a learning algorithm that scales to real-world scenarios with hundreds of examples, but can no longer guarantee to produce minimal consistent LTL formulas. We compare both learning algorithms and demonstrate their performance on a wide range of synthetic benchmarks. Additionally, we illustrate their usefulness on the task of understanding executions of a leader election protocol.


I. INTRODUCTION
Making sense of the observed behavior of complex systems is an important problem in practice. It arises, for instance, in debugging (especially in the context of distributed systems), reverse engineering (e.g., of malware and viruses), specification mining for formal verification, and modernization of legacy systems, to name but a few examples. However, understanding a system based on examples of its execution is clearly a challenging task that can quickly become overwhelming without proper tool support.
In this paper, we address this problem and develop learningbased techniques to help engineers understand the dynamic (i.e., temporal) behavior of complex systems. More precisely, we solve the problem of learning formulas in Linear Temporal Logic (LTL) [1], which are meant to distinguish between desirable and undesirable executions of a system (e.g., to explain the root-cause of a bug). The particular choice of LTL in this work is motivated by two observations: first, logical formulas often provide concise descriptions of the observed behavior and are relatively easy for humans to comprehend; second, LTL-together with Computational Tree Logic (CTL) [2]-is widely considered to be the de facto standard for specifying temporal properties and, hence, many engineers are familiar with its use.
The precise problem we are aiming at is the following: given a sample S consisting of two finite sets of positive and negative examples, learn an LTL formula ϕ that is consistent with S in the sense that all positive examples satisfy ϕ, whereas all negative examples violate ϕ. 1 To be as general and succinct as possible, we here consider examples to be infinite, ultimately periodic words (e.g., traces of a non-terminating system) and assume the standard syntax of LTL. However, our techniques can easily be adapted to the case of finite words and extend smoothly to arbitrary future-time temporal operators, such as "release", "weak until", and so on. We fix all necessary definitions and notations in Section II.
The main contribution of this work are two novel learning algorithms for LTL formulas from data, one based on SAT solving, the other on learning decision trees.
SAT-based learning algorithm: The idea of our first algorithm, presented in Section III, is to reduce the problem of learning an LTL formula to a series of satisfiability problems in propositional Boolean logic and to use highly-optimized SAT solvers to search for solutions. Inspired by ideas from bounded model checking [10], our learning algorithm produces a series of propositional formulas Φ S n for increasing values of n ∈ N \ {0} that depend on the sample S and have the following two properties: (1) Φ S n is satisfiable if and only if there exists an LTL formula of size n (i.e., with n subformulas) that classifies the examples correctly, and (2) a model of Φ S n contains sufficient information to construct such an LTL formula. By increasing the value of n until Φ S n becomes satisfiable, we obtain an effective algorithm that learns an LTL formula that is guaranteed to classify the examples correctly (given that the sample is non-contradictory).
By design, our SAT-based learning algorithm has three distinguished features, which we believe are essential in practice. First, our algorithm learns LTL formulas of minimal size (i.e., with the minimal number of subformulas). As we seek to learn formulas to be read by humans, the size of the learned formula is a crucial metric since larger formulas are generally harder to understand than smaller ones. Second, once an LTL formula has been learned, our algorithm can be queried for further, distinct formulas that are consistent with the sample. We believe that this feature is important in practice as it allows generating multiple explanations for the observed data. Third, our algorithm does not rely on an a priori given set of templates, which is in stark contrast to existing work on learning temporal properties (e.g., Bombara et al. [11]). To the best of our knowledge, our SAT-based algorithm is in fact the first learning algorithm that is not restricted to a fixed class of templates. However, restrictions to the shape of LTL formulas (e.g., to the popular GR(1)-fragment of LTL [12]) can easily be encoded if desired.
Learning algorithm based on decision trees: Our second learning algorithm, which we present in Section IV, trades in the guarantee of finding minimal solutions in order to attain better scalability. The key idea is to perform the learning in two phases. In the first phase, we run the SAT-based learning algorithm described above on various subsets of the examples. This results in a (small) number of LTL formulas, named "LTL primitives", that classify at least these subsets correctly.
In the second phase we use a standard learning algorithm for decision trees [13] to learn a Boolean combination of these LTL primitives that classifies the whole set of examples correctly, though it might not be minimal. Note, however, that we need to carefully choose the subsets of examples such that the resulting LTL primitives (a) separate all pairs of positive and negative examples and (b) are general enough to permit "small" decision trees. We have experimented with numerous strategies to select subsets, but in this paper we present only the two that performed best. A well known advantage of decision trees is that they are simple to comprehend due to their rule-based structure.
In Section V, we evaluate the performance of both learning algorithms on a wide range of synthetic benchmarks that reflect typical patterns of LTL formulas used in practice. Additionally, we illustrate their usefulness for understanding causes of inconsistencies in the leader election used by Zookeeper's atomic broadcast protocol [14].

Related Work
Learning of temporal properties from examples has recently attracted increasing interest, especially in the area of Signal Temporal Logic (STL) [16] and parametric STL [17]. Examples include the work by Asarin et al. [17], Kong et al. [18], [19], Vaidyanathan et al. [20], and Bartocci, Bortolussi, and Sanguinetti [21]. In contrast to our SAT-based learning algorithm, however, all of these techniques either rely on usergiven templates or can only learn formulas from very restricted syntactic fragments. Various techniques for mining LTL specifications [22], [23] and CTL specifications [24] exist as well, but these also rely on templates or restrict the class of formulas severely. To the best of our knowledge, our SAT-based algorithm is in fact the first that is capable of learning unrestricted LTL formulas without relying on usergiven templates. Nonetheless, expert knowledge in form of constraints on the syntax can easily be encoded if desired.
Our SAT-based learning algorithm is inspired by bounded model checking [10] and earlier work of the first author on learning (minimal) automata over finite words [7], [9]. However, since regular languages are strictly more expressive than LTL (the former being equivalent to monadic secondorder logic [25], while the latter being equivalent to fist-order logic [26]), automata learning techniques-including active learning algorithms [27], [28] that operate in Angluin's active learning framework [29]-are not immediately applicable. However, lifting the methods developed in this work to an active learning setup, without a detour via automata, is part of our plans for future work.
Using decision trees to learn Signal Temporal Logic (STL) formulas has been explored by Bombara et al. [11], whose main contribution is an adaptation of the classical impurity measure to account for STL formulas. However, this work still requires user-defined STL primitives to be provided, which serve as the features for the decision tree learning algorithm. By contrast, our technique uses the SAT-based learning algorithm to infer LTL primitives fully automatically.
Learning of logical formulas has also been studied in the context of probably approximately correct learning (PAC) [3]. Grohe and Ritzert [30], for instance, considered learning of first-order definable concepts over structures of small degree. Subsequently, Grohe, Löding, and Ritzert [31] studied the learning of hypotheses definable using monadic second order logic on strings. Due to the fundamental differences between PAC learning and the learning model considered here (one being approximate and the other being exact), their techniques cannot easily be applied.

II. PRELIMINARIES
In this section, we set up definitions and notations used throughout the paper.
Finite and Infinite Words: An alphabet Σ is a nonempty, finite set. The elements of this set are called symbols.
A finite word over an alphabet Σ is a sequence u = a 0 . . . a n of symbols a i ∈ Σ, i ∈ {0, . . . , n}. The empty sequence is called empty word and written as ε. The length of a finite word u is denoted by |u|, where |ε| = 0. Moreover, Σ * denotes the set of all finite words over the alphabet Σ, while Σ + = Σ * \{ε} is the set of all non-empty words.
An infinite word over Σ is an infinite sequence α = a 0 a 1 . . . of symbols a i ∈ Σ, i ∈ N. We denote the i-th symbol of an infinite word α by α(i) and the infinite suffix starting at position j by α[j, ∞). Given u ∈ Σ + , the infinite word u ω = uu . . . ∈ Σ ω is the infinite repetition of u. An infinite word α is called ultimately periodic if it is of the form α = uv ω for a u ∈ Σ * and v ∈ Σ + . Finally, Σ ω denotes the set of all infinite words over the alphabet Σ.
Propositional Boolean Logic: Let Var be a set of propositional variables, which take Boolean values from B = {0, 1} (0 representing false and 1 representing true). Formulas in propositional (Boolean) logic-which we denote by capital Greek letters-are inductively constructed as follows: • each x ∈ Var is a propositional formula; and • if Ψ and Φ are propositional formulas, so are ¬Ψ and Ψ ∨ Φ. Moreover, we add syntactic sugar and allow the formulas true, false, Ψ ∧ Φ, Ψ ⇒ Φ, and Ψ ⇔ Φ, which are defined as usual.
A propositional valuation is a mapping v : Var → B, which maps propositional variables to Boolean values. The semantics of propositional logic is given by a satisfaction relation |= that is inductively defined as follows: v |= x if and only if v(x) = 1, v |= ¬Ψ if and only if v |= Ψ, and v |= Ψ ∨ Φ if and only if v |= Ψ or v |= Φ. In the case that v |= Φ, we say that v satisfies Φ and call it a model of Φ. A propositional formula Φ is satisfiable if there exists a model v of Φ. The size of a formula is the number of its subformulas (as defined in the usual way).
The satisfiability problem of propositional logic is the problem to decide whether a given formula is satisfiable. Although this problem is well-known to be NP-complete [32], modern SAT solvers implement optimized decision procedures that can check satisfiability of formulas with millions of variables [33]. Moreover, SAT solvers also return a model if the input-formula is satisfiable.
Linear Temporal Logic: Linear Temporal Logic (LTL) [1] is an extension of propositional Boolean logic with modalities that allow expressing temporal properties. Starting with a finite, nonempty set P of atomic propositions, formulas in LTLwhich we denote by small Greek letters-are inductively defined as follows: • each atomic proposition p ∈ P is an LTL formula; • if ψ and ϕ are LTL formulas, so are ¬ψ, ψ ∨ ϕ, X ψ ("next"), and ψ U ϕ ("until"). Again, we add syntactic sugar and allow the formulas true := p ∨ ¬p for some p ∈ P, false := ¬true, as well as ψ ∧ ϕ and ψ → ϕ, which are defined as usual. Moreover, we allow the additional temporal formulas F ψ := true U ψ ("finally") and G ψ := ¬ F ¬ψ ("globally"). The size of an LTL formula ϕ, which we denote by |ϕ|, is the number of its subformulas. Finally, let C = {∧, ∨, ¬, →, F, G, U, X} be the set of LTL operators.
LTL formulas are interpreted over infinite words α ∈ (2 P ) ω , though there exist various semantics for LTL over finite words and our techniques smoothly extend to these situations. For the sake of a simpler presentation, we define the semantics of LTL in a slightly non-standard way by means of a valuation function V . This functions maps pairs of LTL formulas and infinite words to Boolean values and is inductively defined as follows: Our SAT-Based learning algorithm relies on a canonical syntactic representation of LTL formulas, which we call syntax DAGs. A syntax DAG is essentially a syntax tree (i.e., the unique tree labeled with atomic propositions as well as Boolean and temporal operators that is derived from the inductive definition of an LTL formula) in which common subformulas are shared. This sharing turns the syntax tree into a directed, acyclic graph (DAG), whose number of nodes coincides with the number of subformulas of the represented LTL formula. As an example, Figure 1b (on Page 4) depicts the (unique) syntax DAG of the formula (p U G q) ∨ (F G q), in which the subformula G q is shared; the corresponding syntax tree is depicted in Figure 1a. Note that syntactically distinct formulas have different (i.e., non-isomorphic) syntax DAGs.
Samples and Consistency: Throughout this paper, we assume that the data we learn from is given as two (potentially empty) finite, disjoint sets P, N ⊂ (2 P ) ω of ultimately periodic words. The words in P are interpreted as positive examples, while the words in N are interpreted as negative examples. We call the pair S = (P, N ) a sample. Since we want to work with the ultimately periodic words in a sample algorithmically, we assume that they are stored as pairs (u, v) of finite words u ∈ (2 P ) * and v ∈ (2 P ) + , which can be accessed individually. To measure the complexity of a sample, we define its size to be |S| = uv ω ∈P ∪N |u| + |v|.
Given an LTL formula ϕ and a sample S = (P, N ), both over a set P of atomic propositions, we call ϕ consistent with S if V (ϕ, uv ω ) = 1 for each uv ω ∈ P (i.e., all positive examples satisfy ϕ) and V (ϕ, uv ω ) = 0 for each uv ω ∈ N (i.e., all negative examples do not satisfy ϕ); in this case, we also say that ϕ separates P and N . We call ϕ minimally consistent with S if ϕ is consistent with S and no consistent LTL formula of smaller size exists.

III. A SAT-BASED LEARNING ALGORITHM
The fundamental task we solve in this section is: "given a sample S, compute an LTL formula of minimal size that is consistent with S". We call this task passive learning of LTL formulas-as opposed to active learning [29] where the learning algorithm is permitted to actively query for additional data. Note that this problem can have more than one solution as there can be multiple, non-equivalent LTL formulas that are minimally consistent with a given sample.
Before we explain our learning algorithm in detail, let us briefly comment on the minimality requirement in the definition above. On the one hand, we observe that the problem becomes simple if no restriction on the size is imposed: for α ∈ P and β ∈ N , construct a formula ϕ α,β with V (ϕ α,β , α) = 1 and V (ϕ α,β , β) = 0 that describes the first symbol where α and β differ using a sequence of X-operators and an appropriate propositional formula; then, α∈P β∈N ϕ α,β is consistent with S since we assume P and N to be disjoint. However, simply characterizing all differences between positive and negative examples is clearly overfitting the sample and, hence, arguably of little help in practice. On the other hand, we believe that small formulas are easier for humans to comprehend than large ones, which justifies spending effort on learning a smallest formula. However, we do not impose any preference amongst minimal consistent formulas (which is an interesting topic for future work).
Let us now turn to describing our learning algorithm. Its underlying idea is to reduce the construction of a minimally consistent LTL formula to a satisfiability problem in propositional logic and use a highly-optimized SAT solver to search for solutions. More precisely, given a sample S and a natural number n ∈ N \ {0}, we construct a propositional formula Φ S n of size polynomial in n and |S| that has the following two properties: 1) Φ S n is satisfiable if and only if there exists an LTL formula of size n that is consistent with S; and 2) if v is a model of Φ S n , then v contains sufficient information to construct an LTL formula ψ v of size n that is consistent with S. By increasing the value of n by one and extracting an LTL formula ψ v from a model v of Φ S n as soon as it becomes satisfiable (indeed, any model is sufficient), we obtain an effective algorithm that learns an LTL formula of minimal size that is consistent with S. This idea is shown in pseudo code as Algorithm 1. In fact, the existence of a trivial solution for the passive LTL learning task (as sketched at the beginning of this section) shows that Algorithm 1 is guaranteed to terminate, and the size of this solution provides an upper bound on the value of n. Construct and solve Φ S n ; 5 until Φ S n is satisfiable, say with model v; 6 Construct and return ψ v ; The key idea of the formula Φ S n is to encode the syntax DAG of an (unknown) LTL formula ϕ ⋆ with n subformulas and then constrain the variables of Φ S n such that ϕ ⋆ is consistent with the sample S. To simplify our encoding, we assign to each node of this syntax DAG a unique identifier i ∈ {1, . . . , n} such that (a) the identifier of the root is n and (b) if the identifier of an inner node is i, then the identifiers of its children are less than i. Note that such a numbering scheme is not unique for a given syntax DAG, but it entails that the root always has identifier n and the node with identifier 1 is always labeled with an atomic proposition. We refer the reader to Figures 1b and 1c for an example.
We encode a syntax DAG using three types of propositional variables: . . , n} and λ ∈ P ∪ C; • l i,j where i ∈ {2, . . . , n} and j ∈ {1, . . . , i − 1}; and • r i,j where i ∈ {2, . . . , n} and j ∈ {1, . . . , i − 1}. Intuitively, the variables x i,λ encode a labeling of the syntax DAG in the sense that if a variable x i,λ is set to true, then node i is labeled with λ (recall that each node is labeled with either an atomic proposition from P or an operator from C). The variables l i,j and r i,j , on the other hand, encode the structure of the syntax DAG (i.e., the left and/or right child of inner nodes): if variable l i,j (r i,j ) is set to true, then j is the identifier of the left (right) child of node i. By convention, we ignore the variables r i,j if node i of the syntax DAG is labeled with an unary operator; similarly, we ignore both l i,j and r i,j if node i is labeled with an atomic proposition. Note that in the case of l i,j and r i,j , the identifier i ranges from 2 to n because node 1 is always labeled with an atomic proposition and, hence, cannot have children. Moreover, j ranges from 1 to i − 1 to reflect the fact that identifier of children have to be smaller than the identifier of the current node.
To enforce that the variables x i,λ , l i,j , and r i,j in fact encode a syntax DAG, we impose the constraints listed in Table I. Formula (1) ensures that each node is labeled with exactly one label. Similarly, Formulas (2) and (3) enforce that each node (except for node 1) has exactly one left and exactly one right child (although we ignore certain children if the node represents an unary operator or an atomic predicate). Finally, Formula (4) makes sure that node 1 is labeled with an atomic proposition.
Let Φ DAG n now be the conjunction of Formulas (1) to (4). Then, one can construct a syntax DAG from a model v of Φ DAG n in a straightforward manner: simply label node i with the unique label λ such that v(x i,λ ) = 1, designate node n as the root, and arrange the nodes of the DAG as uniquely described by v(l i,j ) and v(r i,j ). Moreover, we can easily derive an LTL formula from this syntax DAG, which we denote by ψ v . Note, however, that ψ v is not yet related to the sample S and, thus, might or might not be consistent with it.
To enforce that ψ v is indeed consistent with S, we now constrain the variables x i,λ , l i,j , and r i,j further. More precisely, we add for each ultimately periodic word uv ω in S a propositional formula Φ u,v n that tracks the valuation of the LTL formula encoded by Φ DAG n (and all its subformulas) on uv ω . The observation that enables us to do this is the following.
Intuitively, Observation 1 states that the suffixes of a word uv ω eventually repeat periodically. As a consequence, the valuation of an LTL formula on a word uv ω can be determined based only on the finite prefix uv (recall that the semantics of temporal operators only depend on the suffixes of a word). To illustrate this claim, consider the LTL formula X ϕ and assume that we want to determine the valuation V (X ϕ, uv ω [|uv| − 1, ∞)) (i.e., X ϕ is evaluated at the end of the prefix uv). Then, Observation 1 permits us to compute this valuation based on V (ϕ, uv ω [|u|, ∞)), as opposed to the original semantics of the X-operator, which recurs to V (ϕ, uv ω [|uv|, ∞)) (i.e., the valuation at the next position). Note that similar, though more involved ideas can be applied to all other temporal operators.
Each formula Φ u,v n is built over an auxiliary set of propositional variables y u,v i,t where i ∈ {1, . . . , n} is a node in the syntax DAG and t ∈ {0, . . . , |uv| − 1} is a position in the finite word uv. The meaning of these variables is that the value of y u,v i,t corresponds to the valuation V (ϕ i , uv ω [t, ∞)) of the LTL subformula ϕ i that is rooted at node i. Note that the set of variables for two distinct words from the sample must be disjoint.
To obtain this desired meaning of the variables y u,v i,t , we impose the constraints listed in Table II, which are inspired by bounded model checking [10]. Formula (5) implements the LTL semantics of atomic propositions and ensures that if node i is labeled with p ∈ P, then y u,v i,t is set to 1 if and only if p ∈ uv(t). Next, Formulas (6) and (7) implement the semantics of negation and disjunction, respectively: if node i is labeled with ¬ and node j is its left child, then y u,v i,t is the negation of y u,v j,t ; on the other hand, if node i is labeled with ∨, node j is its left child, and node j ′ is its right child, then y u,v i,t is the disjunction of y u,v j,t and y u,v j ′ ,t . Moreover, Formula (8) implements the semantics of the X-operator, following the idea of "returning to the beginning of the periodic part v" as sketched above. Finally, Formula (9) implements the semantics of the U-operator. More precisely, the first conjunction in the consequent covers the positions t ∈ {0, . . . , |u| − 1} in the initial part u, while the second conjunct covers the positions t ∈ {|u|, . . . , |uv| − 1} in the periodic part v. Thereby, the second conjunct relies on an auxiliary set t u,v t ′ defined by which contains all positions in v "between t and t ′ ". To avoid cluttering this section too much, we have omitted the description of the missing operators ∧, →, F, G and the 1<i≤n 1≤j<i constants true and false, which are implemented analogously. Moreover, our SAT encoding is extensible, and additional LTL operators such as weak until or weak and strong release can easily be added. For each uv ω ∈ P ∪ N , let Φ u,v n now be the conjunction of Formulas (5) to (9). Then, we define Note that the subformula Φ u,v n ∧y u,v n,0 makes sure that uv ω ∈ P satisfies the prospective LTL formula (more concretely, uv ω starting from position 0 satisfies the LTL formula at the root of the syntax DAG), while Φ u,v n ∧¬y u,v n,0 ensures that uv ω ∈ N does not satisfy it.
To prove the correctness of our learning algorithm, we first establish that the formula Φ S n has in fact the desired properties. Lemma 1: Let S = (P, N ) be a sample, n ∈ N\{0}, and Φ S n the propositional formula defined above. Then, the following holds: 1) If an LTL formula of size n that is consistent with S exists, then the propositional formula Φ S n is satisfiable. 2) If v |= Φ S n , then ψ v is an LTL formula of size n that is consistent with S. Termination and correctness of Algorithm 1 then follow from Lemma 1.
Theorem 1: Given a sample S, Algorithm 1 terminates eventually and outputs an LTL formula of minimal size that is consistent with S. Proof: Since there exists a consistent LTL formula for every non-contradictory sample, Part 1 of Lemma 1 guarantees that Algorithm 1 terminates. Moreover, Part 2 ensures that the output is indeed an LTL formula that is consistent with S. Since n is increased by one in every iteration of the loop until Φ S n becomes satisfiable, the output of Algorithm 1 is a consistent LTL formula of minimal size.
It is important to emphasize that the size of Φ S n and, hence, the performance of Algorithm 1 depends on the size of a sample S = (P, N ), as summarized next.
Remark 1: The formula Φ S n ranges over O(n 2 + n|S|) variables and is of size O(n 2 + n 3 uv ω ∈P ∪N |uv| 3 ). Finally. we conclude this section with a remark on incorporating expert knowledge into the learning process.
Remark 2: By adding constraints to the variables x i,λ , l i,j , and r i,j , one can easily incorporate expert knowledge (e.g., syntactic templates) into the learning process.

IV. A DECISION TREE BASED LEARNING ALGORITHM
The SAT-based algorithm described in Section III is an elegant, out-of-the-box way to discover minimal LTL formulas describing a sample. Even though it scales well beyond toy examples, its running time seems too prohibitive for real-world examples (as discussed in Section V). That is why we now present a learning algorithm based on a combination of SAT solving and decision tree learning.
Our second algorithm proceeds in two phases, outlined in Algorithm 2. In the first phase, we run Algorithm 1 on small subsets of P and N . This is repeated until we obtain a set Π of LTL formulas (we call them LTL primitives) that separate all pairs of words from P and N . In the second phase, formulas from Π are used as features for a standard decision tree learning algorithm [13]. The resulting decision tree is a Boolean combination of LTL formulas ϕ i ∈ Π that is consistent with the sample.

Algorithm 2: Learning algorithm based on decision trees
Input: a sample S 1 Run Algorithm 1 on small subsets of P and N to construct a set Π = {ϕ 1 , . . . , ϕ n } of LTL formulas such that for each pair u 1 v ω 1 ∈ P and u 2 v ω 2 ∈ N there exists a ϕ i ∈ Π with V (ϕ i , u 1 v ω 1 ) = 1 and V (ϕ i , u 2 v ω 2 ) = 0; 2 Learn a decision tree t with LTL primitives from Π as features and return the resulting Boolean combination ψ t of LTL primitives (which is consistent with S); Note that this relaxes the problem addressed in Section III: we can no longer guarantee finding a formula of minimal size. However, decision trees are among the structures that are the easiest to interpret by end-users. That makes them suitable for our use-case, and the minimality of formulas is replaced by structural simplicity of decision trees.
Learning Decision Trees: We assume familiarity with decision tree learning and refer the reader to a standard textbook for further details [5]. As illustrated in Figure 3, the decision trees we seek to learn are tree-shaped structures whose inner nodes are labeled with LTL formulas from Π and whose leaves are labeled with either true or false. The LTL formula represented by such a tree t is given by ψ t := ρ∈P ϕ∈ρ ϕ where P is the set of all paths from the root to a leaf labeled with true and ϕ ∈ ρ denotes that ϕ occurs on ρ (negated if the path follows a dashed edge).
To learn a decision tree over LTL primitives, we perform a preprocessing step and modify the sample as follows. For each word uv ω ∈ P ∪N , we use the LTL primitives as features and create a Boolean vector of size |Π| with the i-th entry set to V (ϕ i , uv ω ); this vector is then labeled with true if uv ω ∈ P or with false if uv ω ∈ N . In the second step, we apply a standard learning algorithm for decision trees to this modified sample (we used Gini impurity [34] as split heuristic in our experiments). Since we are interested in a tree that classifies our sample correctly, we disable heuristics such as pruning.
Obtaining LTL Primitives: Meaningful features are essential for a successful classification using decision trees. In our algorithm, features are generated from the set of LTL primitives Π. We used two different strategies, called Strategy α and Strategy β, for obtaining Π.
Strategy α iteratively chooses subsets P ′ ⊂ P and N ′ ⊂ N of size k according to probability distributions prob P and prob N on P and N , respectively. After a formula ϕ separating P ′ and N ′ is found using Algorithm 1 and added to Π, prob P and prob N are updated to increase the likelihood of any word that is not yet classified correctly by any of the ϕ ∈ Π to be selected. This process is repeated until all pairs of positive and negative examples are separated by some LTL primitive or restarted after a user-given number of iterations. Although this strategy is, in general, not guaranteed to terminate due to its probabilistic nature, it always did in our experiments.
Strategy β computes LTL primitives in a more aggressive way. Starting with the set S = P × N , it uniformly at random selects k pairs from S and uses Algorithm 1 to compute an LTL primitive ϕ that separates those pairs. Then, it removes all pairs separated by ϕ from S and repeats the process until S becomes empty (i.e., all pairs of examples are separated).
We refer to the extended version of this paper [35] for a detailed explanation of both strategies.
Correctness: The correctness of Algorithm 2 is formalized below.
Theorem 2: Given a sample S, Algorithm 2 learns a (not necessarily minimal) formula ψ t that is consistent with S. Theorem 2 follows from the fact that Step 1 of Algorithm 2 constructs a set of LTL primitives that allows separating any pair of positive and negative examples. Once such a set is constructed, any decision tree learner produces a decision tree t that is guaranteed to classify the examples correctly. The resulting LTL formula ψ t , hence, is consistent with S.

V. EVALUATION
In this section, we answer questions that arise naturally: how performant is Algorithm 1 and what is the performance gain of Algorithm 2. Furthermore, what is the complexity of the learned decision trees in terms of the number of decision nodes, and, finally, how do different parameters influence the performance of Algorithm 2. After answering these questions with experiments performed on synthetic data, we demonstrate the usefulness of our algorithms for understanding executions of a leader-election algorithm. We implemented both learning algorithms in a Python tool 2 using Microsoft Z3 [36]. All experiments were conducted on Debian machines with Intel Xeon E7-8857 CPUs at 3 GHz, using up to 5 GB of RAM.
Performance on Synthetic Data: To simulate real-world use-cases, we generated samples based on common LTL patterns [37], which are shown in Table III. Starting from a pattern formula ψ, we generated sets of random words and separated them into P and N depending on whether they are a model of ψ or not. Thereby, we fixed |u| + |v| = 10 for all words in the sample and added noise in form of one additional atomic proposition that is not constrained by the pattern formula. The size of the generated samples ranges between 50 and 5000. In total, we generated 192 samples. Figure 2 compares the running times of Algorithm 1 and Algorithm 2 (using Strategy α and k = 3) on samples of varying sizes. (So as not to clutter the presentation too much, we selected four LTL patterns that showed a typical behavior of our learning algorithms. The complete results are available in the technical report [35].) Overall, Algorithm 1 produces minimal formulas consistent with a sample. It does so even for samples of considerable size, but if the sample size grows beyond 2000 (varies over samples), the SAT-based learner (Algorithm 1) frequently times out. When Algorithm 2 (using decision tree learning) is applied to these samples-as shown on the right-hand-side of Figure 2-none of the computations timed out and the running times significantly improved.
What kind of trees does Algorithm 2 produce? An example output of the algorithm is shown in Figure 3. Moreover, as Table IV illustrates, Algorithm 2 learns small trees, often with less than five inner nodes. Upon closer inspection, we noticed that it often happens that one of the LTL primitives was the specified formula itself. This suggests that small subsets already characterize our samples completely.
To be able to compare decision trees to the formulas learned by Algorithm 2, we measure the size of a tree t in terms of the size of the formula ψ t this tree encodes. In our experiments, the formulas learned by Algorithm 2 were on average 1.41 times larger than those learned by Algorithm 1. However, there are outlier trees that are four times bigger than the one learned by Algorithm 1. Nonetheless, about 70 % are of the same size. Even for the outliers, as emphasized previously, the 2 Our tool is publicly available at https://github.com/gergia/samples2LTL.
false If a node evaluates to true, the outgoing full edge should be followed (and the dashed edge otherwise). The tree on the left represents the formula readability does not degrade completely because the rule-based structure of decision trees is known to be easily understandable by humans. Note that the runtime and size of decision trees depends on the parameters of Algorithm 2, which we discuss next.
Tuning the Decision Tree-Based Algorithm: As described in Section IV, Algorithm 2 can be tuned by various parameters (sampling strategy for obtaining LTL primitives, size of sample subsets, probability increase rate, and number of repetitions inside a single sampling). In this subsection, we explore how those parameters affect the performance of the algorithm.  Table IV shows the performance of Algorithm 2 for different parameters, averaged over all 192 benchmarks. As the table indicates, the less aggressive method of separating sets, Strategy α, performs better. It seems that if the subset sizes are increased, or Strategy β is used, the sampled subsets already describe the specified formula completely. Finally, we chose Strategy α and k = 3 to be our default parameters. Varying the probability decrease rate and the number of repetitions inside a single sampling did not influence the performance much.
Explaining Executions of a Leader Election Protocol: A number of methods exist for finding errors or reproducing certain behavior in distributed systems through systematic testing [38], [39]. However, finding an execution and a corresponding schedule is only a first step towards understanding an issue. In the following, we demonstrate how to apply our technique in order to obtain a minimal LTL description of a specific inconsistency in a leader election protocol.
The leader election protocol we consider is the Fast Leader Election algorithm [14], [40] used by Apache Zookeeper. In this protocol, every node has a unique ID and initially tries to become the leader. To this end, every node sends messages to all other nodes proclaiming its leadership. Upon receiving a message by an aspirant leader with a higher ID, a node gives up its claim and acknowledges its support for the aspirant. If a node learns that an aspirant node has a support of a majority of all nodes, it commits (after waiting for a constant time for new messages) to the aspirant as the leader. Once committed, the node never again changes its decision and informs any other node of its commitment (one example is the message depicted by the dotted arrow in Figure 5). If a node has not committed and learns about another node that has committed, it commits to the same leader.  Figure 4 shows an example of a successful leader election with three nodes in an UML-style message sequence chart. The messages exchanged between nodes are proposing the leader i (P i ) and node j acknowledging the claim of a leader (A j ). The arrows indicate exchanged messages and imply a precedence of events. Note that not all messages are shown in the figures, but only the ones important for understanding the protocol.
In Figure 4 all the nodes have committed to the same leader. On the other hand, Figure 5 shows a schedule that ends up in an inconsistent state where nodes committed to different leaders. This schedule was discovered by the PCTCP algorithm [41], which systematically explores the space of possible executions of distributed algorithms. The situation in Figure 5 is caused by the asynchronous communication: for performance reasons, nodes commit as quickly as possible and then discard any messages, which otherwise would have changed their commitment (indicated as a dashed line in Figure 5). Note, however, that this is not a bug in Zookeeper's broadcast algorithm, as a leader without a quorum will not be allowed to perform any action in the later phase.
To better understand how this inconsistent state arises, our goal is to generate an LTL formula that describes the difference between the schedules in Figures 4 and 5. To this end, we constructed a sample by generating 20 linearizations of the schedule from Figure 4 and 20 linearizations of the schedule from Figure 5. Since we seek an explanation for the inconsistent behavior, the former (with consistent outcomes) correspond to negative examples (set N ), and the latter (with inconsistent outcomes) correspond to positive examples (set P ). The set of atomic propositions used to construct the examples contains twelve elements: recv(i, j) for i, j ∈ {1, 2, 3} (meaning that node j received a message from node i) and comm(i) for i ∈ {1, 2, 3} (meaning that node i committed to a leader). 3 Finally, we ran Algorithm 1 on this sample. The result was the formula ¬recv(2, 1) U comm (1). Intuitively, node 1 did not receive a message from node 2 before it committed to a leader. That is exactly the difference between the schedules in Figures 4 and 5. Also, it hints at a specific reason for the inconsistency in Figure 5, thus potentially helping the engineers improve the system. Note, however, that this experiment still required a significant amount of manual effort. In order to apply the technique in practice, more automation is needed.
Summary: Algorithm 2 significantly improves upon the performance of Algorithm 1, though with a small increase in the size of the formula. The original motivation of getting readable explanations for the behavior of a system is preserved due to the fact that decision-trees are easy to comprehend. Algorithm 2 works the best using Strategy α and subsets of size k = 3. Finally, our techniques are able to give interesting insight into real-world systems.

VI. CONCLUSION
We have presented two novel algorithms for learning LTL formulas from examples. Our first algorithm is based on SAT solving, while the second algorithm extends the first with techniques for learning decision trees. We have shown that both algorithms are able to learn LTL formulas for a comprehensive set of benchmarks that we have derived from common LTL patterns. Moreover, we have demonstrated how our methods can help understand distributed algorithms.
Interesting directions of future work include the integration of LTL past-time operators, lifting our techniques to an active learning setup [29], as well as the development of similar learning algorithms for CTL. Furthermore, we plan to investigate the use of maximum-margin classifiers, such as support vector machines. To this end, one needs to develop a notion of distance between temporal formulas and words, which is clearly of independent, theoretical interest as well.