{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T10:31:01Z","timestamp":1763202661040},"publisher-location":"California","reference-count":0,"publisher":"International Joint Conferences on Artificial Intelligence Organization","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022,7]]},"abstract":"<jats:p>Linear temporal logic over finite traces (LTLf) satisfiability checking is a fundamental and hard (PSPACE-complete) problem in the artificial intelligence community. We explore teaching end-to-end neural networks to check satisfiability in polynomial time. It is a challenge to characterize the syntactic and semantic features of LTLf via neural networks. To tackle this challenge, we propose LTLfNet, a recursive neural network that captures syntactic features of LTLf by recursively combining the embeddings of sub-formulae. LTLfNet models permutation invariance and sequentiality in the semantics of LTLf through different aggregation mechanisms of sub-formulae. Experimental results demonstrate that LTLfNet achieves good performance in synthetic datasets and generalizes across large-scale datasets. They also show that LTLfNet is competitive with state-of-the-art symbolic approaches such as nuXmv and CDLSC.<\/jats:p>","DOI":"10.24963\/ijcai.2022\/457","type":"proceedings-article","created":{"date-parts":[[2022,7,15]],"date-time":"2022-07-15T22:55:56Z","timestamp":1657925756000},"page":"3292-3298","source":"Crossref","is-referenced-by-count":6,"title":["Teaching LTLf Satisfiability Checking to Neural Networks"],"prefix":"10.24963","author":[{"given":"Weilin","family":"Luo","sequence":"first","affiliation":[{"name":"School of Computer Science and Engineering, Sun Yat-sen University, Guangzhou, China"}]},{"given":"Hai","family":"Wan","sequence":"additional","affiliation":[{"name":"School of Computer Science and Engineering, Sun Yat-sen University, Guangzhou, China"},{"name":"Key Laboratory of Machine Intelligence and Advanced Computing (Sun Yat-sen University), Ministry of Education, China"}]},{"given":"Jianfeng","family":"Du","sequence":"additional","affiliation":[{"name":"Guangdong University of Foreign Studies, Guangzhou, China"},{"name":"Pazhou Lab, Guangzhou, China"}]},{"given":"Xiaoda","family":"Li","sequence":"additional","affiliation":[{"name":"School of Computer Science and Engineering, Sun Yat-sen University, Guangzhou, China"}]},{"given":"Yuze","family":"Fu","sequence":"additional","affiliation":[{"name":"School of Computer Science and Engineering, Sun Yat-sen University, Guangzhou, China"}]},{"given":"Rongzhen","family":"Ye","sequence":"additional","affiliation":[{"name":"School of Computer Science and Engineering, Sun Yat-sen University, Guangzhou, China"}]},{"given":"Delong","family":"Zhang","sequence":"additional","affiliation":[{"name":"School of Computer Science and Engineering, Sun Yat-sen University, Guangzhou, China"}]}],"member":"10584","event":{"number":"31","sponsor":["International Joint Conferences on Artificial Intelligence Organization (IJCAI)"],"acronym":"IJCAI-2022","name":"Thirty-First International Joint Conference on Artificial Intelligence {IJCAI-22}","start":{"date-parts":[[2022,7,23]]},"theme":"Artificial Intelligence","location":"Vienna, Austria","end":{"date-parts":[[2022,7,29]]}},"container-title":["Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence"],"original-title":[],"deposited":{"date-parts":[[2022,7,18]],"date-time":"2022-07-18T07:09:49Z","timestamp":1658128189000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.ijcai.org\/proceedings\/2022\/457"}},"subtitle":[],"proceedings-subject":"Artificial Intelligence Research Articles","short-title":[],"issued":{"date-parts":[[2022,7]]},"references-count":0,"URL":"https:\/\/doi.org\/10.24963\/ijcai.2022\/457","relation":{},"subject":[],"published":{"date-parts":[[2022,7]]}}}