# satbased_explicit_ltlf_satisfiability_checking__123f3b79.pdf

The Thirty-Third AAAI Conference on Artiﬁcial Intelligence (AAAI-19)

SAT-Based Explicit LTLf Satisﬁability Checking

Jianwen Li, Kristin Y. Rozier Iowa State University Ames, IA, USA {jianwen,kyrozier}@iastate.edu

Geguang Pu, Yueling Zhang East China Normal University Shanghai, China {ggpu,ylzhang}@sei.ecnu.edu.cn

Moshe Y. Vardi Rice University Houston, TX, USA vardi@cs.rice.edu

We present a SAT-based framework for LTLf (Linear Temporal Logic on Finite Traces) satisﬁability checking. We use propositional SAT-solving techniques to construct a transition system for the input LTLf formula; satisﬁability checking is then reduced to a path-search problem over this transition system. Furthermore, we introduce CDLSC (Conﬂict-Driven LTLf Satisﬁability Checking), a novel algorithm that leverages information produced by propositional SAT solvers from both satisﬁability and unsatisﬁability results. Experimental evaluations show that CDLSC outperforms all other existing approaches for LTLf satisﬁability checking, by demonstrating an approximate four-fold speed-up compared to the second-best solver.

Introduction Linear Temporal Logic over Finite Traces, or LTLf, is a formal language gaining popularity in the AI community for formalizing and validating system behaviors. While standard Linear Temporal Logic (LTL) is interpreted on inﬁnite traces (Pnueli 1977), LTLf is interpreted over ﬁnite traces (De Giacomo and Vardi 2013). While LTL is typically used in formal-veriﬁcation settings, where we are interested in nonterminating computations, cf. (Vardi 2007), LTLf is more attractive in AI scenarios focusing on ﬁnite behaviors, such as planning (Bacchus and Kabanza 1998; De Giacomo and Vardi 1999; Calvanese, De Giacomo, and Vardi 2002; Patrizi et al. 2011; Camacho et al. 2017), plan constraints (Bacchus and Kabanza 2000; Gabaldon 2004), and user preferences (Bienvenu, Fritz, and Mc Ilraith 2006; 2011; Sohrabi, Baier, and Mc Ilraith 2011). Due to the wide spectrum of applications of LTLf in the AI community (De Giacomo, Masellis, and Montali 2014), it is worthwhile to study and develop an efﬁcient framework for solving LTLf-reasoning problems. Just as propositional satisﬁability checking is one of the most fundamental propositional reasoning tasks, LTLf satisﬁability checking is a fundamental task for LTLf reasoning. Given an LTLf formula, the satisﬁability problem asks whether there is a ﬁnite trace that satisﬁes the formula. A

A full report is at http://temporallogic.org/research/AAAI19/. Geguang Pu and Kristin Y. Rozier are corresponding authors. Copyright c 2019, Association for the Advancement of Artiﬁcial Intelligence (www.aaai.org). All rights reserved.

classical solution to this problem is to reduce it to the LTL satisﬁability problem (De Giacomo and Vardi 2013). The advantage of this approach is that the LTL satisﬁability problem has been studied for at least a decade, and many mature tools are available, cf. (Rozier and Vardi 2007; 2010). Thus, LTLf satisﬁability checking can beneﬁt from progress in LTL satisﬁability checking. There is, however, an inherent drawback that an extra cost has to be paid when checking LTL formulas, as the tool searches for a lasso (a lasso consists of a ﬁnite path plus a cycle, representing an inﬁnite trace), whereas models of LTLf formulas are just ﬁnite traces. Based on this motivation, (Li et al. 2014) presented a tableau-style algorithm for LTLf satisﬁability checking. They showed that the dedicated tool, Aalta-ﬁnite, which conducts an explicit-state search for a satisfying trace, outperforms extant tools for LTLf satisﬁability checking. The conclusion of a dedicated solver being superior to LTLf satisﬁability checking from (Li et al. 2014), seems to be out of date by now because of the recent dramatic improvement in propositional SAT solving, cf. (Malik and Zhang 2009). On one hand, SAT-based techniques have led to a signiﬁcant improvement on LTL satisﬁability checking, outperforming the tableau-based techniques of Aaltaﬁnite (Li et al. 2014). (Also, the SAT-based tool ltl2sat for LTLf satisﬁability checking outperforms Aalta-ﬁnite on particular benchmarks (Fionda and Greco 2016).) On the other hand, SAT-based techniques are now dominant in symbolic model checking (Cavada et al. 2014; Vizel, Weissenbacher, and Malik 2015). Our preliminary evaluation indicates that LTLf satisﬁability checking via SAT-based model checking (Bradley 2011; Een, Mishchenko, and Brayton 2011) or via SAT-based LTL satisﬁability checking (Li et al. 2015) both outperform the tableau-based tool Aalta-ﬁnite. Thus, the question raised initially in (Rozier and Vardi 2007) needs to be re-opened with respect to LTLf satisﬁability checking: is it best to reduce to SAT-based model checking or develop a dedicated SAT-based tool? Inspired by (Li et al. 2015), we present an explicit-state SAT-based framework for LTLf satisﬁability. We construct the LTLf transition system by utilizing SAT solvers to compute the states explicitly. Furthermore, by making use of both satisﬁability and unsatisﬁability information from SAT solvers, we propose a conﬂict-driven algorithm, CDLSC, for efﬁcient LTLf satisﬁability checking. We show that by

specializing the transition-system approach of (Li et al. 2015) to LTLf and its ﬁnite-trace semantics, we get a framework that is signiﬁcantly simpler and yields a much more efﬁcient algorithm CDLSC than the one in (Li et al. 2015). We conduct a comprehensive comparison among different approaches. Our experimental results show that the performance of CDLSC dominates all other existing LTLf-satisﬁability-checking algorithms. On average, CDLSC achieves an approximate four-fold speed-up, compared to the second-best solution (IC3 (Bradley 2011)+KLIVE (Claessen and S orensson 2012)) tested in our experiments. Our results re-afﬁrm the conclusion of (Li et al. 2014) that the best approach to LTLf satisﬁability solving is via a dedicated tool, based on explicit-state techniques.

LTL over Finite Traces Given a set P of atomic propositions, an LTLf formula φ has the form: φ ::= tt | p | φ | φ φ | Xφ | φUφ; where tt is true, is the negation operator, is the and operator, X is the strong Next operator and U is the Until operator. We also have the duals ﬀ(false) for tt, for , N (weak Next) for X and R for U. A literal is an atom p P or its negation ( p). Moreover, we use the notation Gφ (Globally) and Fφ (Eventually) to represent ﬀRφ and tt Uφ. Notably, X is the standard next operator, while N is weak next; X requires the existence of a successor state, while N does not. Thus Nφ is always true in the last state of a ﬁnite trace, since no successor exists there. This distinction is speciﬁc to LTLf. LTLf formulas are interpreted over ﬁnite traces (De Giacomo and Vardi 2013). Given an atom set P, we deﬁne Σ = 2P be the family of sets of atoms. Let ξ Σ+ be a ﬁnite nonempty trace, with ξ = σ0σ1 . . . σn. we use |ξ| = n + 1 to denote the length of ξ. Moreover, for 0 i n, we denote ξ[i] as the i-th position of ξ, and ξi to represent σiσi+1 . . . σn, which is the sufﬁx of ξ from position i. We deﬁne the satisfaction relation ξ |= φ as follows: ξ |= tt; and ξ |= p, if p P and p ξ[0]; ξ |= φ, if ξ |= φ; ξ |= φ1 φ2, if ξ |= φ1 and ξ |= φ2; ξ |= Xφ if |ξ| > 1 and ξ1 |= ψ; ξ |= (φ1Uφ2), if there exists 0 i < |ξ| such that ξi |= φ2 and for every 0 j < i it holds that ξj |= φ1; Deﬁnition 1 (LTLf Satisﬁability Problem). Given an LTLf formula φ over the alphabet Σ, we say φ is satisﬁable iff there is a ﬁnite nonempty trace ξ Σ+ such that ξ |= φ. Notations. We use cl(φ) to denote the set of subformulas of φ. Let A be a set of LTLf formulas, we denote V A to be the formula V

ψ A ψ. The two LTLf formulas φ1, φ2 are semantically equivalent, denoted as φ1 φ2, iff for every ﬁnite trace ξ, ξ |= φ1 iff ξ |= φ2. Obviously, we have (φ1 φ2) ( φ1 φ2), Nψ X ψ and (φ1Rφ2) ( φ1U φ2). We say an LTLf formula φ is in Tail Normal Form (TNF) if φ is in Negated Normal Form (NNF) and N-free. It is trivial to know that every LTLf formula has an equivalent NNF.

Assume φ is in NNF, tnf(φ) is deﬁned as t(φ) FTail, where Tail is a new atom to identify the last state of satisfying traces (Motivated from (De Giacomo and Vardi 2013)), and t(φ) is an LTLf formula deﬁned recursively as follows: (1) t(φ) = φ if φ is tt, ﬀor a literal; (2) t(Xψ) = Tail X(t(ψ)); (3) t(Nψ) = Tail X(t(ψ)); (4) t(φ1 φ2) = t(φ1) t(φ2); (5) t(φ1 φ2) = t(φ1) t(φ2); (6) t(φ1Uφ2) = ( Tail t(φ1))Ut(φ2); (7) t(φ1Rφ2) = (Tail t(φ1))Rt(φ2).

Theorem 1. φ is satisﬁable iff tnf(φ) is satisﬁable.

In the rest of the paper, unless clearly speciﬁed, the input LTLf formula is in TNF.

Approach Overview There is a Non-deterministic Finite Automaton (NFA) Aφ that accepts exactly the same language as an LTLf formula φ (De Giacomo and Vardi 2013). Instead of constructing the NFA for φ, we generate the corresponding transition system (Deﬁnition 5), by leveraging SAT solvers. The transition system represents an intermediate structure of the NFA, in which every state consists of a set of subformulas of φ. The classic approach to generate the NFA from an LTLf formula, i.e., Tableau Construction (Gerth et al. 1995), creates the set of all one-transition next states of the current state. Since the number of these states can be extremely large, we leverage SAT solvers to compute the next states of the current state iteratively. Although both approaches share the same worst case (computing all states in the state space), our new approach is better for on-the-ﬂy checking, as it computes new states only if the satisﬁability of the formula cannot be determined based on existing states. We show the SAT-based approach via an example. Consider the formula φ = ( Tail a)Ub. The initial state s0 of the transition system is {φ}. To compute the next states of s0, we translate φ to its equivalent ne Xt Normal Form (XNF), e.g., xnf(φ) = (b (( Tail a) Xφ)), see Deﬁnition 4. If we replace Xφ in xnf(φ) with a new propositions p1, the new formula, denoted xnf(φ)p, is a pure Boolean formula. As a result, a SAT solver can compute an assignment for the formula xnf(φ)p. Assume the assignment is {a, b, Tail, p1}, then we can induce that (a b Tail Xφ) φ is true, which indicates {φ} = s0 is a one-transition next state of s0, i.e., s0 has a self-loop with the label {a, b, Tail}. To compute another next state of s0, we add the constraint p1 to the input of the SAT solver. Repeat the above process and we can construct all states in the transition system. Checking the satisﬁability of φ is then reduced to ﬁnding a ﬁnal state (Deﬁnition 6) in the corresponding transition system. Since φ is in TNF, a ﬁnal state s meets the constraint that Tail xnf(V s)p (recall s is a set of subformulas of φ) is satisﬁable. For the above example, the initial state s0 is actually a ﬁnal state, as Tail xnf(φ)p is satisﬁable. Because all states computed by the SAT solver in the transition system are reachable from the initial state, we can prove that φ is satisﬁable iff there is a ﬁnal state in the system (Theorem 4). We present a conﬂict-driven algorithm, i.e., CDLSC, to accelerate the satisﬁability checking. CDLSC maintains a

conﬂict sequence C, in which each element, denoted as C[i] (0 i < |C|), is a set of states in the transition system that cannot reach a ﬁnal state in i steps. Starting from the initial state, CDLSC iteratively checks whether a ﬁnal state can be reached, and makes use of the conﬂict sequence to accelerate the search. Consider the formula φ = ( Tail)Ua ( Tail)U( a) ( Tail)Ub ( Tail)U( b) ( Tail)Uc. In the ﬁrst iteration, CDLSC checks whether the initial state s0 = {φ} is a ﬁnal state, i.e., whether Tail xnf(φ)p is satisﬁable. The answer is negative, so s0 cannot reach a ﬁnal state in 0 steps and can be added into C[0]. However, we can do better by leveraging the Unsatisﬁable Core (UC) returned from the SAT solver. Assume that we get the UC u1 = {( Tail)Ua, ( Tail)U( a)}. That indicates every state s containing u, i.e., s u, is not a ﬁnal state. As a result, we can add u instead of s0 into C[0], making the algorithm much more efﬁcient. Now in the second iteration, CDLSC ﬁrst tries to compute a one-transition next state of s0 that is not included in C[0]. (Otherwise the new state cannot reach a ﬁnal state in 0 step.) This can be encoded as a Boolean formula xnf(φ)p (p1 p2) where p1, p2 represent X(( Tail)Ua) and X(( Tail)U( a)) respectively. Assume the new state s1 = {( Tail)Ua, ( Tail)Ub, ( Tail)U( b), ( Tail)Uc} is generated from the assignment of the SAT solver. Then CDLSC checks whether s1 can reach a ﬁnal state in 0 step, i.e., xnf(V s1)p Tail is satisﬁable. The answer is negative and we can add the UC u2 = {( Tail)Ub, ( Tail)U( b)} to C[0] as well. Now to compute a next state of s0 that is not included in C[0], the encoded Boolean formula becomes xnf(φ)p (p1 p2) (p3 p4) where p3, p4 represent X(( Tail)Ub) and X(( Tail)U( b)) respectively. Assume the new state s2 = {( Tail)Ua, ( Tail)Ub, ( Tail)Uc} is generated from the assignment of the SAT solver. Since xnf(V s2)p Tail is satisﬁable, s2 is a ﬁnal state and we conclude that the formula φ is satisﬁable. In principle, there are a total of 25 = 32 states in the transition system of φ, but CDLSC succeeds to ﬁnd the answer by computing only 3 of them (including the initial state). CDLSC also leverages the conﬂict sequence to accelerate checking unsatisﬁable formulas. Like Bounded Model Checking (BMC) (Biere et al. 1999), CDLSC searches the model iteratively, but BMC invokes only one SAT call for each iteration, while CDLSC invokes multiple SAT calls. CDLSC is more like an IC3-style algorithm, but achieves a much simpler implementation by using UC instead of the Minimal Inductive Core (MIC) like IC3 (Bradley 2011).

SAT-based Explicit-State Checking Given an LTLf formula φ, we construct the LTLf transition system (Li et al. 2014; 2015) leveraging SAT solvers and then check the satisﬁability of the formula over its corresponding transition system.

LTLf Transition System First, we show how one can consider LTLf formulas as propositional ones. This requires considering temporal subformulas as propositional atoms.

Deﬁnition 2 (Propositional Atoms). For an LTLf formula φ, we deﬁne the set of propositional atoms of φ, i.e., PA(φ), as follows: (1) PA(φ) = {φ} if φ is an atom, Next, Until or Release formula; (2) PA(φ) = PA(ψ) if φ = ( ψ); (3) PA(φ) = PA(φ1) PA(φ2) if φ = (φ1 φ2) or (φ1 φ2). Consider φ = (a (( Tail a)Ub) ( Tail X(a b))). We have PA(φ) = {a, Tail, (( Tail a)Ub), (X(a b))}. Intuitively, the propositional atoms are obtained by treating all temporal subformulas of φ as atomic propositions. Thus, an LTLf formula φ can be viewed as a propositional formula over PA(φ). Deﬁnition 3. For an LTLf formula φ, let φp be φ considered as a propositional formula over PA(φ). A propositional assignment A of φp, is in 2PA(φ) and satisﬁes A |= φp. Consider the formula φ = (a ( Tail a)Ub) (b (Tail c)Rd). From Deﬁnition 3, φp is (a p1) (b p2) where p1, p2 are two Boolean variables representing the truth values of ( Tail a)Ub and (Tail c)Rd. Moreover, the set { a, p1(( Tail a)Ub), b, p2((Tail c)Rd)} is a propositional assignment of φp. In the rest of the paper, we do not introduce the intermediate variables and directly say { a, ( Tail a)Ub, b, (Tail c)Rd} is a propositional assignment of φp. The following theorem shows the relationship between the propositional assignment of φp and the satisfaction of φ. Theorem 2. For an LTLf formula φ and a ﬁnite trace ξ, ξ |= φ implies there exists a propositional assignment A of φp such that ξ |= V A; On the other hand, ξ |= V A where A is a propositional assignment of φp, also implies ξ |= φ. We now introduce the ne Xt Normal Form (XNF) of LTLf formulas, which is useful for the construction of the transition system. Deﬁnition 4 (ne Xt Normal Form). An LTLf formula φ is in ne Xt Normal Form (XNF) if there are no Until or Release subformulas of φ in PA(φ). For example, φ = (( Tail a)Ub) is not in XNF, while (b ( Tail a (X(( Tail a)Ub)))) is. Every LTLf formula φ has a linear-time conversion to an equivalent formula in XNF, which we denoted as xnf(φ). Theorem 3. For an LTLf formula φ, there is a corresponding LTLf formula xnf(φ) in XNF such that φ xnf(φ). Furthermore, the cost of the conversion is linear. Observe that when φ is in XNF, there can be only Next (no Until or Release) temporal formulas in the propositional assignment of φp. For φ = b (a Tail X(a Ub)), the set A = {a, b, Tail, X(a Ub)} is a propositional assignment of φp. Based on LTLf semantics, we can induce from A that if a ﬁnite trace ξ satisfying ξ[0] {a, b, Tail} and ξ1 |= a Ub, ξ |= φ is true. This motivates us to construct the transition system for φ, in which {a Ub} is a next state of {φ} and {a, b, Tail} is the transition label between these two states. Let φ be an LTLf formula and A be a propositional assignment of φp, we denote L(A) = {l|l A is a literal} and X(A) = {θ|Xθ A}. Now we deﬁne the transition system for an LTLf formula.

Deﬁnition 5. Given an LTLf formula φ and its literal set L, let Σ = 2L. We deﬁne the transition system Tφ = (S, s0, T) for φ, where S 2cl(φ) is the set of states, s0 = {φ} S is the initial state, and

T : S Σ 2S is the transition relation, where s2 T(s1, σ) (σ Σ) holds iff there is a propositional assignment A of xnf(V s1)p such that σ L(A) and s2 = X(A).

A run of Tφ on a ﬁnite trace ξ(|ξ| = n > 0) is a ﬁnite sequence s0, s1, . . . , sn such that s0 is the initial state and si+1 T(si, ξ[i]) holds for all 0 i < n.

We deﬁne the notation |r| for a run r, to represent the length of r, i.e., number of states in r. We say state s2 is reachable from state s1 in i(i 0) steps (resp. in up to i steps), if there is a run r on some ﬁnite trace ξ leading from s1 to s2 and |r| = i (resp. |r| i). In particular, we say s2 is a one-transition next state of s1 if s2 is reachable from s1 in 1 steps. Since a state s is a subset of cl(φ), which essentially is a formula with the form of V

ψ s ψ, we mix the usage of the state and formula in the rest of the paper. That is, a state can be a formula of V ψ s ψ, and a formula φ can be a set of states, i.e., s φ iff s φ.

Lemma 1. Let Tφ = (S, s0, T) be the transition system of φ. Every state s S is reachable from the initial state s0.

Deﬁnition 6 (Final State). Let s be a state of a transition system Tφ. Then s is a ﬁnal state of Tφ iff the Boolean formula Tail (xnf(s))p is satisﬁable.

By introducing the concept of ﬁnal state, we are able to check the satisﬁability of the LTLf formula φ over Tφ.

Theorem 4. Let φ be an LTLf formula. Then φ is satisﬁable iff there is a ﬁnal state in Tφ.

An intuitive solution from Theorem 4 to check the satisﬁability of φ is to construct states of Tφ until (1) either a ﬁnal state is found by Deﬁnition 6, meaning φ is satisﬁable; or (2) all states in Tφ are generated but no ﬁnal state can be found, meaning φ is unsatisﬁable. This approach is simple and easy to implement, however, it does not perform well according to our preliminary experiments.

Conﬂict-Driven LTLf Satisﬁability Checking

In this section, we present a conﬂict-driven algorithm for LTLf satisﬁability checking. The new algorithm is inspired by (Li et al. 2015), where information of both satisﬁability and unsatisﬁability results of SAT solvers are used. The motivation is as follows: In Deﬁnition 6, if the Boolean formula Tail xnf(s)p is unsatisﬁable, the SAT solver is able to provide a UC (Unsatisﬁable Core) c such that c s and Tail xnf(c)p is still unsatisﬁable. It means that c represents a set of states that are not ﬁnal states. By adding a new constraint (V

ψ c Xψ), the SAT solver can provide a model (if exists) that avoids re-generation of those states in c, which accelerates the search of ﬁnal states. More generally, we deﬁne the conﬂict sequence, which is used to maintain all information of UCs acquired during the checking process.

Deﬁnition 7 (Conﬂict Sequence). Given an LTLf formula φ, a conﬂict sequence C for the transition system Tφ is a ﬁnite sequence of set of states such that:

1. The initial state s0 = {φ} is in C[i] for 0 i < |C|; 2. Every state in C[0] is not a ﬁnal state; 3. For every state s C[i + 1] (0 i < |C| 1), all the one-transition next states of s are included in C[i]. We call each C[i] is a frame, and i is the frame level. In the deﬁnition, |C| represents the length of C and C[i] denotes the i-th element of C. Consider the transition system shown in Figure 1, in which s0 is the initial state and s4 is the ﬁnal state. Based on Deﬁnition 7, the sequence C = {s0, s1, s2, s3}, {s0, s1}, {s0} is a conﬂict sequence. Notably, the conﬂict sequence for a transition system may not be unique. For the above example, the sequence {s0, s1}, {s0} is also a conﬂict sequence for the system. This suggests that the construction of a conﬂict sequence is algorithm-speciﬁc. Moreover, it is not hard to induce that every non-empty preﬁx of a conﬂict sequence is also a conﬂict sequence. For example, a preﬁx of C above, i.e., {s0, s1, s2, s3}, {s0, s1}, is a conﬂict sequence. As a result, a conﬂict sequence can be constructed iteratively, i.e., the elements can be generated (and updated) in order. Our new algorithm is motivated by these two observations.

s0 start s1

Figure 1: An example transition system for the conﬂict sequence.

An inherent property of conﬂict sequences is described in the following lemma. Lemma 2. Let φ be an LTLf formula with a conﬂict sequence C for the transition system Tφ, then T

0 j i C[j](0 i < |C|) represents a set of states that cannot reach a ﬁnal state in up to i steps.

Proof. We ﬁrst prove C[i](i 0) is a set of states that cannot reach a ﬁnal state in i step. Basically from Deﬁnition 7, C[0] is a set of states that are not ﬁnal states. Inductively, assume C[i](i 0) is a set of states that cannot reach a ﬁnal state in i steps. From Item 3 of Deﬁnition 7, every state s C[i + 1] satisﬁes all its one-transition next states are in C[i], thus every state s C[i + 1] cannot reach a ﬁnal state in i + 1 steps. Now since C[i](i 0) is a set of states that cannot reach a ﬁnal state in i steps, T

0 j i C[j] is a set of states that cannot reach a ﬁnal state in up to i steps.

We are able to utilize the conﬂict sequence to accelerate the satisﬁability checking of LTLf formulas, using the theoretical foundations provided by Theorem 5 and 6 below.

Theorem 5. The LTLf formula φ is satisﬁable iff there is a run r = s0, s1, . . . , sn(n 0) of Tφ such that (1) sn is a ﬁnal state; and (2) si (0 i n) is not in C[n i] for every conﬂict sequence C of Tφ with |C| > n i.

Proof. ( ) Since sn is a ﬁnal state, φ is satisﬁable according to Theorem 4. ( ) Since φ is satisﬁable, there is a ﬁnite trace ξ such that the corresponding run r of Tφ on ξ ends with a ﬁnal state (according to Theorem 4). Let r be s0 s1 . . . sn where sn is the ﬁnal state. It holds that si (0 i n) is a state that can reach a ﬁnal state in n i steps. Moreover for every C of Tφ with |C| > n i, C[n i] (C[n i] is meaningless when |C| n i) represents a set of states that cannot reach a ﬁnal state in n i steps (From the proof of Lemma 2). As a result, it is true that si is not in C[n i] if |C| > n i.

Theorem 5 suggests that to check whether a state s can reach a ﬁnal state in i steps (i 1), ﬁnding a one-transition next state s of s that is not in C[i 1] is necessary; as s C[i 1] implies s cannot reach a ﬁnal state in i 1 steps (From the proof of Lemma 2). If all one-transition next states of s are in C[i 1], s cannot reach a ﬁnal state in i steps.

Theorem 6. The LTLf formula φ is unsatisﬁable iff there is a conﬂict sequence C and i 0 such that T

0 j i C[j] C[i + 1].

Proof. ( ) T

0 j i C[j] C[i + 1] is true implies that T

0 j i C[j] = T

0 j i+1 C[j] is true. Also from Lemma 2 we know T

0 j i C[j] is a set of states that cannot reach a ﬁnal state in up to i steps. Since φ C[i] is true for each i 0, φ is in T

0 j i C[j]. Moreover, T

0 j i C[j] = T

0 j i+1 C[j] is true implies all reachable states from φ are included in T 0 j i C[j]. We have known all states in T

0 j i C[j] are not ﬁnal states, so φ is unsatisﬁable. ( ) If φ is unsatisﬁable, every state in Tφ is not a ﬁnal state. Let S be the set of states of Tφ. According to Lemma 2, T

0 j i C[j](i 0) contains the set of states that are not ﬁnal in up to i steps. Now we let C satisfy that T

0 j i C[j](i 0) contains all states that are not ﬁnal in up to i steps, so T

0 j i C[j] includes all reachable states from φ, as φ is unsatisﬁable. However, because T

0 j i C[j] T

0 j i+1 C[j] S(i 0), there must be an i 0 such that T

0 j i C[j] = T

0 j i+1 C[j], which indicates that T

0 j i C[j] C[i + 1] is true.

Algorithm Design. The algorithm, named CDLSC (Conﬂict-Driven LTLf Satisﬁability Checking), constructs the transition system on-the-ﬂy. The initial state s0 is ﬁxed to be {φ} where φ is the input formula. From Deﬁnition 6, whether a state s is ﬁnal is reducible to the satisﬁability checking of the Boolean formula Tail xnf(s)p. If s0 is a ﬁnal state, there is no need to maintain the conﬂict sequence in CDLSC, and the algorithm can return SAT immediately; Otherwise, the conﬂict sequence is maintained as follows.

In CDLSC, every element of C is a set of set of subformulas of the input formula φ. Formally, each C[i] (i 0)

can be represented by the LTLf formula W c C[i] V ψ c ψ where c is a set of subformulas of φ. We mix-use the notation C[i] for the corresponding LTLf formula as well. Every state s satisfying s C[i] is included in C[i].

C is created iteratively. In each iteration i 0, C[i] is initialized as the empty set.

To compute elements in C[0], we consider an existing state s (e.g., s0). If the Boolean formula Tail xnf(s)p is unsatisﬁable, s is not a ﬁnal state and can be added into C[0] from Item 2 of Deﬁnition 7. Moreover, CDLSC leverages the Unsatisﬁable Core (UC) technique from the SAT community to add a set of states, all of which are not ﬁnal and include s, to C[0]. This set of states, denoted as c, is also represented by a set of LTLf formulas and satisﬁes c s.

To compute elements in C[i + 1] (i 0), we consider the Boolean formula (xnf(s) X(C[i]))p, where X(C[i]) represents the LTLf formula W

ψ c X(ψ). The above Boolean formula is used to check whether there is a one-transition next state of s that is not in C[i]. If the formula is unsatisﬁable, all the one-transition next states of s are in C[i], thus s can be added into C[i+1] according to Item 3 of Deﬁnition 7. Similarly, we also utilize the UC technique to obtain a subset c of s, such that c represents a set of states that can be added into C[i + 1].

As shown above, every Boolean formula sent to a SAT solver has the form of (xnf(s) θ)p where s is a state and θ is either Tail or X(C[i]). Since every state s consists of a set of LTLf formulas, the Boolean formula can be rewritten as α1 = (V

ψ s xnf(ψ) θ)p. Moreover, we introduce a new Boolean variable pψ for each ψ s, and re-encode the formula to be α2 = V

ψ s(xnf(ψ) pψ) θ)p. α2 is satisﬁable iff α1 is satisﬁable, and A is an assignment of α2 iff A\{pψ|ψ s} is an assignment of α1. Sending α2 instead of α1 to the SAT solver that supports assumptions (e.g., Minisat (E en and S orensson 2003)) enables the SAT solver to return the UC, which is a set of s, when α2 is unsatisﬁable. For example, assume s = {ψ1, ψ2, ψ3} and α2 is sent to the SAT solver with {pψi|i {1, 2, 3}} being the assumptions. If the SAT solver returns unsatisﬁable and the UC {pψ1}, the set c = {ψ1}, which represents every state including ψ1, is the one to be added into the corresponding C[i]. We use the notation get uc() for the above procedure. The pseudo-code of CDLSC is shown in Algorithm 1. Lines 1-2 consider the case when the input formula φ is a ﬁnal state itself. Otherwise, the ﬁrst frame C[0] is initialized to {φ} (Line 3), and the current frame level is set to 0 (Line 4). After that, the loop body (Line 5-11) keeps updating the elements of C iteratively, until either the procedure try satisfy returns true, which means it found a model of φ, or the procedure inv found returns true, which is the implementation of Theorem 6. The loop continues to create a new frame in C if neither of the procedures succeeds to return true. We call each run of the while loop body in Algorithm 1 an iteration. The procedure try satisfy updates C. Taking a formula φ and the current frame level, frame level, try satisfy returns true iff a model of φ can be found, with the length of frame level + 1. As shown in Algorithm 2, try satisfy is

Algorithm 1 Implementation of CDLSC Require: An LTLf formula φ. Ensure: SAT or UNSAT.

1: if Tail xnf(φ)p is satisﬁable then 2: return SAT; 3: Set C[0] := {φ}; 4: Set frame level := 0; 5: while true do 6: if try satisfy(φ, frame level) returns true then 7: return SAT; 8: if inv found(frame level) returns true then 9: return UNSAT; 10: frame level := frame level + 1; 11: Set C[frame level] = ;

implemented recursively. Each time it checks whether a next state of the input φ, which belongs to a lower level (than the input frame level) frame can be found (Line 2). If such a new state φ is constructed, try satisfy ﬁrst checks whether φ is a ﬁnal state when frame level is 0 and returns true if so. If φ is not a ﬁnal state, a UC is extracted from the SAT solver and added to C[0] (Line 5-11). If frame level is not 0, try satisfy recursively checks whether a model of φ can be found with the length of frame level (Line 1213). If the result is negative and such a state cannot be constructed, a UC is extracted from the SAT solver and added into C[frame level + 1] (Line 14-15).

Algorithm 2 Implementation of try satisfy Require: φ: The formula is working on; frame level: The frame level is working on. Ensure: true or false.

1: Let ψ = X(C[frame level]); 2: while (ψ xnf(φ))p is satisﬁable do 3: Let A be the model of (ψ xnf(φ))p; 4: Let φ = X(A), i.e., be the next state of φ extracted from A; 5: if frame level == 0 then 6: if Tail xnf(φ )p is satisﬁable then 7: return true; 8: else 9: Let c = get uc(); 10: Add c into C[frame level]; 11: Continue; 12: if try satisfy(φ , frame level 1) is true then 13: return true; 14: Let c = get uc(); 15: Add c into C[frame level + 1]; 16: return false;

Notably, Item 1 of Deﬁnition 7, i.e., {φ} C[i], is guaranteed for each i 0, as the original input formula of try satisfy is always φ (Line 6 in Algorithm 1) and there is some c (Line 15 in Algorithm 2) including {φ} that is added into C[i], if no model can be found in the current iteration. The procedure inv found in Algorithm 1 implements Theorem 6 in a straightforward way: it reduces checking

0 5000 10000 15000 20000

0 1000 2000 3000 4000 5000 6000 7000

Aalta-finite

ltl2sat Aalta-infinite

Figure 2: Result for LTLf Satisﬁability Checking on LTLas-LTLf Benchmarks. The X axis represents the number of benchmarks, and the Y axis is the accumulated checking time (s).

0 j i C[j] C[i + 1] holds on some frame level i, to satisﬁability checking of the Boolean formula V

1 j i C[j] C[i + 1]. Theorem 7 provides the theoretical guarantee that CDLSC always terminates correctly.

Lemma 3. After each iteration of CDLSC with no model found, the sequence C is a conﬂict sequence of Tφ for the transition system Tφ.

Theorem 7. The CDLSC algorithm terminates with a correct result.

Summarily, CDLSC is a conﬂict-driven on-the-ﬂy satisﬁability checking algorithm, which successfully leads to either an earlier ﬁnding of a satisfying model, or the faster termination with the unsatisﬁable result.

Experimental Evaluation Benchmarks1 Our extensive experimental evaluation, checking 9142 formulas, uses two classes of benchmarks: 7442 LTL-as-LTLf (since LTL formulas share the same syntax as LTLf) and 1700 LTLf-Speciﬁc benchmarks, which are common LTLf patterns that are all satisﬁable by ﬁnite traces (but not necessarily by inﬁnite traces). We check both execution time and correctness; checking also correctness, as in (Rozier and Vardi 2007), ensures we are comparing performance of tools ﬁnding the same results. LTL-as-LTLf benchmarks consist of the following. Random Formulas generated as in (Rozier and Vardi 2011), vary the number of variables {1, 2, 3}, formula length {5, ..., 100}, and probability of choosing a temporal operator {0.3, 0.5, 0.7, 0.95} from the operator set { , , , X, U, R, G, F, GF}. We generate all formulas prior to testing for repeatability. Counter Formulas scale four, temporally complex patterns that describe large state

1All artifacts for enabling reproducibility, including benchmark formulas and their generators, are available from the paper website at http://temporallogic.org/research/AAAI19.

Type Number Result IC3+K-LIVE Aalta-ﬁnite Aalta-inﬁnite ltl2sat CDLSC Alternate Response 100 sat 134 1 48 123 3 Alternate Precedence 100 sat 154 3 70 380 4 Chain Precedence 100 sat 127 2 45 83 2 Chain Response 100 sat 79 1 41 49 2 Precedence 100 sat 132 2 14 124 1 Responded Existence 100 sat 130 1 14 327 1 Response 100 sat 155 1 41 53 2 Practical Conjunction 1000 varies 1669 19564 4443 20477 115

Table 1: Results for LTLf Satisﬁability Checking on LTLf-speciﬁc Benchmarks.

spaces: n-bit binary counters for 1 n 20 (Rozier and Vardi 2007). The four templates differ in variables and nesting of X s. Pattern Formulas encode eight scalable patterns (from (Geldenhuys and Hansen 2006), and are generated by code from (Rozier and Vardi 2007)) scaling to n = 100. Other LTL formulas that were used as speciﬁcations in realistic case studies: (Bloem et al. 2007; De Wulf et al. 2008; Filiot, Jin, and Raskin 2009). LTLf-Speciﬁc benchmarks consist of the following. Conjunctive Formulas combine common LTLf formulas from (De Giacomo, Masellis, and Montali 2014; Ciccio and Mecella 2015; Prescher, Di Ciccio, and Mendling 2014) as random conjunctions in the style of (Li et al. 2013) in two sets of 500 formulas: (1) 20 variables, varying the number of conjuncts in {10, 30, 50, 70, 100}; and (2) 50 conjuncts, varying the number of variables in {10, 30, 50, 70, 100}. Pattern Formulas scalable patterns inspired by (Di Ciccio, Maggi, and Mendling 2016) up to length 100; see Table 1. Experimental Setup We implement CDLSC in the tool aaltaf 2 and use Minisat 2.2.0 (E en and S orensson 2003) as the SAT engine. We compare it with two extant LTLf satisﬁability solvers: Aalta-ﬁnite (Li et al. 2014) and ltl2sat (Fionda and Greco 2016). We also compared with the stateof-art LTL solver Aalta-inﬁnite (Li et al. 2015), using the LTLf-to-LTL satisﬁability-preserving reduction described in (De Giacomo and Vardi 2013). As LTL satisﬁability checking is reducible to model checking, as described in (Rozier and Vardi 2007), we also compared with this reduction, using nu Xmv with the IC3+K-LIVE back-end (Cavada et al. 2014), as an LTLf satisﬁability checker. We ran the experiments on a Red Hat 6.0 cluster with 2304 processor cores in 192 nodes (12 processor cores per node), running at 2.83 GHz with 48GB of RAM per node. Each tool executed on a dedicated node with a timeout of 60 seconds, measuring execution time with Unix time. Excluding timeouts, all solvers found correct verdicts for all formulas. All artifacts are available in the supplemental material. Results Figure 2 shows the results for LTLf satisﬁability checking on LTL-as-LTLf benchmarks. CDLSC outperforms all other approaches. On average, CDLSC performs about 4 times faster than the second-best approach IC3+KLIVE (1705 seconds vs. 6075 seconds). CDLSC checks the LTLf formula directly, while IC3+K-LIVE must take the input of the LTL formula translated from the LTLf formula. As a result, IC3-KLIVE may take extra cost, e.g., ﬁnding a satisfying lasso for the model, to the satisﬁability checking.

2https://github.com/lijwen2748/aaltaf

Meanwhile, CDLSC can beneﬁt from the heuristics dedicated for LTLf that are proposed in (Li et al. 2014). Finally, the performance of ltl2sat is highly tied to its performance for unsatisﬁability checking as most of the timeout cases for ltl2sat are unsatisﬁable. For Aalta-ﬁnite, its performance is restricted by the heavy cost of the Tableau Construction. Table 1 shows the results for LTLf-speciﬁc experiments. Columns 1-3 show the types of LTLf formulas under test, the number of test instances for each formula type, and the results by formula type. Columns 4-8 show the checking times by formula types in seconds. The dedicated LTLf solvers perform extremely fast on the seven scalable pattern formulas (Column 5 and 8), because their heuristics work well on these patterns. For the difﬁcult conjunctive benchmarks, CDLSC still outperforms all other solvers.

Discussion and Concluding Remarks There are two ways to apply Bounded Model Checking (BMC) to LTLf satisﬁability checking. The ﬁrst one is to check the satisﬁability of the LTL formula from the input LTLf formula. Since (Li et al. 2015) showed this approach performs worse than IC3+K-LIVE, CDLSC outperforming IC3+K-LIVE implies that CDLSC also outperforms BMC. The second approach is to check the satisﬁability of the LTLf formula φ directly, by unrolling φ iteratively. In the worst case, BMC can terminate (with UNSAT) once the iteration reaches the upper bound. This is exactly what is implemented in ltl2sat (Fionda and Greco 2016). Our experiments demonstrate that CDLSC outperforms Aalta-inﬁnite and IC3+K-LIVE, which are designed for LTL satisﬁability checking, showing the advantage of a dedicated algorithm for LTLf. Notably, CDLSC maintains a conﬂict sequence, which is similar to the state-of-art model checking technique IC3 (Bradley 2011). CDLSC does not require the conﬂict sequence to be monotone, and simply use the UC from SAT solvers to update the sequence. Meanwhile, IC3 requires the sequence to be strictly monotone, and has to compute its dedicated MIC (Minimal Inductive Core) to update the sequence. We conclude that CDLSC outperforms other existing approaches for LTLf satisﬁability checking. Acknowledgments. We thank anonymous reviewers for helpful comments. This work is supported by NASA ECF NNX16AR57G, NSF CAREER Award CNS-1552934, NSF grants CCF-1319459 and IIS-1527668, NSF Expeditions in Computing project Ex CAPE: Expeditions in Computer Augmented Program Engineering, NSFC projects No. 6157297, 61632005, 61532019, and China HGJ project No. 2017ZX01038102-002.

Bacchus, F., and Kabanza, F. 1998. Planning for temporally extended goals. Ann. of Mathematics and Artiﬁcial Intelligence 22:5 27. Bacchus, F., and Kabanza, F. 2000. Using temporal logic to express search control knowledge for planning. Artiﬁcial Intelligence 116(1 2):123 191. Bienvenu, M.; Fritz, C.; and Mc Ilraith, S. 2006. Planning with qualitative temporal preferences. In KR, 134 144. Bienvenu, M.; Fritz, C.; and Mc Ilraith, S. A. 2011. Specifying and computing preferred plans. Artiﬁcial Intelligence 175(7C8):1308 1345. Biere, A.; Cimatti, A.; Clarke, E.; and Zhu, Y. 1999. Symbolic model checking without BDDs. In Proc. 5th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 1579 of Lecture Notes in Computer Science. Springer. Bloem, R.; Galler, S.; Jobstmann, B.; Piterman, N.; Pnueli, A.; and Weiglhofer, M. 2007. Automatic hardware synthesis from speciﬁcations: A case study. In DATE, 1188 1193. Bradley, A. 2011. SAT-based model checking without unrolling. In Jhala, R., and Schmidt, D., eds., Veriﬁcation, Model Checking, and Abstract Interpretation, volume 6538 of LNCS. Springer. 70 87. Calvanese, D.; De Giacomo, G.; and Vardi, M. 2002. Reasoning about actions and planning in LTL action theories. In Principles of Knowledge Representation and Reasoning, 593 602. Morgan Kaufmann. Camacho, A.; Baier, J.; Muise, C.; and Mc Ilraith, A. 2017. Bridging the gap between LTL synthesis and automated planning. Technical report, U. Toronto. Cavada, R.; Cimatti, A.; Dorigatti, M.; Griggio, A.; Mariotti, A.; Micheli, A.; Mover, S.; Roveri, M.; and Tonetta, S. 2014. The Nu XMV symbolic model checker. In CAV, 334 342. Ciccio, C. D., and Mecella, M. 2015. On the discovery of declarative control ﬂows for artful processes. ACM Trans. Manage. Inf. Syst. 5(4):24:1 24:37. Claessen, K., and S orensson, N. 2012. A liveness checking algorithm that counts. In FMCAD, 52 59. IEEE. De Giacomo, G., and Vardi, M. 1999. Automata-theoretic approach to planning for temporally extended goals. In Proc. European Conf. on Planning, Lecture Notes in AI 1809, 226 238. Springer. De Giacomo, G., and Vardi, M. 2013. Linear temporal logic and linear dynamic logic on ﬁnite traces. In IJCAI, 2000 2007. AAAI Press. De Giacomo, G.; Masellis, R. D.; and Montali, M. 2014. Reasoning on LTL on ﬁnite traces: Insensitivity to inﬁniteness. In AAAI, 1027 1033. De Wulf, M.; Doyen, L.; Maquet, N.; and Raskin, J.-F. 2008. Antichains: Alternative algorithms for LTL satisﬁability and model-checking. In TACAS, volume 4963 of LNCS, 63 77. Springer. Di Ciccio, C.; Maggi, F.; and Mendling, J. 2016. Efﬁcient

discovery of target-branched declare constraints. Inf. Syst. 56(C):258 283. E en, N., and S orensson, N. 2003. An extensible SAT-solver. In SAT, 502 518. Een, N.; Mishchenko, A.; and Brayton, R. 2011. Efﬁcient implementation of property directed reachability. In FMCAD, 125 134. Filiot, E.; Jin, N.; and Raskin, J.-F. 2009. An antichain algorithm for LTL realizability. In CAV, 263 277. Fionda, V., and Greco, G. 2016. The complexity of LTL on ﬁnite traces: Hard and easy fragments. In AAAI, 971 977. AAAI Press. Gabaldon, A. 2004. Precondition control and the progression algorithm. In KR, 634 643. AAAI Press. Geldenhuys, J., and Hansen, H. 2006. Larger automata and less work for LTL model checking. In SPIN, volume 3925 of LNCS, 53 70. Springer. Gerth, R.; Peled, D.; Vardi, M.; and Wolper, P. 1995. Simple on-the-ﬂy automatic veriﬁcation of linear temporal logic. In Dembiski, P., and Sredniawa, M., eds., Protocol Speciﬁcation, Testing, and Veriﬁcation, 3 18. Chapman & Hall. Li, J.; Zhang, L.; Pu, G.; Vardi, M.; and He, J. 2013. LTL satisﬁbility checking revisited. In TIME, 91 98. Li, J.; Zhang, L.; Pu, G.; Vardi, M. Y.; and He, J. 2014. LTLf satisﬁbility checking. In ECAI, 91 98. Li, J.; Zhu, S.; Pu, G.; and Vardi, M. 2015. SAT-based explicit LTL reasoning. In HVC, 209 224. Springer. Malik, S., and Zhang, L. 2009. Boolean satisﬁability from theoretical hardness to practical success. Commun. ACM 52(8):76 82. Patrizi, F.; Lipoveztky, N.; De Giacomo, G.; and Geffner, H. 2011. Computing inﬁnite plans for LTL goals using a classical planner. In IJCAI, 2003 2008. AAAI Press. Pnueli, A. 1977. The temporal logic of programs. In IEEE FOCS, 46 57. Prescher, J.; Di Ciccio, C.; and Mendling, J. 2014. From declarative processes to imperative models. SIMPDA 1293:162 173. Rozier, K., and Vardi, M. 2007. LTL satisﬁability checking. In SPIN, volume 4595 of LNCS, 149 167. Springer. Rozier, K., and Vardi, M. 2010. LTL satisﬁability checking. STTT 12(2):123 137. Rozier, K., and Vardi, M. 2011. A multi-encoding approach for LTL symbolic satisﬁability checking. In Int l Symp. on Formal Methods, volume 6664 of LNCS, 417 431. Springer. Sohrabi, S.; Baier, J. A.; and Mc Ilraith, S. A. 2011. Preferred explanations: Theory and generation via planning. In AAAI, 261 267. Vardi, M. 2007. Automata-theoretic model checking revisited. In VMCAI, LNCS 4349, 137 150. Springer. Vizel, Y.; Weissenbacher, G.; and Malik, S. 2015. Boolean satisﬁability solvers and their applications in model checking. Proceedings of the IEEE 103(11):2021 2035.