{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T18:04:10Z","timestamp":1778349850875,"version":"3.51.4"},"reference-count":55,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2024,3,15]],"date-time":"2024-03-15T00:00:00Z","timestamp":1710460800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,3,15]],"date-time":"2024-03-15T00:00:00Z","timestamp":1710460800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100008815","name":"Libera Universit\u00e0 di Bolzano","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100008815","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2024,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p><jats:italic>Linear temporal logic<\/jats:italic>(<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{LTL}\\,$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>LTL<\/mml:mi><mml:mspace\/><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>) and its variant interpreted on<jats:italic>finite traces<\/jats:italic>(<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{LTL}_{\\textsf{f}\\,}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:msub><mml:mi>LTL<\/mml:mi><mml:mrow><mml:mi>f<\/mml:mi><mml:mspace\/><\/mml:mrow><\/mml:msub><\/mml:math><\/jats:alternatives><\/jats:inline-formula>) are among the most popular specification languages in the fields of formal verification, artificial intelligence, and others. In this paper, we focus on the satisfiability problem for<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{LTL}\\,$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>LTL<\/mml:mi><mml:mspace\/><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>and<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{LTL}_{\\textsf{f}\\,}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:msub><mml:mi>LTL<\/mml:mi><mml:mrow><mml:mi>f<\/mml:mi><mml:mspace\/><\/mml:mrow><\/mml:msub><\/mml:math><\/jats:alternatives><\/jats:inline-formula>formulas, for which many techniques have been devised during the last decades. Among these are<jats:italic>tableau systems<\/jats:italic>, of which the most recent is Reynolds\u2019 tree-shaped tableau. We provide a SAT-based algorithm for<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{LTL}\\,$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>LTL<\/mml:mi><mml:mspace\/><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>and<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{LTL}_{\\textsf{f}\\,}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:msub><mml:mi>LTL<\/mml:mi><mml:mrow><mml:mi>f<\/mml:mi><mml:mspace\/><\/mml:mrow><\/mml:msub><\/mml:math><\/jats:alternatives><\/jats:inline-formula>satisfiability checking based on Reynolds\u2019 tableau, proving its correctness and discussing experimental results obtained through its implementation in the BLACK satisfiability checker.<\/jats:p>","DOI":"10.1007\/s10817-023-09691-1","type":"journal-article","created":{"date-parts":[[2024,3,15]],"date-time":"2024-03-15T16:01:51Z","timestamp":1710518511000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["SAT Meets Tableaux for Linear Temporal Logic Satisfiability"],"prefix":"10.1007","volume":"68","author":[{"given":"Luca","family":"Geatti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicola","family":"Gigante","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Angelo","family":"Montanari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gabriele","family":"Venturato","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,3,15]]},"reference":[{"key":"9691_CR1","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1016\/j.entcs.2009.02.036","volume":"231","author":"P Abate","year":"2009","unstructured":"Abate, P., Gor\u00e9, R., Widmann, F.: An on-the-fly tableau-based decision procedure for PDL-satisfiability. Electron. Notes Theor. Comput. Sci. 231, 191\u2013209 (2009). https:\/\/doi.org\/10.1016\/j.entcs.2009.02.036","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"1\u20132","key":"9691_CR2","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1023\/A:1018985923441","volume":"22","author":"F Bacchus","year":"1998","unstructured":"Bacchus, F., Kabanza, F.: Planning for temporally extended goals. Ann. Math. Artif. Intell. 22(1\u20132), 5\u201327 (1998)","journal-title":"Ann. Math. Artif. Intell."},{"key":"9691_CR3","doi-asserted-by":"publisher","unstructured":"Barbosa, H., Barrett, C.W., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., N\u00f6tzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: a versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems-28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I, Lecture Notes in Computer Science, vol. 13243, pp. 415\u2013442. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"9691_CR4","unstructured":"Bertello, M., Gigante, N., Montanari, A., Reynolds, M.: Leviathan: a new LTL satisfiability checking tool based on a one-pass tree-shaped tableau. In: Proceedings of the 25th International Joint Conference on Artificial Intelligence, pp. 950\u2013956. IJCAI\/AAAI Press (2016)"},{"issue":"54","key":"9691_CR5","first-page":"311","volume":"14","author":"EW Beth","year":"1959","unstructured":"Beth, E.W.: Semantic entailment and formal derivability. Sapientia 14(54), 311 (1959)","journal-title":"Sapientia"},{"key":"9691_CR6","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 117\u2013148 (2003). https:\/\/doi.org\/10.1016\/S0065-2458(03)58003-2","journal-title":"Adv. Comput."},{"key":"9691_CR7","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-2(5:5)2006","author":"A Biere","year":"2006","unstructured":"Biere, A., Heljanko, K., Junttila, T.A., Latvala, T., Schuppan, V.: Linear encodings of bounded LTL model checking. Log. Methods Comput. Sci. (2006). https:\/\/doi.org\/10.2168\/LMCS-2(5:5)2006","journal-title":"Log. Methods Comput. Sci."},{"key":"9691_CR8","doi-asserted-by":"publisher","unstructured":"Brafman, R.I., De Giacomo, G.: Planning for LTLf\/LDLf goals in non-markovian fully observable nondeterministic domains. In: Kraus, S. (ed.) Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, pp. 1602\u20131608 (2019). https:\/\/doi.org\/10.24963\/ijcai.2019\/222","DOI":"10.24963\/ijcai.2019\/222"},{"key":"9691_CR9","doi-asserted-by":"crossref","unstructured":"Brafman, R.I., De Giacomo, G., Patrizi, F.: LTLf\/LDLf non-markovian rewards. In: S.A. McIlraith, K.Q. Weinberger (eds.) Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, pp. 1771\u20131778. AAAI Press (2018)","DOI":"10.1609\/aaai.v32i1.11572"},{"key":"9691_CR10","doi-asserted-by":"publisher","unstructured":"Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: Computer Aided Verification, pp. 334\u2013342. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"9691_CR11","doi-asserted-by":"crossref","unstructured":"Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: Proceedings of the 26th International Conference on Computer Aided Verification, pp. 334\u2013342. Springer (2014)","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"9691_CR12","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Roveri, M., Sheridan, D.: Bounded verification of past LTL. In: Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design, pp. 245\u2013259. Springer (2004)","DOI":"10.1007\/978-3-540-30494-4_18"},{"key":"9691_CR13","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Roveri, M., Sheridan, D.: Bounded Verification of Past LTL. In: Formal Methods in Computer-Aided Design, LNCS, pp. 245\u2013259. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-30494-4_18","DOI":"10.1007\/978-3-540-30494-4_18"},{"key":"9691_CR14","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, vol. 7795, pp. 93\u2013107. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"9691_CR15","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50026-6","volume-title":"Model Checking","author":"EM Clarke","year":"2001","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2001)"},{"key":"9691_CR16","unstructured":"De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: Rossi, F. (ed.) Proceedings of the 23rd International Joint Conference on Artificial Intelligence, pp. 854\u2013860. IJCAI\/AAAI (2013)"},{"key":"9691_CR17","doi-asserted-by":"publisher","unstructured":"De Giacomo, G., De Masellis, R., Grasso, M., Maggi, F.M., Montali, M.: Monitoring business metaconstraints based on LTL and LDL for finite traces. In: Sadiq, S.W., Soffer, P., V\u00f6lzer, H. (eds.) Proceedings of the 12th International Conference on Business Process Management, Lecture Notes in Computer Science, vol. 8659, pp. 1\u201317. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-10172-9_1","DOI":"10.1007\/978-3-319-10172-9_1"},{"key":"9691_CR18","unstructured":"De Giacomo, G., Vardi, M.Y.: Synthesis for LTL and LDL on finite traces. In: Yang, Q., Wooldridge, M.J. (eds.) Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, pp. 1558\u20131564. AAAI Press (2015)"},{"key":"9691_CR19","doi-asserted-by":"crossref","unstructured":"De Giacomo, G., Iocchi, L., Favorito, M., Patrizi, F.: Foundations for restraining bolts: Reinforcement learning with LTLf\/LDLf restraining specifications. In: Benton, J., Lipovetzky, N., Onaindia, E., Smith, D.E., Srivastava, S. (eds.) Proceedings of the Twenty-Ninth International Conference on Automated Planning and Scheduling, pp. 128\u2013136. AAAI Press (2019)","DOI":"10.1609\/icaps.v29i1.3549"},{"key":"9691_CR20","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, vol. 4963, pp. 337\u2013340. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9691_CR21","doi-asserted-by":"publisher","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible sat-solver. In: Selected Revised Papers of the 6th International Conference on Theory and Applications of Satisfiability Testing, pp. 502\u2013518 (2003). https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"9691_CR22","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible sat-solver. In: International conference on theory and applications of satisfiability testing, pp. 502\u2013518. Springer (2003)","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"9691_CR23","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1613\/jair.1.11256","volume":"63","author":"V Fionda","year":"2018","unstructured":"Fionda, V., Greco, G.: LTL on finite and process traces: complexity results and a practical reasoner. J. Artif. Intell. Res. 63, 557\u2013623 (2018). https:\/\/doi.org\/10.1613\/jair.1.11256","journal-title":"J. Artif. Intell. Res."},{"key":"9691_CR24","unstructured":"Fisher, M.: A resolution method for temporal logic. In: Mylopoulos, J., Reiter, R. (eds.) Proceedings of the 12th International Joint Conference on Artificial Intelligence, pp. 99\u2013104. Morgan Kaufmann (1991)"},{"issue":"4","key":"9691_CR25","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1093\/logcom\/7.4.429","volume":"7","author":"M Fisher","year":"1997","unstructured":"Fisher, M.: A normal form for temporal logics and its applications in theorem-proving and execution. J. Logic Comput. 7(4), 429\u2013456 (1997). https:\/\/doi.org\/10.1093\/logcom\/7.4.429","journal-title":"J. Logic Comput."},{"key":"9691_CR26","doi-asserted-by":"publisher","unstructured":"Geatti, L., Gigante, N., Montanari, A., Reynolds, M.: One-pass and tree-shaped tableau systems for TPTL and TPTLb+Past. In: Orlandini, A., Zimmermann, M. (eds.) Proceedings 9th International Symposium on Games, Automata, Logics, and Formal Verification, EPTCS, vol. 277, pp. 176\u2013190 (2018). https:\/\/doi.org\/10.4204\/EPTCS.277.13","DOI":"10.4204\/EPTCS.277.13"},{"key":"9691_CR27","doi-asserted-by":"publisher","unstructured":"Geatti, L., Gigante, N., Montanari, A.: A SAT-Based encoding of the one-pass and tree-shaped tableau system for LTL. In: Cerrito, S., Popescu, A. (eds.) Proceedings of the 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Lecture Notes in Computer Science, vol. 11714, pp. 3\u201320. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-29026-9_1","DOI":"10.1007\/978-3-030-29026-9_1"},{"key":"9691_CR28","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2020.104599","volume":"278","author":"L Geatti","year":"2021","unstructured":"Geatti, L., Gigante, N., Montanari, A., Reynolds, M.: One-pass and tree-shaped tableau systems for TPTL and TPTL${}_{\\text{ b }}Past. Inf. Comput. 278, 104599 (2021). https:\/\/doi.org\/10.1016\/j.ic.2020.104599","journal-title":"Inf. Comput."},{"key":"9691_CR29","unstructured":"Geatti, L., Gigante, N., Montanari, A., Venturato, G.: Past matters: Supporting LTL+Past in the BLACK satisfiability checker. In: Proceedings of the 28th International Symposium on Temporal Representation and Reasoning (2021)"},{"key":"9691_CR30","doi-asserted-by":"publisher","unstructured":"Geatti, L., Gianola, A., Gigante, N.: Linear temporal logic modulo theories over finite traces. In: L.D. Raedt (ed.) Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI 2022, Vienna, Austria, 23\u201329 July 2022, pp. 2641\u20132647. ijcai.org (2022). https:\/\/doi.org\/10.24963\/ijcai.2022\/366","DOI":"10.24963\/ijcai.2022\/366"},{"key":"9691_CR31","doi-asserted-by":"crossref","unstructured":"Gigante, N., Montanari, A., Reynolds, M.: A one-pass tree-shaped tableau for LTL+Past. In: Proc. of 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, EPiC Series in Computing, vol. 46, pp. 456\u2013473 (2017)","DOI":"10.29007\/3hb9"},{"key":"9691_CR32","doi-asserted-by":"crossref","unstructured":"Heljanko, K., Junttila, T., Latvala, T.: Incremental and complete bounded model checking for full PLTL. In: Proceedings of the 17th International Conference on Computer Aided Verification, pp. 98\u2013111. Springer (2005)","DOI":"10.1007\/11513988_10"},{"key":"9691_CR33","doi-asserted-by":"publisher","unstructured":"Hustadt, U., Konev, B.: TRP++2.0: A temporal resolution prover. In: Proceedings of the 19th International Conference on Automated Deduction, LNCS, vol. 2741, pp. 274\u2013278. Springer (2003). https:\/\/doi.org\/10.1007\/978-3-540-45085-6_21","DOI":"10.1007\/978-3-540-45085-6_21"},{"key":"9691_CR34","unstructured":"Hustadt, U., Nalon, C., Dixon, C.: Evaluating pre-processing techniques for the separated normal form for temporal logics. In: B.\u00a0Konev, J.\u00a0Urban, P.\u00a0R\u00fcmmer (eds.) Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning co-located with Federated Logic Conference 2018 (FLoC 2018), Oxford, UK, July 19th, 2018, CEUR Workshop Proceedings, vol. 2162, pp. 34\u201348. CEUR-WS.org (2018)"},{"key":"9691_CR35","doi-asserted-by":"publisher","unstructured":"Kesten, Y., Manna, Z., McGuire, H., Pnueli, A.: A decision algorithm for full propositional temporal logic. In: Proc. of the 5th International Conference on Computer Aided Verification, LNCS, vol. 697, pp. 97\u2013109. Springer (1993). https:\/\/doi.org\/10.1007\/3-540-56922-7_9","DOI":"10.1007\/3-540-56922-7_9"},{"key":"9691_CR36","doi-asserted-by":"publisher","unstructured":"Li, J., Yao, Y., Pu, G., Zhang, L., He, J.: Aalta: an LTL satisfiability checker over infinite\/finite traces. In: Cheung, S., Orso, A., Storey, M.D. (eds.) Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 731\u2013734. ACM (2014). https:\/\/doi.org\/10.1145\/2635868.2661669","DOI":"10.1145\/2635868.2661669"},{"issue":"2","key":"9691_CR37","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/s10703-018-00326-5","volume":"54","author":"J Li","year":"2019","unstructured":"Li, J., Zhu, S., Pu, G., Zhang, L., Vardi, M.Y.: Sat-based explicit LTL reasoning and its application to satisfiability checking. Formal Methods Syst. Des. 54(2), 164\u2013190 (2019). https:\/\/doi.org\/10.1007\/s10703-018-00326-5","journal-title":"Formal Methods Syst. Des."},{"key":"9691_CR38","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2020.103369","volume":"289","author":"J Li","year":"2020","unstructured":"Li, J., Pu, G., Zhang, Y., Vardi, M.Y., Rozier, K.Y.: Sat-based explicit LTLF satisfiability checking. Artif. Intell. 289, 103369 (2020). https:\/\/doi.org\/10.1016\/j.artint.2020.103369","journal-title":"Artif. Intell."},{"issue":"1","key":"9691_CR39","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1093\/jigpal\/8.1.55","volume":"8","author":"O Lichtenstein","year":"2000","unstructured":"Lichtenstein, O., Pnueli, A.: Propositional temporal logics: decidability and completeness. Logic J. IGPL 8(1), 55\u201385 (2000). https:\/\/doi.org\/10.1093\/jigpal\/8.1.55","journal-title":"Logic J. IGPL"},{"key":"9691_CR40","doi-asserted-by":"publisher","unstructured":"Lichtenstein, O., Pnueli, A., Zuck, L.D.: The Glory of the Past. In: Procedings of the Logics of Programs Conference, LNCS, vol. 193, pp. 196\u2013218. Springer (1985). https:\/\/doi.org\/10.1007\/3-540-15648-8_16","DOI":"10.1007\/3-540-15648-8_16"},{"key":"9691_CR41","first-page":"122","volume":"79","author":"N Markey","year":"2003","unstructured":"Markey, N.: Temporal logic with past is exponentially more succinct. Bull. EATCS 79, 122\u2013128 (2003)","journal-title":"Bull. EATCS"},{"key":"9691_CR42","doi-asserted-by":"crossref","unstructured":"McCabe-Dansted, J.C., Reynolds, M.: A parallel linear temporal logic tableau. In: Bouyer, P., Orlandini, A., Pietro, P.S. (eds.) Proceedings of the 8th International Symposium on Games, Automata, Logics and Formal Verification, EPTCS, vol. 256, pp. 166\u2013179 (2017)","DOI":"10.4204\/EPTCS.256.12"},{"key":"9691_CR43","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient sat solver. In: Proceedings of the 38th annual Design Automation Conference, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"9691_CR44","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The Temporal Logic of Programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science, pp. 46\u201357. IEEE Computer Society (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"9691_CR45","doi-asserted-by":"publisher","unstructured":"Reynolds, M.: A New Rule for LTL Tableaux. In: Proceedings of the 7th International Symposium on Games, Automata, Logics and Formal Verification, EPTCS, vol. 26, pp. 287\u2013301 (2016). https:\/\/doi.org\/10.4204\/EPTCS.226.20","DOI":"10.4204\/EPTCS.226.20"},{"key":"9691_CR46","doi-asserted-by":"crossref","unstructured":"Schuppan, V., Darmawan, L.: Evaluating LTL satisfiability solvers. In: Proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis, pp. 397\u2013413 (2011)","DOI":"10.1007\/978-3-642-24372-1_28"},{"key":"9691_CR47","doi-asserted-by":"publisher","unstructured":"Schwendimann, S.: A new one-pass tableau calculus for PLTL. In: Proceedings of the 7th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, LNCS, vol. 1397, pp. 277\u2013292. Springer (1998). https:\/\/doi.org\/10.1007\/3-540-69778-0_28","DOI":"10.1007\/3-540-69778-0_28"},{"issue":"3","key":"9691_CR48","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"AP Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733\u2013749 (1985). https:\/\/doi.org\/10.1145\/3828.3837","journal-title":"J. ACM"},{"key":"9691_CR49","doi-asserted-by":"publisher","unstructured":"Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: O.\u00a0Kullmann (ed.) Proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing, Lecture Notes in Computer Science, vol. 5584, pp. 244\u2013257. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-02777-2_24","DOI":"10.1007\/978-3-642-02777-2_24"},{"key":"9691_CR50","doi-asserted-by":"publisher","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: Starexec: A cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) Automated Reasoning\u20147th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19\u201322, 2014. Proceedings, Lecture Notes in Computer Science, vol. 8562, pp. 367\u2013373. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_28","DOI":"10.1007\/978-3-319-08587-6_28"},{"key":"9691_CR51","doi-asserted-by":"publisher","unstructured":"Suda, M., Weidenbach, C.: A PLTL-prover based on labelled superposition with partial model guidance. In: Proceedings of the 6th International Joint Conference on Automated Reasoning, LNCS, vol. 7364, pp. 537\u2013543. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_42","DOI":"10.1007\/978-3-642-31365-3_42"},{"key":"9691_CR52","unstructured":"Tahrat, S., Braun, G., Artale, A., Ozaki, A.: Abstracting temporal aboxes in TDL-Lite. In: Proceedings of the 34th International Workshop on Description Logics (2021)"},{"issue":"1","key":"9691_CR53","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/s100090200070","volume":"4","author":"H Tauriainen","year":"2002","unstructured":"Tauriainen, H., Heljanko, K.: Testing LTL formula translation into B\u00fcchi automata. Int. J. Softw. Tools Technol. Transf. 4(1), 57\u201370 (2002). https:\/\/doi.org\/10.1007\/s100090200070","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"1\/2","key":"9691_CR54","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P Wolper","year":"1983","unstructured":"Wolper, P.: Temporal logic can be more expressive. Inf. Control 56(1\/2), 72\u201399 (1983). https:\/\/doi.org\/10.1016\/S0019-9958(83)80051-5","journal-title":"Inf. Control"},{"key":"9691_CR55","first-page":"119","volume":"28","author":"P Wolper","year":"1985","unstructured":"Wolper, P.: The tableau method for temporal logic: an overview. Logique et Analyse 28, 119\u2013136 (1985)","journal-title":"Logique et Analyse"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-023-09691-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-023-09691-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-023-09691-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,14]],"date-time":"2024-11-14T11:21:03Z","timestamp":1731583263000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-023-09691-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,3,15]]},"references-count":55,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,6]]}},"alternative-id":["9691"],"URL":"https:\/\/doi.org\/10.1007\/s10817-023-09691-1","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,3,15]]},"assertion":[{"value":"11 March 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 December 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 March 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests affecting this manuscript.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing Interests"}}],"article-number":"6"}}