--- title: "Learning Interpretable Models in the Property Specification Language" authors: - "Rajarshi Roy" - "Dana Fisman" - "Daniel Neider" doi: "10.24963/ijcai.2020/306" url: "https://ijcai.org/proceedings/2020/306" pdf: "https://ijcai.org/proceedings/2020/0306.pdf" venue: "Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence" year: 2020 pages: "2213-2219" track: "Main track" keywords: - "Machine Learning: Explainable Machine Learning" - "Machine Learning: Classification" - "Constraints and SAT: SAT: : Solvers and Applications" --- # Learning Interpretable Models in the Property Specification Language Rajarshi Roy, Dana Fisman, Daniel Neider *Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence*, pages 2213-2219. DOI: [10.24963/ijcai.2020/306](https://doi.org/10.24963/ijcai.2020/306) ## Abstract We address the problem of learning human-interpretable descriptions of a complex system from a finite set of positive and negative examples of its behavior. In contrast to most of the recent work in this area, which focuses on descriptions expressed in Linear Temporal Logic (LTL), we develop a learning algorithm for formulas in the IEEE standard temporal logic PSL (Property Specification Language). Our work is motivated by the fact that many natural properties, such as an event happening at every n-th point in time, cannot be expressed in LTL, whereas it is easy to express such properties in PSL. Moreover, formulas in PSL can be more succinct and easier to interpret (due to the use of regular expressions in PSL formulas) than formulas in LTL. The learning algorithm we designed, builds on top of an existing algorithm for learning LTL formulas. Roughly speaking, our algorithm reduces the learning task to a constraint satisfaction problem in propositional logic and then uses a SAT solver to search for a solution in an incremental fashion. We have implemented our algorithm and performed a comparative study between the proposed method and the existing LTL learning algorithm. Our results illustrate the effectiveness of the proposed approach to provide succinct human-interpretable descriptions from examples. ## Full text ## 1 Introduction Inferring an understandable and meaningful model of a complex system is an important problem in practice. It arises naturally in various areas, including debugging, reverse engineering (e.g., of malware and viruses), specification mining for formal verification, and the modernization of legacy software. Also, this topic clearly falls under explainable AI, as the challenge is to obtain an explainable model of the studied phenomena rather than a black box function implementing it. In recent years, inferring models in Linear Temporal Logic (LTL) has crystallized as one of the most promising approaches to help humans understand the (temporal) behavior of complex systems (see the related work for a detailed discussion). Originally developed by [Pnueli, 1977] in the context of reactive systems, LTL possesses not only a host of desirable theoretical properties (e.g., the ability to effectively translate formulas into finite automata) but also features a compact, variable-free syntax and an intuitive semantics. Specifically, these latter properties make it interesting as an interpretable description language with many applications in the area of artificial intelligence, including plan intent recognition, knowledge extraction, and reward function learning (see [Camacho and McIlraith, 2019] for details). ∗The last two authors are ordered alphabetically. However, one of the major downsides of LTL is its limited expressive power as compared to other temporal logics. As a consequence, many properties that arise naturally (e.g., an event happening at every n-th point in time) cannot be expressed in LTL. In fact, the class of properties that can be expressed in LTL corresponds exactly to that of star-free ω-languages [Wolper, 1981], which excludes-among othersall properties involving modulo counting. To overcome this serious limitation, the Property Specification Language (PSL) has been proposed, which has since been adopted by IEEE as an industrial standard for expressing temporal properties [IEEE Standards Association, 2010]. Although PSL is an extension of LTL and, hence, shares many of its beneficial properties, it differs from LTL in three aspects: 1. The expressive power of PSL exceeds that of LTL (it is as expressive as the full class of regular ω-languages [Armoni et al., 2002]). In particular, properties involving modulo counting-as mentioned above-can easily be expressed in PSL. 2. PSL integrates easy-to-understand regular expressions in its syntax. 3. When learning from the observed behavior of a system, models expressed in PSL can be arbitrarily more succinct than those expressed in LTL (see Proposition 1). We believe that these three properties make PSL particularly well-suited as an interpertable description language. The main contribution of this paper is an algorithm for learning models (i.e., formulas) in PSL. Following earlier work on learning formulas expressed in LTL [Neider and Gavran, 2018; Camacho and McIlraith, 2019], the precise learning problem our algorithm solves, is as follows: given a sample S consisting of two finite sets of positive and negative examples, learn a PSL formula ϕ that is consistent with S in the sense that all positive examples satisfy ϕ, whereas all negative examples violate ϕ. Although we cannot expect algorithms that learn consistent formulas to scale as well as statistical methods that allow for misclassifications (e.g., [Kim et al., 2019]), being able to learn an exact model describing the given data is essential in a multitude of applications, including few-shot learning, debugging of software systems, and many situations in which the observed data is without noise. We refer the reader to [Neider and Gavran, 2018; Camacho and McIlraith, 2019] for more examples where learning consistent formulas is important. To be as general and succinct as possible, we here assume examples to be infinite, ultimately periodic words (i.e., words of the form uvω , where u, v are a finite words and vω is the infinite repetition of v) and focus on the core fragment of PSL. However, our algorithm can easily be adapted to learn from finite words and extends smoothly to other future-time temporal operators of PSL. Our learning algorithm builds on top of the framework proposed by [Neider and Gavran, 2018] for learning formulas in LTL. Its key idea is to reduce the learning task to a series of constraint satisfaction problems in propositional logic and use a highly-optimized SAT solver to search for a solution. By design, our algorithm infers a minimal PSL formula that is consistent with the examples, which is a particularly valuable property in our setting: we seek to learn human-interpretable formulas and the size of the learned formula is a crucial metric for their interpretability (since larger formulas are generally harder to understand than smaller ones). As a result from the fact that PSL makes heavy use of regular expressions, we also obtain a learning algorithm for minimal regular expressions over finite words as a byproduct of our approach. Such a learning algorithm has many potential applications, for instance, in the field of natural language processing (e.g., see [Bartoli et al., 2014]). We empirically evaluate a prototype of our algorithm on benchmarks that reflect typical patterns of both LTL and PSL formulas used in practice. This evaluation shows that our algorithm can infer informative PSL formulas and that these formulas are often more succinct than pure LTL formulas learned from the same examples. Moreover, the runtime of our prototype is comparable to the state-of-the-art tool for learning LTL formulas by [Neider and Gavran, 2018]. RelatedWork. Learning of temporal properties has recently attracted increasing attention. The literature in this area can be broadly structured along three dimensions. The first dimension is the type of logic used to express models. Examples include learning of models expressed in Signal Temporal Logic [Kong et al., 2017], in Linear Temporal Logic [Neider and Gavran, 2018; Camacho and McIlraith, 2019; Riener, 2019], Computational Temporal Logic [Wasylkowski and Zeller, 2009] and several other temporal logics [Lamma et al., 2007; Chesani et al., 2009]. To the best of our knowledge, learning of models in PSL or an equally expressive logic has not yet been considered. The second dimension is whether the learning algorithm requires the user to provide templates. Examples of algorithms that require templates are the works of [Li et al., 2011] and [Lemieux et al., 2015], whereas the algorithms for LTL mentioned above do not require templates. Note, however, that providing templates is often a challenging task as it requires the user to have a good understanding of the data. By contrast, our algorithm can learn arbitrary formulas without any assistance from the user. The third dimension distinguishes between algorithms that learn an exact model and those that learn an approximate one. Like the majority of algorithms mentioned so far, the learning algorithm we devise in this paper is exact (i.e., it learns models that describe the data perfectly; due to our minimality constraint, however, these models generalize the data rather than overfit it). On the other hand, there also exists work that uses statistical methods to derive approximate formulas from noisy data [Kim et al., 2019]. This work is built upon the SAT-based learning algorithm by [Neider and Gavran, 2018]. In fact, constraint solving is often used in learning problems. The perhaps most prominent examples are passive automata learning [Heule and Verwer, 2010; Neider, 2012] and counterexample-guided inductive synthesis [Alur et al., 2018; Alur et al., 2015]. ## 2 Preliminaries We now introduce the concepts used throughout this paper. Alphabets and Words. An alphabet is a finite, nonempty set Σ, whose elements are called symbols. A finite word over Σ is a finite sequence u = a0 . . . an with ai ∈ Σ for i ∈ {0, . . . , n}. The empty word, denoted by ε, is the empty sequence, and the length |u| of a finite word u is the number of its symbols (note that |ε| = 0). Moreover, we denote the set of all words by Σ∗ and define Σ+ = Σ∗ \ {ε}. An infinite word over Σ is an infinite sequence α = a0a1 . . . with ai ∈ Σ for i ∈ N, and Σω denotes the set of all infinite words over Σ. Given u ∈ Σ+, the infinite word uω = uuu . . . is called the infinite repetition of u. An infinite word α is said to be ultimately periodic if it is of the form α = uvω for finite words u ∈ Σ∗ and v ∈ Σ+. Given an infinite word α = a0a1 . . . ∈ Σω and i, j ∈ N with i ≤ j, let α[i, j) = ai . . . aj-1 be the finite infix of α from position i up to (and excluding) position j (note that α[i, i) = ε). Moreover, let α[i] = ai be the symbol at position i and α[i,∞) = aiai+1 . . . the infinite suffix of α starting at position i. We define u[i, j) and u[i] analogously for finite words u ∈ Σ∗ and appropriate indices i, j. Propositional Logic. Let Var be a set of propositional variables, which take Boolean values from B = {0, 1}. Formulas in propositional logic-which we denote by capital Greek letters-are inductively constructed as follows: Additionally, we add syntactic sugar and allow the formulas tt (true), ff (false), Φ1 ∧Φ2, Φ1 →Φ2, and Φ1 ↔Φ2, which are defined as usual. An interpretation is a function v : Var → B, which assigns a Boolean value to each variable. The semantics of propositional logic is given in terms of a satisfaction relation |= that is inductively defined as follows: v |= x with x ∈ Var if and only if v(x) = 1; v |= ¬Φ if and only if v ̸|= Φ; and v |= Φ1 ∨ Φ2 if and only if v |= Φ1 or v |= Φ2. If v |= Φ, we say that v satisfies Φ and call it a model of Φ. Moreover, a formula Φ is satisfiable if there exists a model v of Φ. The problem of deciding whether a propositional formula is satisfiable is the prototypical NP-complete problem [Cook, 1971]. Despite this fact, modern SAT solvers implement highly-optimized decision procedures that can check the satisfiability of formulas with millions of variables [Balyo et al., 2017]. Moreover, virtually all SAT solvers return a model if the input-formula is satisfiable. Linear Temporal Logic. The logic LTL, short for Linear Temporal Logic [Pnueli, 1977], is an extension of propositional logic that enables reasoning about time. The main building blocks of LTL are so-called atomic propositions, which, intuitively, correspond to interesting properties about the system in consideration. Given a finite set P of atomic propositions, formulas in LTL-which we denote by small Greek letters-are inductively constructed as follows: In addition to the temporal operators X ("next") and U ("until"), we also allow the derived operators F ("finally"), defined by Fϕ := tt Uϕ, and "globally", defined by Gϕ := ¬F¬ϕ (note that our technique seamlessly extends to any future-time temporal operator, such as "release", "weak until", and so on). Analogous to propositional logic, we also allow the formulas tt, ff , ϕ∧ψ, ϕ→ψ, and ϕ↔ψ. Formulas in LTL are evaluated over infinite words α ∈ Σω with Σ = 2P (i.e., over infinite sequences of sets of atomic propositions, modeling which propositions hold true at which points in time). Similar to propositional logic, the semantics of LTL is defined in terms of a satisfaction relation |=, which formalizes when an infinite word α ∈ (2P )ω satisfies an LTL formula: α |= p if and only if p ∈ α[0]; α |= ¬ϕ if and only if α ̸|= ϕ; α |= ϕ1 ∨ ϕ2 if and only if α |= ϕ1 or α |= ϕ2; α |= Xϕ if and only if α[1,∞) |= ϕ; and α |= ϕ1 Uϕ2 if and only if there exists a j ∈ N such that α[j,∞) |= ϕ2 and α[i,∞) |= ϕ1 for each i ∈ {0, . . . , j - 1}. Note that the satisfaction of a formula, due to the temporal operators, depends on the satisfaction of its subformulas on (potentially different) infinite suffixes of α. It is well-known that LTL cannot express natural properties such as modulo counting. To alleviate this serious restriction, the Property Specification Language (PSL) has been developed (e.g., see [Eisner and Fisman, 2006]), which makes extensive use of regular expressions. The remainder of this section introduces regular expressions and PSL in detail. Regular Expressions. To simplify the definition of PSL, we define regular expressions in a slightly non-standard way. Firstly, we use propositional formulas rather than symbols of an alphabet as atomic expressions (e.g., for P = {p, q}, the formula p ∨ q represents the set {{p}, {q}, {p, q}} of symbols from Σ = 2P ), whereas p ∧ ¬q represents the singleton set {{p}}). Secondly, we take an operational view on regular expressions in terms of a matching relation rather than the classical view as generators of regular languages. Regular expressions are inductively constructed as follows, where the left-hand-side describes the construction of atomic expressions and the right-hand-side describes the construction of general regular expressions: As usual, the regular operator + stands for choice, ◦ stands for concatenation, and ∗ for finite repetition (Kleene star). As syntactic sugar, we also allow the Boolean operators ∧, →, and ↔ in atomic expressions. Let us first give a meaning to atomic expressions. To this end, we assign to each atomic expression ξ a set [[ξ]] ⊆ 2P of symbols in the following way: [[p]] = {A ∈ 2P | p ∈ A}; [[¬ξ]] = 2P \ [[ξ]]; and [[ξ1 ∨ ξ2]] = [[ξ1]] ∪ [[ξ2]]. To define the semantics of regular expressions, we introduce a matching relation ⊢, which formalizes when an infix u[i, j) of a finite word u ∈ (2P )∗ matches a regular expression. Formally, the matching relation is defined as follows: u[i, j) ⊢ ε if and only if j = i; u[i, j) ⊢ ξ if and only if j = i + 1 and u[i] ∈ [[ξ]]; u[i, j) ⊢ ρ1 + ρ2 if and only if u[i, j) ⊢ ρ1 or u[i, j) ⊢ ρ2; u[i, j) ⊢ ρ1 ◦ ρ2 if and only if there exists a k ∈ {i, . . . , j} such that u[i, k) ⊢ ρ1 and u[k, j) ⊢ ρ2; and u[i, j) ⊢ ρ∗ if and only if j = i or there exists a k ∈ {i + 1, . . . , j} such that u[i, k) ⊢ ρ and u[k, j) ⊢ ρ∗ . Note that this definition applies to finite infixes α[i, j) of infinite words α ∈ (2P )ω as well. Property Specification Language. In this paper, we consider the core fragment of the Property Specification Language [Eisner and Fisman, 2006], which we here abbreviate as PSL for the sake of brevity. This fragment extends LTL with a so-called triggers operator ρ ↦→ ϕ where ρ is a regular expression and ϕ is a PSL formula. Intuitively, a word α ∈ (2P )ω satisfies the PSL formula ρ ↦→ ϕ if ϕ holds every time the regular expression ρ matches on a finite prefix of α. To define the semantics of the triggers operator formally, we extend the satisfaction relation of LTL by α |= ρ ↦→ ϕ if and only if α[0, i) ⊢ ρ implies α[i-1,∞) |= ϕ for all i ∈ N\{0}. Finally, we define the size |ϕ| of a PSL formula ϕ to be the number of its unique subformulas and subexpressions. PSL is a popular specification language in industrial applications, having been standardized by IEEE [IEEE Standards Association, 2010]. It is as expressive as ω-regular languages [Armoni et al., 2002] (i.e., languages accepted by nondeterministic B¨uchi automata) and, hence, exceeds the expressive power of LTL [Wolper, 1981]. A simple property that cannot be expressed in LTL is that a proposition p holds at every second point in time, which can be expressed in PSL as (tt ◦ tt)∗ ↦→ p [Eisner and Fisman, 2018]. ## 3 The Learning Problem In this section, we formally define the learning problem studied in this paper. We assume the data to learn from is given as a pair S = (P,N) consisting of two finite, disjoint sets P, N ⊂ Σω of ultimately periodic words such that P ∩N = ∅. We call this pair a sample. Moreover, we say that a PSL formula ϕ is consistent with a sample S = (P, N) if α |= ϕ for each α ∈ P and α ̸|= ϕ for each α ∈ N. Having defined the setting, we can now state the learning task as "given a sample S, compute a PSL formula of minimal size that is consistent with S". Note that this definition asks to ## Algorithm 1: SAT-based learning algorithm for PSL ``` Input: A sample S 1 n← 0 2 repeat 3 n←n+1 4 Construct ΦSn and check its satisfiability 5 until ΦSn is satisfiable, say with model v 6 return ϕv ``` construct a PSL formula that is minimal among all consistent formulas. The motivation for this requirement is threefold. Firstly, we observe that the problem becomes simple without a restriction on the size: for α ∈ P and β ∈ N, one can easily construct a formula ϕα,β with α |= ϕα,β and β ̸|= ϕα,β, which describes the first symbol where α and β differ using a sequence of X-operators and an appropriate propositional formula; then, ∨α∈P ∧β∈N ϕα,β is trivially consistent with S. However, simply enumerating all differences of a sample is clearly of little help towards the goal of learning a descriptive model. Secondly, small formulas are easier for humans to interpret, which justifies spending effort on learning a formula that is as small as possible. Thirdly, small formulas tend to provide good generalization of the behavior represented by the sample and avoids the possibility of simply overfitting it. Before we explain our learning algorithm in detail, let us show that models expressed in PSL can be arbitrarily more succinct than those expressed in LTL, which follows from Theorem 4.1 of [Wolper, 1981]. Proposition 1. Let n ∈ N and Sn = (Pn,Nn) over P = {p} with Pn = {{p}2n+1 ∅{p}ω } and Nn = {{p}2n ∅{p}ω }. Then (p ◦ p)∗ ↦→ Xp is a PSL formula (of constant size) consistent with Sn, whereas every LTL formula that is consistent with Sn has size greater than 2n. ## 4 The Learning Algorithm The idea underlying our algorithm is to reduce the construction of a minimally consistent PSL formula to a constraint satisfaction problem in propositional logic and to use a highlyoptimized SAT solver to search for a solution. More precisely, given a sample S, we construct a series (ΦSn )n=1,2,... of propositional formulas that have the following properties: 1. there exists a PSL formula of size n ∈ N \ {0} that is consistent with S if and only if ΦSn is satisfiable; and 2. given a model v of ΦSn , we can extract a PSL formula ϕv of size n that is consistent with S. By incrementing n (starting from 1) until ΦSn becomes satisfiable, we obtain an effective learning algorithm for models expressed in PSL, as shown in Algorithm 1. Note that termination of this algorithm follows from the existence of a trivial solution (see Section 3). Moreover, its correctness follows from Properties 1 and 2 of ΦSn . Theorem 1. Given a sample S, Algorithm 1 terminates and outputs a minimal PSL formula that is consistent with S. Corollary 1. A simple modification of Algorithm 1 learns a minimal regular expression from (finite) sample of finite words. Figure 1: Different representations of the PSL formula (p ◦ q) ↦→ X q ![Image](https://ijcai.org/proceedings/2020/fulltext/306/image_000000_65d583642c2ac56efc68591f43ebd3882e0c9f5ee83d3df49c0cda715936958a.png) Roughly speaking, the formula ΦSn is the conjunction ΦSn := Φstr n ∧ Φcst n , where Φstr n encodes the structure of the prospective PSL formula and Φcst n enforces that the prospective PSL formula is consistent with the sample. In the remainder of this section, we describe both Φstr n and Φcst n in detail. Structural Constraints. The formula Φstr n relies on a canonical syntactic representation of PSL formulas, which we call syntax DAGs. A syntax DAG is essentially a syntax tree (i.e., the unique tree that is derived from the inductive definition of a PSL formula) in which common subformulas are merged. This merging results into a directed, acyclic graph (DAG), whose number of nodes coincides with the number of subformulas of the prospective PSL formula. Figures 1a and 1b illustrate syntax trees and syntax DAGs, respectively. To simplify our encoding, we assign a unique identifier k ∈ {1, . . . , n} to each node of a syntax DAG such that (a) the identifier of the root is n and (b) the identifier of an inner node is larger than the identifiers of its children (see Figure 1c). Note that this encoding entails that Node 1 is always a leaf, which is necessarily labeled with an atomic proposition. Let now ΛR = {¬, ∨, +, ◦, ∗ } ∪ P be the set of operators and atomic propositions that can appear in regular expressions and ΛP = ΛR ∪ {X, U, ↦→} be the set of all PSL operators and atomic propositions. Then, we can encode a syntax DAG using the following propositional variables: - xk,λ where k ∈ {1, . . . , n} and λ ∈ ΛP - lk,ℓ where k ∈ {2, . . . , n} and ℓ ∈ {1, . . . , k -1} - rk,ℓ where k ∈ {2, . . . , n} and ℓ ∈ {1, . . . , k - 1} Intuitively, the variables xk,λ encode the labeling of a syntax DAG in the sense that if xk,λ is set to true, then node k is labeled by λ. Similarly, the variables lk,ℓ and rk,ℓ encode the left and right child of node k, respectively. By convention, we ignore the variables rk,ℓ (resp. rk,ℓ and lk,ℓ) if node k is labeled with an unary operator (resp. an atomic proposition). To enforce that these variables in fact encode a syntax DAG, we first need to make sure that for each k ∈ {1, . . . , n} there exists precisely one λ ∈ ΛP such that xk,λ is set to true. This can be done with the following constraint: Similarly, we assert that for each k ∈ {1, . . . , n} there exists precisely one ℓ ∈ {1, . . . , k - 1} and one ℓ′ ∈ {1, . . . , k - 1} such that lk,ℓ and rk,ℓ′ is set to true, respectively. Next, we have to ensure that the labeling of the syntax DAG respects the type of the operators (e.g., children of a regular expression are also regular expressions). The constraint below exemplifies this for the concatenation operator ◦: We add analogous constraints for all other operators. Note that the constraint for the triggers operator is slightly different as it combines a regular expression and a PSL formula. It is left to enforce that Node 1 is always labeled with an atomic proposition. We do so using the constraint ∨p∈P x1,p. Finally, let Φstr n be the conjunction of all constraints discussed above. Then, one can construct a syntax DAG from a model v of Φstr n in a straightforwardmanner: label Node k with the unique λ ∈ ΛP such that v(xk,λ) = 1, designate Node n as the root, and arrange the nodes as described uniquely by v(lk,ℓ) and v(rk,ℓ). Subsequently, we can derive a PSL formula from this syntax DAG, which we denote by ϕv. To ensure that ϕv is consistent with S, we add further constraints (i.e., a formula Φcst n ), which we describe next. Constraints for Consistency. To construct the propositional formula Φcst n , we exploit a simple observation about PSL. Intuitively, Observation 1 states that there exists only a finite number of distinct infinite suffixes of a word uvω , which eventually repeat periodically. Since the semantics of PSL is defined in terms of the suffixes of a word, we can determine whether a word uvω satisfies a PSL formula based on its finite prefix uv alone. To illustrate this claim, consider the formula Xϕ and suppose that we want to determine whether uvω [|uv| - 1,∞) |= Xϕ holds (i.e., the satisfaction of Xϕ at the end of the prefix uv). Then, Observation 1 allows us to reduce this question to checking whether uvω [|u|,∞) |= ϕ holds, instead of the original semantics of the X-operator, which depends on whether uvω [|uv|,∞) |= ϕ is satisfied. For reasoning about matchings of regular expressions, however, it is not enough to just consider the prefix uv. For instance, consider the ultimately periodic word uvω = ∅{p}(∅)ω and the PSL formula ϕ := (tt ◦ tt)∗ ↦→ p (stating that p is true at every second position). By just considering the prefix uv = ∅{p}∅, it seems that uvω |= ϕ. However, unrolling the repeating part v = ∅ once more, resulting in the prefix uvv = ∅{p}∅∅, immediately shows that uvω ̸|= ϕ. Similar to Observation 1, the next lemma provides a bound b ∈ N on the number of unrollings required to gather enough information to determine the satisfaction of a triggers operator. This bound depends on the number n of nodes of the syntax DAG and the function Mu,v : N → N defined by where a%b is the remainder of the division a/b. Intuitively, Mu,v maps a position j in the word uvω to an appropriate position within the prefix uv. The lemma uses finite automata as representations of regular expressions to derive the bound. Lemma 1. Let uvω ∈ (2P )ω , ψ = ρ ↦→ ϕ with |ψ| = n, and b = 2n+1 . Then, uvω [i,∞) |= ψ if and only if uvω [i, j) ⊢ ρ implies uvω [Mu,v(j - 1),∞) |= ϕ for all j ≤ |u| + b|v|. Note an important property of Lemma 1: reasoning about regular expressions and the triggers operator ↦→ requires us to consider the prefix uvb , while the prefix uv is sufficient for reasoning about the remaining PSL operators. Towards the definition of the formula Φcst n , we construct for each ultimately periodic word uvω in S a propositional formula Φu,v n that tracks the satisfaction of the PSL formula encoded by Φcst n (and all its subformulas/subexpressions) on uvω . Each of these formulas is built over auxiliary variables: - yu,v i,k with 0 ≤ i < |uv| and k ∈ {1, . . . , n} - zu,v i,j,k with 0 ≤ i ≤ j ≤ |uvb |, b = 2n+1 as in Lemma 1, and k ∈ {1, . . . , n} The meaning of these variables is that yu,v i,k is set to true if and only if uvω [i,∞) satisfies the PSL formula rooted at Node k (if that node is labeled with a PSL operator); similarly, zu,v i,j,k is set to true if and only if uvω [i, j) matches the regular expression rooted at Node k (if that node is labeled with a regular expression operator). Note that we have to create both the variables yu,v i,k and zu,v i,j,k for each node since the "type" of a node is determined dynamically during SAT solving. It is left to enforce that the variables yu,v i,k and zu,v i,j,k have the desired meaning. For the Boolean and temporal operators (except the triggers operator), we reuse the constraints proposed by [Neider and Gavran, 2018]. For instance, the constraint for the atomic propositions is Intuitively, this constraint states that if Node k is labeled with the atomic proposition p ∈ P, then the variables yu,v i,k capture precisely the presence or absence of p in the k-th position of the prefix uv. Similarly, the constraint for the X-operator is which states that if Node k is labeled with X and its left child is Node ℓ, then the satisfaction of the formula rooted at Node k at time i (i.e., yu,v i,k ) equals the satisfaction of the subformula rooted at Node ℓ at time i+1 (i.e., yu,v i+1,ℓ ), except at time |uv|- 1, where it "wraps around" to time |u| (see Observation 1). The constraints for regular expressions follow the matching relation and refer to the variables zu,v i,j,k instead of yu,v i,k . Exemplarily, we present the constraints for the ◦-operator (constraints for the other regular operators are analogous): Figure 2: Comparison of Flie-PSL and LTL-Infer. Bubble size is ∝ to no. of benchmarks with the formula size. "TO" indicates timeouts. ![Image](https://ijcai.org/proceedings/2020/fulltext/306/image_000001_9d5ab0f8014ac04cea60a344e446f1f327a285d105d404255d0b565f733976b5.png) Finally, the constraint below captures the semantics of the triggers operator ↦→ by relating the variables yu,v i,k and zu,v i,j,k . As the final step, we define the formula Φcst n by which enforces that all positive words in S satisfy the prospective PSL formula (yu,v 0,n has to be true), while all negative words violate it (yu,v 0,n has to be false). ## 5 Evaluation We have implemented a prototype of our learning algorithm, named Flie-PSL 1 (Formal Language Inference Engine for PSL), which is written in Python and uses Z3 [de Moura and Bjørner, 2008] as SAT solver. Deviating slightly from Algorithm 1, we have implemented the following improvement: instead of using yu,v i,k and zu,v i,j,k for each node, we use the latter variables only for 0 ≤ m < n nodes and the former variables for the remaining n -m nodes (the constraints generated for these variables remain as in Section 4. This modification essentially limits the size of a regular expression in the final PSL formula to m. To obtain a complete algorithm, we iterate over all valid values for m before increasing n. To assess the performance of our prototype, we have compared it to the LTL learning algorithm by [Neider and Gavran, 2018], which we call LTL-Infer for brevity. To make this comparison as fair as possible, we have used two benchmark suites. The first benchmark suite is taken directly from [Neider and Gavran, 2018] and contains 1217 samples, which were generated from common LTL properties. The second benchmark suite simulates real-world PSL use-cases and contains 390 synthetic samples, which we have generated from PSL formulas that commonly appear in practice (e.g., (p1 ◦ p2)∗ ↦→ q; see [Eisner and Fisman, 2006] for more examples). Our procedure to generate these samples is similar to the one by [Neider and Gavran, 2018] and proceeds as follows: firstly, we select a formula ϕ from our pool of PSL formulas; secondly, we generate samples consisting of a number (ranging from 10 to 500) of ultimately periodic words uvω with |u| + |v| ≤ 15; thirdly, we partition the words in each sample into sets P and N depending on their satisfaction of ϕ. In total, the median size of the samples in the second benchmark suite is 100 words. All experiments were conducted on a single core of an Intel Xeon E7-8857 V2 CPU (at 3.6 GHz) with a timeout of 1800 s. [1 The tool is available at https://github.com/ifm-mpi/Flie-PSL.](https://github.com/ifm-mpi/Flie-PSL) The two diagrams on the left of Figure 2 compare the runtime of Flie-PSL and LTL-Infer on the first and second benchmark suite, respectively. In general, Flie-PSL was moderately slower than LTL-Infer and timed out 1.34 times more often (Flie-PSL timed out 38.4% and 56.2% of the times on the first and second benchmark suite, respectively, whereas LTL-Infer timed out 24.8% and 53.6% of the times). This was surprising given that learning PSL formulas is inherently more complex than learning LTL formulas (both are essentially search problems, and the search space for PSL formulas subsumes the one for LTL formulas). Moreover, for PSL formulas that are not LTL formulas, one has to consider longer prefixes of the word uvω (see Lemma 1), resulting in a more complex SAT encoding. In fact, there were even 25 benchmarks on which Flie-PSL outperformed LTL-Infer because it was able to learn smaller formulas. The two diagrams on the right of Figure 2 compare the size of the learned formulas. On the first benchmark suite, we observe that Flie-PSL mainly produced pure LTL formulas of the same size as LTL-Infer (a likely explanation for this is that these benchmarks have explicitly been designed to capture LTL properties). However, on 68 benchmarks of the second suite, Flie-PSL learned PSL formulas containing regular expressions and was able to recover the exact PSL property used to generate the sample in 40 of the benchmarks. Overall, Flie-PSL learned a smaller formula in 52 benchmarks. ## 6 Conclusion We have developed an algorithm for learning interpretable models expressed in PSL and have shown empirically that this algorithm infers interesting PSL formulas with only little overhead as compared to learning LTL formulas. For future work, we plan to extend our algorithm to noisy data and, orthogonally, to learn models expressed as ω-regular expressions. ## Acknowledgements This work was partly supported by DFG grant no. 434592664. ## References 1. [Alur et al., 2015] Rajeev Alur, Rastislav Bodík, Eric Dal- lal, Dana Fisman, Pranav Garg, Garvit Juniwal, Hadas Kress-Gazit, P. Madhusudan, Milo M. K. Martin, Mukund Raghothaman, Shambwaditya Saha, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. Syntax-guided synthesis. In Dependable Software Systems Engineering, pages 1-25. 2015. 2. [Alur et al., 2018] Rajeev Alur, Rishabh Singh, Dana Fisman, and Armando Solar-Lezama. Search-based program syn- thesis. Commun. ACM, 61(12):84-93, 2018. 3. [Armoni et al., 2002] Roy Armoni, Limor Fix, Alon Flaisher, Rob Gerth, Boris Ginsburg, Tomer Kanza, Avner Land- ver, Sela Mador-Haim, Eli Singerman, Andreas Tiemeyer, Moshe Y. Vardi, and Yael Zbar. The forspec temporal logic: A new temporal property-specification language. In 8th International Conference of Tools and Algorithms for the Construction and Analysis of Systems, TACAS '02, volume 2280 of LNCS, pages 296-211. Springer, 2002. 4. [Balyo et al., 2017] Tomás Balyo, Marijn J. H. Heule, and Matti Järvisalo. SAT competition 2016: Recent develop- ments. In 31st AAAI Conference on Artificial Intelligence, AAAI '17, pages 5061-5063. AAAI Press, 2017. 5. [Bartoli et al., 2014] Alberto Bartoli, Giorgio Davanzo, An- drea De Lorenzo, Eric Medvet, and Enrico Sorio. Au- tomatic synthesis of regular expressions from examples. IEEE Computer, 47(12):72-80, 2014. 6. [Camacho and McIlraith, 2019] Alberto Camacho and Sheila A. McIlraith. Learning interpretable models expressed in linear temporal logic. In 29th International Conference on Automated Planning and Scheduling, ICAPS '18, pages 621-630. AAAI Press, 2019. 7. [Chesani et al., 2009] Federico Chesani, Evelina Lamma, Paola Mello, Marco Montali, Fabrizio Riguzzi, and Ser- gio Storari. Exploiting inductive logic programming tech- niques for declarative process mining. Trans. Petri Nets Other Model. Concurr., 2:278-295, 2009. 8. [Cook, 1971] Stephen A. Cook. The complexity of theorem- proving procedures. In 3rd Annual ACM Symposium on Theory of Computing, STOC '71, pages 151-158. ACM, 1971. 9. [de Moura and Bjørner, 2008] Leonardo Mendonc ¸a de Moura and Nikolaj Bjørner. Z3: an efficient SMT solver. In 14th International Conference of Tools and Algorithms for the Construction and Analysis of Systems, TACAS '08, volume 4963 of LNCS, pages 337-340. 10. [Eisner and Fisman, 2006] Cindy Eisner and Dana Fisman. A Practical Introduction to PSL. Series on Integrated Circuits and Systems. Springer, 2006. 11. [Eisner and Fisman, 2018] Cindy Eisner and Dana Fisman. Functional specification of hardware via temporal logic. In Handbook of Model Checking, pages 795-829. 2018. 12. [Heule and Verwer, 2010] Marijn Heule and Sicco Verwer. Exact DFA identification using SAT solvers. In 10th Inter- national Colloquium of Grammatical Inference: Theoret- ical Results and Applications, ICGI '10, volume 6339 of LNCS, pages 66-79. Springer, 2010. 13. [IEEE Standards Association, 2010] IEEE Standards Associ- ation. IEEE 1850-2010 -IEEE standard for property speci- fication language (PSL), 2010. 14. [Kim et al., 2019] Joseph Kim, Christian Muise, Ankit Shah, Shubham Agarwal, and Julie Shah. Bayesian inference of linear temporal logic specifications for contrastive explana- tions. In 28th International Joint Conference on Artificial Intelligence, IJCAI '19, pages 5591-5598. ijcai.org, 2019. 15. [Kong et al., 2017] Zhaodan Kong, Austin Jones, and Calin Belta. Temporal logics for learning and detection of anoma- lous behavior. IEEE Trans. Automat. Contr., 62(3):1210- 1222, 2017. 16. [Lamma et al., 2007] Evelina Lamma, Paola Mello, Marco Montali, Fabrizio Riguzzi, and Sergio Storari. Inducing declarative logic-based models from labeled traces. In BPM, volume 4714 of LNCS, pages 344-359. Springer, 2007. 17. [Lemieux et al., 2015] Caroline Lemieux, Dennis Park, and Ivan Beschastnikh. General LTL specification mining (T). In 30th IEEE/ACM International Conference on Automated Software Engineering, ASE '15, pages 81-92. IEEE Com- puter Society, 2015. 18. [Li et al., 2011] Wenchao Li, Lili Dworkin, and Sanjit A. Se- shia. Mining assumptions for synthesis. In 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign, MEMOCODE '11, pages 43-50. IEEE, 2011. 19. [Neider and Gavran, 2018] Daniel Neider and Ivan Gavran. Learning linear temporal properties. In 2018 Formal Meth- ods in Computer Aided Design, FMCAD '18, pages 1-10. IEEE, 2018. 20. [Neider, 2012] Daniel Neider. Computing minimal separating dfas and regular invariants using SAT and SMT solvers. In 10th International Symposium of Automated Technology for Verification and Analysis, ATVA '12, volume 7561 of LNCS, pages 354-369. Springer, 2012. 21. [Pnueli, 1977] Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium of Foundations of Computer Science, FOCS '77, pages 46-57. IEEE Computer Society, 1977. 22. [Riener, 2019] Heinz Riener. Exact synthesis of LTL prop- erties from traces. In 2019 Forum for Specification and Design Languages, FDL '19, pages 1-6. IEEE, 2019. 23. [Wasylkowski and Zeller, 2009] Andrzej Wasylkowski and Andreas Zeller. Mining temporal specifications from object usage. In 24th IEEE/ACM International Conference on Automated Software Engineering, ASE '09, pages 295-306. IEEE Computer Society, 2009. 24. [Wolper, 1981] Pierre Wolper. Temporal logic can be more expressive. In 22nd Annual Symposium on Foundations of Computer Science, FOCS '81, pages 340-348. IEEE Computer Society, 1981.