Teaching LTLf Satisfiability Checking to Neural Networks

1 Introduction

Linear temporal logic over finite traces (LTLf ) [Giacomo and Vardi, 2013] is one of the popular modal logics in artificial intelligence (AI). Since LTLf is well-defined and unambiguous, it has been widely applied to formalize and validate system behaviors. LTLf satisfiability checking is a fundamental problem of LTLf , i.e., checking whether a given LTLf formula is satisfiable or unsatisfiable. Compared with Linear temporal logic (LTL) [Pnueli, 1977], LTLf is interested in finite traces [Giacomo and Vardi, 2013]. Therefore, LTLf is more attractive in AI focusing on finite behaviors, such as reinforcement learning [Xie et al., 2021], program synthesis [Xiao et al., 2021], and explainable AI [Kim et al., 2019].

The complexity of LTLf satisfiability checking is PSPACE-complete [Giacomo and Vardi, 2013]. Lots of approaches have tried to efficiently solve this problem. They are all based on crafted symbolic reasoning, e.g., based on tableau [Li et al., 2014] and based on SAT [Fionda and Greco, 2016; Li et al., 2020]. We refer to these approaches as symbolic approaches. A symbolic approach needs to be sound and complete, i.e., it must correctly answer whether a given formula is satisfiable or not. Given the inherent intractability of LTLf satisfiability checking, no symbolic approach scales to all datasets [Li et al., 2020]. Therefore, developing new methods for all different paradigms remains to be an interesting research direction [Li et al., 2020].

∗Corresponding author.

Recently, some approaches tried to introduce end-to-end neural networks to solve Boolean satisfiability (SAT) problems [Selsam et al., 2019; Cameron et al., 2020]. Their success stems from the fact that neural networks are able to capture permutation invariance of the semantics of Boolean formulae. A task is permutation invariant if permutations of its input do not change the output. Although these works are not competitive with state-of-the-art (SOTA) symbolic approaches, they show the potential of neural networks in solving hard computational problems. This poses an interesting question: whether LTLf satisfiability checking can be effectively tackled by end-to-end neural networks?

To answer this question, we explore teaching end-to-end neural networks to check LTLf satisfiability. It is a challenge to integrate symbolic reasoning of LTLf with continuous neural reasoning, as it requires neural networks to capture the permutation invariance of LTLf . Some logical operators (e.g., ∧ operators) of LTLf are permutation invariant, i.e., arbitrarily changing the position of the sub-formula, the satisfiability of the formula remains unchanged. For example, both (north∨west) U door and (west ∨north) U door are satisfiable. Besides, neural networks need to model the sequentiality of LTLf . Some logical operators (e.g., U operator) of LTLf is sequential, i.e., changing the position of the sub-formula, the satisfiability of the formula can be changed. For example, (door U west) ∧ G¬door is satisfiable while (west U door) ∧ G¬door is unsatisfiable.

In this paper, we propose LTLfNet, a recursive neural network, to predict the satisfiability of a given LTLf formula end-to-end. While symbolic approaches scales exponentially with the formula size, LTLfNet spends only polynomial time to predict the result. Although LTLfNet does not guarantee soundness, its efficient framework and highly confident prediction are still worthwhile for some LTLf -SAT-heavy tasks. To bridge the gap between symbolic reasoning of LTLf and continuous neural reasoning, LTLfNet not only captures the syntactic features of LTLf by combining and aggregating features recursively over the syntax tree, but also models the permutation invariance and sequentiality of LTLf (semantic features). Specifically, to characterize the different semantics of logical operators, LTLfNet learns independent combination function for each logical operator as well as exploits aggregation functions fulfilling the permutation invariance or sequentiality for each logical operator.

Empirical evaluation on synthetic datasets shows that LTLfNet outperforms existing architectures that have been used to embed LTL or LTLf formulae. Besides, we also evaluate LTLfNet on some large-scale datasets. Results demonstrate strong generalization of LTLfNet and competitive results with the SOTA symbolic approaches such as nuXmv [Cavada et al., 2014] and CDLSC [Li et al., 2020].

2 RelatedWork

Symbolic approaches to LTLf satisfiability checking. The classical solution to LTLf satisfiability checking is reducing it to LTL satisfiability checking, which has been studied for decades and many tools are available, e.g., nuXmv [Cavada et al., 2014]. However, an extra cost has to be paid when checking LTL formulae, because the traces in LTL satisfiability checking are infinite while those are finite in LTLf satisfiability checking. Therefore, Li et al. (2014) presented a tableau-style algorithm for LTLf satisfiability checking so as to avoid this cost. Inspired by recent dramatic improvements in propositional SAT solving, Li et al. (2020) proposed an LTLf satisfiability checker via SAT-based model checking and demonstrated outstanding performance.

Permutation invariance. Permutation invariance is a key property in many symbolic logical reasoning mechanisms. A task is permutation invariant if permutations of its input leave the output unchanged. Take SAT problem for example, satisfiability status is unaffected by the permutation of variables and clauses. A number of recent works have studied neural network based methods for permutation invariance, such as sets [Zaheer et al., 2017; Lee et al., 2019], matrices and tensors [Hartford et al., 2018; Cameron et al., 2020], pooling [Murphy et al., 2019; Zhang et al., 2020], and graph structured data [Cameron et al., 2020]. All these methods build neural network layers respecting the permutation invariance, but they differ in how to aggregate the embeddings and which permutation-invariant function will be used in aggregation.

End-to-end neural networks for SAT. End-to-end neural networks for the SAT problem are often designed delicately to keep the property of permutation invariance so as to improve performance. Amizadeh et al. (2019) used an aggregation function in the model, which is invariant to the permutation of its input, to keep the property. Selsam et al. (2019) built a graph of the propositional formula and enforced permutation invariance by managing nodes and edges according to the topology of the graph without any additional ordering. Cameron et al. (2020) demonstrated that two different architectural approaches, i.e., exchangeable architecture [Hartford et al., 2018] and message passing [Selsam et al., 2019], can outperform previous approaches on random 3-SAT problems. Inspired by their work, we explore efficient end-to-end neural networks for LTLf satisfiability checking that can capture permutation invariance and sequentiality of LTLf .

Continuous neural representation of logical expressions.

It is hard to embed logical expressions because of the gap between the continuous neural representation and the discrete semantic definition of logical expressions. Nevertheless, there is work attempting to bridge this gap. Allamanis et al. (2017) proposed a TreeNN [Socher et al., 2013] based approach to learning the identical representation of the syntactic parse tree for semantically equivalent Boolean expressions. Evans et al. (2018) compared the abilities of different approaches in capturing and exploiting the structure of logical expressions against an entailment prediction task. They also proposed a model class named PossibleWorldNets, which computes entailment as a "convolution over possible worlds". Paliwal et al. (2020) used message passing graph neural networks to learn the representation of the modified abstract syntax tree of higher-order logic expressions. They demonstrated the benefits of modeling syntactic features of formulae to embed logical expressions.

Embedding LTL/LTLf formulae. In recent years, some works have tried to find a good way to embed LTL/LTLf formulae and explored the applications of LTL/LTLf formula embeddings. Xie et al. (2021) sought to incorporate temporal knowledge into deep sequential learning. They transferred an LTLf formula to a semantically equivalent deterministic finite-state automaton (DFA) and used the graph embeddings of the DFA as the representation of the LTLf formula. Empirical results confirmed that their approach improved deep models for sequential human action recognition and imitation learning. However, their approach is hard to handle long formulae because the size of the DFA grows exponentially with the formula size. Since the size of most formulae in industrial datasets is more than 1k, we do not compare their approach with ours in our experiments. Vaezipoor et al. (2021) taught a deep reinforcement learning agent to follow instructions expressed in LTL in multi-task environments. They used relational graph convolutional network (R-GCN) [Schlichtkrull et al., 2018] to embed the parse tree for LTL formulae. Hahn et al. (2021) explored the ability of Transformer [Vaswani et al., 2017] to predict a trace satisfying the given LTL formula. They directly employed Transformer to encode the LTLf formulae in Polish notation and decode a satisfying trace. Since experimental results show the potential of neural networks in predicting a satisfying trace of LTLf formulae, they suggested that deep learning can already augment combinatorial approaches in automatic verification and the broader formal methods community [Hahn et al., 2021]. In comparison with Transformer and R-GCN in LTLf satisfiability checking, our proposed approach is shown to have more advantages in our experiments. Our superiority is probably due to the fact that our approach explicitly models permutation invariance and sequentiality, but Transformer and R-GCN do not.

3 Preliminaries

The syntax of LTLf for a finite set of atomic propositions P includes true (⊤), standard logical operators (conjunction (∧) and negation (¬)), and temporal logical operators (next (X) and until (U)), described as follows:

where p ∈ P ∪ {⊤} and φ, φ1, and φ2 are LTLf formulae. For brevity, we only consider the above fundamental operators in this paper. Operator disjunction (∨), weak next (N), release (R), eventually (F), and always (G) are commonly used, and can be defined as φ1 ∨ φ2 := ¬(¬φ1 ∧ ¬φ2), Nφ1 := ¬X⊤ ∨ Xφ1, φ1Rφ2 := ¬(¬φ1 U ¬φ2), Fφ1 := ⊤ U φ1, and Gφ1 := ¬(⊤ U ¬φ1) respectively. The sub-formula of an LTLf formula φ is defined as follows, where p ∈ P∪{⊤} and φ1, φ2 are LTLf formulae: (1) if φ = p, then p is sub-formula of φ; (2) if φ = ¬φ1, then ¬φ1 and the sub-formulae of φ1 are sub-formulae of φ; (3) if φ = φ1 ∧φ2, then φ1 ∧φ2, the subformulae of φ1, and the sub-formulae of φ2 are sub-formulae of φ; (4) if φ = Xφ1, then Xφ1 and the sub-formulae of φ1 are sub-formulae of φ; (5) if φ = φ1 U φ2, then φ1 U φ2, the subformulae of φ1, and the sub-formulae of φ2 are sub-formulae of φ. The set of sub-formulae of φ is denoted by sub(φ). The size of an LTLf formula φ is the number of logical operators and atomic propositions in φ, denoted by |φ|.

LTLf is interpreted over finite traces. An finite trace is represented in the form π = s0, s1, . . . , sn, where st ∈ 2P is a state at time t. For every state si of π and every p ∈ P, p holds if p ∈ si or ¬p holds otherwise. The traces mentioned in this paper are finite. The size of π is the number of states of π, denoted by |π|. πi denotes a sub-trace of π beginning from the state si. Let π is a trace and |π| = n. The satisfaction relation |= is defined as follows:

πi |= p iff p ∈ si πi |= ¬φ iff πi ̸|= φ πi |= φ1 ∧ φ2 iff πi |= φ1 and πi |= φ2 πi |= Xφ iff i < n and πi+1 |= φ πi |= φ1 U φ2 iff ∃i ≤ k ≤ n, πk |= φ2 and ∀i ≤ j < k, πj |= φ1.

where φ, φ1, φ2 are LTLf formulae, and p ∈ P ∪ {⊤}. An LTLf formula φ is satisfiable if and only if there is a trace π such that π0 |= ϕ; otherwise it is satisfiable.

In this paper, we focus on the task of LTLf satisfiability checking. Its input is an LTLf formula φ and the output is a binary classification predicting whether φ is satisfiable or unsatisfiable. For example, given an LTLf formula (west ∨ north) U door, it is satisfiable because there is a trace such that west ∨ north is true until the door is true. In contrast, ((west ∨ north) U door) ∧ G¬door is unsatisfiable because door being always false (G¬door) contradicts door being true in the future ((west ∨ north) U door)).

4 Approach

The core neural network of our approach is named LTLfNet. Overall, LTLfNet first embeds a given LTLf formula, then uses the embedding to perform a binary classification (satisfiable or unsatisfiable). In order to capture the syntactic features and handle formulae of any size, we employ the general framework of recursive neural networks (TreeNN) [Socher et al., 2011] to embed the syntax tree of a given LTLf formula. The syntax tree of LTLf formula is defined as follows. An example of syntax tree is shown in Figure 1.

Definition 1. Let φ be an LTLf formula. Its syntax tree Gφ is a four-tuple (Vφ, Eφ, rφ, Lφ) defined as follows, where Vφ is a set of vertices, rφ ∈ Vφ is the root vertex, Eφ ⊆ Vφ ×Vφ is a set of undirected edges, and Lφ : Vφ → {⊤} ∪ P ∪ {¬, ∧, X,U}. Vφ and Eφ are initialized as {vφ} and ∅, respectively. rφ = vφ. For each sub-formula φi ∈ sub(φ), Vφ, Eφ, and Lφ are constructed as follows:

• if φi = p, then Lφ(φi) = p;
• if φi = o1 φj, then Vφ = Vφ ∪ {vφj }, Eφ = Eφ ∪ {(vφi , vφj )}, and Lφ(φi) = o1;
• if φi = φj o2 φk, then Vφ = Vφ ∪ {vφj , vφk }, Eφ = Eφ ∪ {(vφi , vφj ) , (vφi , vφk )}, and Lφ(φi) = o2,

where p ∈ P ∪ {⊤}, o1 ∈ {¬, X}, o2 ∈ {∧, U}, and φj, φk are LTLf formulae.

Algorithm 1: LTLFEMBEDDING

Input : a syntax tree (Vφ,Eφ, rφ, Lφ) of φ and current vertex rφi . Output : the embedding rφi of φi. 1 if Lφ(rφi ) = p, where p ∈ P∪ {⊤} then 2 rφi ←ONE-HOTEMBEDDING(p) 3 else if Lφ(rφi ) = op1, where op1 ∈ {¬, X} then 4 get rφj ∈ Vφ s.t. (rφi , rφj ) ∈ Eφ 5 rφj ←LTLFEMBEDDING((Vφ, Eφ, rφ, Lφ),rφj ) 6 rφi ←COMBINE(rφj ,op1) 7 else 8 get rφj , rφk ∈ Vφ s.t. (rφi , rφj ) , (rφi , rφk ) ∈ Eφ 9 rφj ←LTLFEMBEDDING((Vφ, Eφ, rφ, Lφ),rφj ) 10 rφk ←LTLFEMBEDDING((Vφ, Eφ, rφ, Lφ),rφk ) 11 if Lφ(rφ) = ∧ then 12 rφi ←COMBINE(MP(rφj ,rφk ),∧) 13 else /* φ = φi U φk */ 14 rφi ←COMBINE([rφi , rφj ],U) 15 return rφ

Algorithm 1 shows the pseudo-code of embedding LTLf formulae. LTLFEMBEDDING learns embeddings of subformula for each vertex in the syntax tree by recursively combining and aggregating the embeddings of its sub-formulae using a neural network. If the sub-formula is an atomic proposition or ⊤, we use a one-hot vector rp ∈ Rdm (line 2 of Algorithm 1). Otherwise, we perform the function COMBINE with different learnable parameters for different logical operators. The pseudo-code of COMBINE is shown in Algorithm 2. We use a two-layer multilayer perceptron (MLP) with a residual-like connection to compute the combination representation of sub-formulae, which is the same as the work [Allamanis et al., 2017]. Note that the dimensions of W0,op,W1,op,W2,op are different from each other and related to the array of the operators.

Algorithm 2: COMBINE

Input : an aggregated representation r of sub-formulae and the logical operator op.

Output : the combination representation rout.

1 r′ ←ReLU(W0,op · r)

• 3 return rout/‖rout‖2

We define aggregation function for each operator fulfilling permutation invariance or sequentiality as follows.

• Permutation invariance. If a formula and its subformulae are connected by an unary operator (line 6 of Algorithm1) or the ∧ operator (line 12 of Algorithm 1), we aggregate the embeddings of sub-formulae by performing a mean pooling (MP).
• Sequentiality. If they are connected by the U operator (line 14 of Algorithm 1), we aggregate the embeddings of sub-formulae by concatenating them.

Given an LTLf formula φ, LTLfNet computes the probability ˆ yφ for φ being satisfiable as follow:

where MLPsat is an MLP. We train LTLfNet to minimize the sigmoid cross-entropy loss between ˆ yφ and the ground truth yφ, where yφ = 1 if φ is satisfiable; yφ = 0 otherwise.

5 Evaluation and Analysis

In this section, we conduct a comprehensive evaluation among different approaches for LTLf satisfiability checking on a large amount of datasets 1 .

5.1 Dataset

Synthetic dataset. In order to generate synthetic datasets, we used the randltl tool in the SPOT framework 2 to generate random formulae. The tool can generate unique formulae following a specified symbol distribution (P, ⊤, ⊥, standard logical operators, and temporal logical operators) in a specified size interval. Our symbol distribution sets weights to: P

1 Our code and benchmarks are publicly available at https:// github.com/wanderer0205/LTLfNet.

2 SPOT is available in https://spot.lrde.epita.fr/.

2.5, ⊤ 1, ⊥ 1, ¬ 1, ∨ 1, X 1, and U 1. The propositions in P obey the uniform distribution.

We generate synthetic datasets where the formula size is in the interval [20, 100) and the number of different atomic propositions is less than 100 for every formula. The synthetic datasets include a training set with 16K formulae and a validation set with 2K formulae. Besides, we generate formulae and divide them into 6 test sets according to their size intervals: [20, 100), [100, 120), [120, 140), [140, 160), [160, 180), and [180, 200). For each test set, we randomly generate 2K formulae. We keep the balance of the number of satisfiable formulae and that of unsatisfiable formulae.

Following the evaluation of the work [Li et al., 2020], we also evaluate our approaches on large-scale datasets that are available so far, which have been used to evaluate symbolic approaches. These datasets are summarized as follows, where the latter two come from industries and generally have larger sizes than the former two.

LTL-as-LTLf . It consists of 4668 formulae coming from LTL satisfiability checking.

LTLf -Specific. It consists of 1700 formulae generated by common LTLf patterns.

NASA-Boeing. It consists of 63 real-world LTLf specifications used in the Boeing AIR 6110 wheelbraking system and the NASA NextGen air traffic control (ATC) system.

DECLARE. It consists of 112 LTLf patterns widely used in the business process management.

The distribution of NASA-Boeing and DECLARE and that of the synthetic datasets are different because they are realworld LTLf specifications.

5.2 Competitor

Our competitors include some neural approaches and some symbolic approaches. The details are shown as follows.

Transformer. We follow the work [Hahn et al., 2021]. Specifically, we use Transformer to encode an LTLf formula and take the embedding of '[CLS]' as the representation of the formula, where '[CLS]' is a special token meaning the beginning of the sentence in Transformer. Then we apply an MLP to the embedding of '[CLS]' to obtain the classification result. We use one-hot embeddings for atomic propositions and trainable embeddings for other tokens.

RGCN. We follow the work [Vaezipoor et al., 2021] to exploit R-GCN [Schlichtkrull et al., 2018] to encode LTLf formulae and then to apply an MLP to obtain the classification result. Every LTLf formula is represented as a directed graph by first creating the parse tree and then adding self-loops for all the nodes, where each sub-formula is connected to its parent operator via a directed edge. The edges in graph are divided into four types: 1. Self-loops, 2. Unary: the edges from the subformula of a unary operator to its parent node, 3. Binary left (resp. 4. Binary right): the edges from the left (resp. right) sub-formula of a binary operator to its parent node. We use one-hot (resp. trainable) embeddings for atomic propositions (resp. other tokens) as initialization. The graphs are fed into R-GCN to get the embeddings of the root node as the embeddings of LTLf formulae.

TreeNN. We follow TreeNN described in [Allamanis et al., 2017] to obtain the representation of LTLf formulae, where the "LOOKUPLEAFEMBEDDING" is set as one-hot embeddings. Different from our method, TreeNN does not apply different 'COMBINE' functions to different operators, thus it does not guarantee permutation invariance or ordering of operators to be kept.

CDLSC. It is a SOTA symbolic approach to LTLf satisfiability checking [Li et al., 2020]. CDLSC conducts LTLf satisfiability checking by reducing the problem to a path-search problem over the transition system constructed by iteratively solving certain Boolean SAT problems. Besides, it leverages information produced by SAT solving from both satisfiable and unsatisfiable results to speed up the checking.

nuXmv. It is one of the SOTA approaches to model checking [Cavada et al., 2014]. As LTL satisfiability checking is reducible to model checking, we can compare with nuXmv using the LTLf -to-LTL satisfiability-preserving reduction [Giacomo and Vardi, 2013].

5.3 Setup

We train all compared neural approaches with the Adam optimizer. The hyperparameters of these approaches are as follows. For Transformer, the number of heads is 4, the number of layers is 3, and the dimension of hidden layers is 256 in the encoder layer. The dimension of embeddings dm is 1024 and the classification layer is an MLP. The batch size is 512, the learning rate is 1e - 5, and the number of training epochs is 1000 with early stopping when the loss does not decrease for 30 epochs. For LTLfNet and TreeNN, the dimension of embeddings dm is 1024 and the classification layer is an MLP. The batch size is 128, the learning rate is 1e - 3, and the number of training epochs is 256 with early stopping when the loss does not decrease for 30 epochs. For RGCN, the dimension of embeddings dm is 1024, the dimension of the hidden layer in R-GCN is 32, and the classification layer is a two-layer MLP with the dimension of the hidden layer 128. The batch size is 128, the learning rate is 1e-3, and the number of training epochs is 256 with early stopping when the loss does not decrease for 30 epochs. The loss function of all these approaches is CrossEntropyLoss and the activation functions for all MLPs are ReLU. All experiments were conducted on a single GPU (NVIDIA A100).

We train all compared approaches on the synthetic datasets and directly test them on datasets with different formula sizes and different distributions. We use the accuracy (acc.), precision (pre.), recall (rec.) and F1 score (F1) of binary classification as the metrics to evaluate the performance.

5.4 Result

Evaluation on Synthetic Datasets

We omit the results of symbolic approaches in the synthetic datasets because they can solve all formulae very quickly. In Table 1, LTLfNet works best. TreeNN and LTLfNet significantly outperform Transformer and RGCN, because the model structures of TreeNN and LTLfNet are the same recursive structures as the parse tree of LTLf formulae, while Transformer only explicitly represents an ordered sequence of symbols and RGCN considers redundant additional edges. Compared with TreeNN, LTLfNet performs better especially on longer formulae as shown in Figure 2 because LTLfNet keeps the sequentiality of the U operator. It is worth to note that Transformer runs very quickly. Similar results are also reported by Table 2. This is due to the fact that Transformer is implemented by efficient parallel matrix operations.

As shown in Figure 2, the performance of Transformer and TreeNN drops sharply as the formulae become larger while that of RGCN and LTLfNet keeps steady. LTLfNet outperforms other approaches and keeps the high performance even when formulae become larger. It suggests that our approach has scale generalizability to a certain extent.

Evaluation on Large Scale Datasets

The results are shown in Table 2. It is occasional that some neural networks including ours have the same accuracy or F1. These occasional cases occur on relatively small datasets. In these cases, all compared neural approaches result in the same numbers of true positives, false positives, true negatives, and false negatives.

The neural approaches are much faster than the symbolic approaches generally. Particularly, the running time of the symbolic approaches is unacceptable on LTL-as-LTLf , NASA-Boeing, and DECLARE, although they guarantee the correctness. The results on the performance of neural approaches are surprising, such as the results on NASA-Boeing and DECLARE, which contain only satisfiable formulae. This shows that neural approaches are able to learn biases that are widely present in industrial datasets. LTLfNet achieves the best accuracy and F1 score on almost all the four datasets among all compared neural approaches while keeping a decent running time. These results confirm that LTLfNet achieves highly confident prediction for LTLf satisfiability checking in relatively short time.

All neural approaches were trained on the synthetic dataset and then tested in the industrial datasets. This way aims to evaluate the generalization ability of neural networks across distributions, which is useful for industrial instances where the distribution cannot be clarified and the number of data is small. However, we also notice that the generalization ability of neural networks is limited for different distributions of data, e.g., on the LTLf -Specific dataset. The development of an effective way to perform LTLf satisfiability checking across distributions is left in our future work.

6 Discussion

The scale of the sampling formulae. We check the satisfiability of formulae to label the ground truth using exact symbolic reasoning. Due to the high complexity (PSPACEcomplete) of LTLf satisfiability checking, the SOTA symbolic approach is time-consuming to check the formula with a large number of atomic propositions and long sizes, which is confirmed by the experimental results of CDLSC on DECLARE. In order to generate a large amount of data to train neural networks in an acceptable time, we sample the formulae whose size and the number of atomic propositions are less than 100 in the synthetic datasets.

Sparsity of unsatisfiable formulae. We discover that unsatisfiable formulae are sparse when generating random formulae via the technique described in Section 5.1. Specifically, we sample 50M formulae, of which there are only about 0.4M unsatisfiable formulae. In order to deal with long-tailed distributions, we balance the satisfiable and unsatisfiable instances in the synthetic datasets. Balanced and sufficient sampling of the minority class (unsatisfiable formulae) allows our approach to precisely characterize the boundary of unsatisfiable formulae. Making the boundary of unsatisfiable formulae precise also improves the performance for satisfiable formulae since our problem is a binary classification problem.

LTL satisfiability checking. Although LTL and LTLf have different semantics, they have the same set of logical constructs, including permutation invariance and sequentiality. Hence, as an approximate approach to LTLf satisfiability checking, our proposed approach can naturally be applied to LTL satisfiability checking.

Applicability. Our approach is practical as it is able to obtain a highly confident result of LTLf satisfiability checking in polynomial time. This makes our approach potentially applicable to some LTLf -SAT-heavy tasks, e.g., goalconflict identification [Degiovanni et al., 2018; Luo et al., 2021]. Our approach can act as a highly confident and efficient pre-identifier, which can not only increase the number of traversed solutions (thanks to the polynomial time complexity) but can also pre-screen candidates that are obviously not valid (thanks to the high confidence). Symbolic approaches can be used in post-processing to ensure soundness.

7 Conclusion and FutureWork

This paper is the first to teach an end-to-end neural network to check LTLf satisfiability. Our main motivation is to explore a new solving paradigm for LTLf satisfiability checking, a symbolic reasoning problem in PSPACE-complete, to improve the SOTA. Combining symbolic reasoning of LTLf with continuous neural reasoning is a grand challenge. Our work has established that, by designing the neural architecture (LTLfNet) to characterize syntactic features and semantic features (permutation invariance and sequentiality) of LTLf , neural networks can learn to distinguish the satisfiable and unsatisfiable instances in LTLf and can generalize across large-scale datasets. Moreover, the experimental results show the competitive results of LTLfNet compared with the SOTA symbolic approaches. Our work makes it possible to obtain a highly confident result of LTLf satisfiability checking in polynomial time, which has great implications for some LTLf -SAT-heavy tasks.

Our future work will improve our approach to generalize across distributions, evaluate our approach in LTL satisfiability checking, and extend our approach to generate a trace as evidence of satisfiability.

Acknowledgments

We thank anonymous referees for their helpful comments. This paper was supported by the National Natural Science Foundation of China (No. 61976232 and 61876204), Guangdong Basic and Applied Basic Research Foundation (No.2022A1515011355 and 2020A1515010642), Guizhou Science Support Project (No. 2022-259), Humanities and Social Science Research Project of Ministry of Education (18YJCZH006).