{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T02:57:24Z","timestamp":1768273044778,"version":"3.49.0"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031742088","type":"print"},{"value":"9783031742095","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,10,9]],"date-time":"2024-10-09T00:00:00Z","timestamp":1728432000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,10,9]],"date-time":"2024-10-09T00:00:00Z","timestamp":1728432000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-74209-5_28","type":"book-chapter","created":{"date-parts":[[2024,10,11]],"date-time":"2024-10-11T06:01:44Z","timestamp":1728626504000},"page":"373-386","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["LTLf2ASP: LTLf Bounded Satisfiability in\u00a0ASP"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7018-1324","authenticated-orcid":false,"given":"Valeria","family":"Fionda","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0006-9644-7975","authenticated-orcid":false,"given":"Antonio","family":"Ielo","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8218-3178","authenticated-orcid":false,"given":"Francesco","family":"Ricca","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,10,9]]},"reference":[{"key":"28_CR1","volume-title":"Frontiers in Artificial Intelligence and Applications","author":"Handbook of Satisfiability","year":"2021","unstructured":"Handbook of Satisfiability: Frontiers in Artificial Intelligence and Applications, vol. 336, 2nd edn. IOS Press, Amsterdam (2021)","edition":"2"},{"issue":"1\u20132","key":"28_CR2","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1080\/11663081.2013.798985","volume":"23","author":"F Aguado","year":"2013","unstructured":"Aguado, F., Cabalar, P., Di\u00e9guez, M., P\u00e9rez, G., Vidal, C.: Temporal equilibrium logic: a survey. J. Appl. Non Class. Logics 23(1\u20132), 2\u201324 (2013)","journal-title":"J. Appl. Non Class. Logics"},{"issue":"1\u20132","key":"28_CR3","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":"28_CR4","doi-asserted-by":"publisher","first-page":"100556","DOI":"10.1016\/j.simpa.2023.100556","volume":"17","author":"A Berti","year":"2023","unstructured":"Berti, A., van Zelst, S.J., Schuster, D.: PM4Py: a process mining library for python. Softw. Impacts 17, 100556 (2023)","journal-title":"Softw. Impacts"},{"issue":"12","key":"28_CR5","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1145\/2043174.2043195","volume":"54","author":"G Brewka","year":"2011","unstructured":"Brewka, G., Eiter, T., Truszczynski, M.: Answer set programming at a glance. Commun. ACM 54(12), 92\u2013103 (2011)","journal-title":"Commun. ACM"},{"issue":"5","key":"28_CR6","doi-asserted-by":"publisher","first-page":"783","DOI":"10.1017\/S1471068420000307","volume":"20","author":"P Cabalar","year":"2020","unstructured":"Cabalar, P., Di\u00e9guez, M., Schaub, T., Schuhmann, A.: Towards metric temporal answer set programming. Theory Pract. Log. Program. 20(5), 783\u2013798 (2020)","journal-title":"Theory Pract. Log. Program."},{"key":"28_CR7","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-030-20528-7_19","volume-title":"LPNMR 2019","author":"P Cabalar","year":"2019","unstructured":"Cabalar, P., Kaminski, R., Morkisch, P., Schaub, T.: telingo = ASP + time. In: Balduccini, M., Lierler, Y., Woltran, S. (eds.) LPNMR 2019. LNCS, vol. 11481, pp. 256\u2013269. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-20528-7_19"},{"issue":"3\u20134","key":"28_CR8","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1017\/S1471068418000297","volume":"18","author":"P Cabalar","year":"2018","unstructured":"Cabalar, P., Kaminski, R., Schaub, T., Schuhmann, A.: Temporal answer set programming on finite traces. Theory Pract. Log. Program. 18(3\u20134), 406\u2013420 (2018)","journal-title":"Theory Pract. Log. Program."},{"key":"28_CR9","unstructured":"Calvanese, D., Giacomo, G.D., Vardi, M.Y.: Reasoning about actions and planning in LTL action theories. In: KR, pp. 593\u2013602 (2002)"},{"key":"28_CR10","doi-asserted-by":"crossref","unstructured":"Camacho, A., McIlraith, S.A.: Learning interpretable models expressed in linear temporal logic. In: ICAPS, pp. 621\u2013630. AAAI Press (2019)","DOI":"10.1609\/icaps.v29i1.3529"},{"key":"28_CR11","doi-asserted-by":"publisher","first-page":"101920","DOI":"10.1016\/j.is.2021.101920","volume":"107","author":"A Cecconi","year":"2022","unstructured":"Cecconi, A., Giacomo, G.D., Ciccio, C.D., Maggi, F.M., Mendling, J.: Measuring the interestingness of temporal logic behavioral specifications in process mining. Inf. Syst. 107, 101920 (2022)","journal-title":"Inf. Syst."},{"key":"28_CR12","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-031-08848-3_4","volume-title":"Process Mining Handbook","author":"CD Ciccio","year":"2022","unstructured":"Ciccio, C.D., Montali, M.: Declarative process specifications: reasoning, discovery, monitoring. In: van der Aalst, W.M.P., Carmona, J. (eds.) Process Mining Handbook. LNCS, vol. 448, pp. 108\u2013152. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-08848-3_4"},{"key":"28_CR13","doi-asserted-by":"publisher","first-page":"102347","DOI":"10.1016\/j.is.2024.102347","volume":"122","author":"C Corea","year":"2024","unstructured":"Corea, C., Kuhlmann, I., Thimm, M., Grant, J.: Paraconsistent reasoning for inconsistency measurement in declarative process specifications. Inf. Syst. 122, 102347 (2024)","journal-title":"Inf. Syst."},{"key":"28_CR14","doi-asserted-by":"crossref","unstructured":"Dodaro, C., Fionda, V., Greco, G.: LTL on weighted finite traces: Formal foundations and algorithms. In: IJCAI, pp. 2606\u20132612. ijcai.org (2022)","DOI":"10.24963\/ijcai.2022\/361"},{"key":"28_CR15","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: ICSE, pp. 411\u2013420. ACM (1999)","DOI":"10.1145\/302405.302672"},{"issue":"3","key":"28_CR16","first-page":"53","volume":"37","author":"E Erdem","year":"2016","unstructured":"Erdem, E., Gelfond, M., Leone, N.: Applications of answer set programming. AI Mag. 37(3), 53\u201368 (2016)","journal-title":"AI Mag."},{"issue":"2\u20133","key":"28_CR17","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/s13218-018-0548-6","volume":"32","author":"AA Falkner","year":"2018","unstructured":"Falkner, A.A., Friedrich, G., Schekotihin, K., Taupe, R., Teppan, E.C.: Industrial applications of answer set programming. K\u00fcnstliche Intell. 32(2\u20133), 165\u2013176 (2018)","journal-title":"K\u00fcnstliche Intell."},{"key":"28_CR18","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)","journal-title":"J. Artif. Intell. Res."},{"issue":"5","key":"28_CR19","first-page":"898","volume":"32","author":"V Fionda","year":"2020","unstructured":"Fionda, V., Guzzo, A.: Control-flow modeling with declare: Behavioral properties, computational complexity, and tools. IEEE TKDE 32(5), 898\u2013911 (2020)","journal-title":"IEEE TKDE"},{"issue":"2","key":"28_CR20","first-page":"137","volume":"19","author":"A Garro","year":"2006","unstructured":"Garro, A., Palopoli, L., Ricca, F.: Exploiting agents in e-learning and skills management context. AI Commun. 19(2), 137\u2013154 (2006)","journal-title":"AI Commun."},{"key":"28_CR21","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-29026-9_1","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"L Geatti","year":"2019","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.) TABLEAUX 2019. LNCS (LNAI), vol. 11714, pp. 3\u201320. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29026-9_1"},{"issue":"2","key":"28_CR22","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/s10817-023-09691-1","volume":"68","author":"L Geatti","year":"2024","unstructured":"Geatti, L., Gigante, N., Montanari, A., Venturato, G.: SAT meets tableaux for linear temporal logic satisfiability. J. Autom. Reason. 68(2), 6 (2024)","journal-title":"J. Autom. Reason."},{"key":"28_CR23","doi-asserted-by":"crossref","unstructured":"Gebser, M., Kaminski, R., Kaufmann, B., Schaub, T.: Answer Set Solving in Practice. Synthesis Lectures on Artificial Intelligence and Machine Learning. Morgan & Claypool Publishers, Williston (2012)","DOI":"10.1007\/978-3-031-01561-8"},{"issue":"1","key":"28_CR24","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1017\/S1471068418000054","volume":"19","author":"M Gebser","year":"2019","unstructured":"Gebser, M., Kaminski, R., Kaufmann, B., Schaub, T.: Multi-shot ASP solving with clingo. Theory Pract. Log. Program. 19(1), 27\u201382 (2019)","journal-title":"Theory Pract. Log. Program."},{"issue":"3\/4","key":"28_CR25","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/BF03037169","volume":"9","author":"M Gelfond","year":"1991","unstructured":"Gelfond, M., Lifschitz, V.: Classical negation in logic programs and disjunctive databases. New Gener. Comput. 9(3\/4), 365\u2013386 (1991)","journal-title":"New Gener. Comput."},{"key":"28_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-319-19069-3_6","volume-title":"Advanced Information Systems Engineering","author":"G De Giacomo","year":"2015","unstructured":"De Giacomo, G., Dumas, M., Maggi, F.M., Montali, M.: Declarative process modeling in BPMN. In: Zdravkovic, J., Kirikova, M., Johannesson, P. (eds.) CAiSE 2015. LNCS, vol. 9097, pp. 84\u2013100. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-19069-3_6"},{"key":"28_CR27","doi-asserted-by":"crossref","unstructured":"Giacomo, G.D., Maggi, F.M., Marrella, A., Sardi\u00f1a, S.: Computing trace alignment against declarative process models through planning. In: ICAPS, pp. 367\u2013375 (2016)","DOI":"10.1609\/icaps.v26i1.13783"},{"key":"28_CR28","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/10720246_18","volume-title":"Recent Advances in AI Planning","author":"G De Giacomo","year":"2000","unstructured":"De Giacomo, G., Vardi, M.Y.: Automata-theoretic approach to planning for temporally extended goals. In: Biundo, S., Fox, M. (eds.) ECP 1999. LNCS (LNAI), vol. 1809, pp. 226\u2013238. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10720246_18"},{"key":"28_CR29","unstructured":"Giacomo, G.D., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, 2013, pp. 854\u2013860. IJCAI\/AAAI (2013)"},{"issue":"4\u20135","key":"28_CR30","doi-asserted-by":"publisher","first-page":"641","DOI":"10.1017\/S1471068413000409","volume":"13","author":"L Giordano","year":"2013","unstructured":"Giordano, L., Martelli, A., Spiotta, M., Dupr\u00e9, D.T.: Business process verification with constraint temporal answer set programming. Theory Pract. Log. Program. 13(4\u20135), 641\u2013655 (2013)","journal-title":"Theory Pract. Log. Program."},{"key":"28_CR31","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"591","DOI":"10.1007\/978-3-642-04238-6_63","volume-title":"Logic Programming and Nonmonotonic Reasoning","author":"G Grasso","year":"2009","unstructured":"Grasso, G., Iiritano, S., Leone, N., Ricca, F.: Some DLV applications for knowledge management. In: Erdem, E., Lin, F., Schaub, T. (eds.) LPNMR 2009. LNCS (LNAI), vol. 5753, pp. 591\u2013597. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04238-6_63"},{"issue":"4\u20135","key":"28_CR32","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1017\/S1471068403001790","volume":"3","author":"K Heljanko","year":"2003","unstructured":"Heljanko, K., Niemel\u00e4, I.: Bounded LTL model checking with stable models. Theory Pract. Log. Program. 3(4\u20135), 519\u2013550 (2003)","journal-title":"Theory Pract. Log. Program."},{"key":"28_CR33","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-031-49299-0_3","volume-title":"ILP 2023","author":"A Ielo","year":"2023","unstructured":"Ielo, A., Law, M., Fionda, V., Ricca, F., Giacomo, G.D., Russo, A.: Towards ILP-based LTL f passive learning. In: Bellodi, E., Lisi, F.A., Zese, R. (eds.) ILP 2023. LNCS, vol. 14363, pp. 30\u201345. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-49299-0_3"},{"key":"28_CR34","unstructured":"Kuhlmann, I., Corea, C., Grant, J.: An ASP-based framework for solving problems related to declarative process specifications. In: NMR. CEUR Workshop Proceedings, vol.\u00a03464, pp. 129\u2013132. CEUR-WS.org (2023)"},{"key":"28_CR35","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/978-3-031-50974-2_30","volume-title":"BPM","author":"I Kuhlmann","year":"2023","unstructured":"Kuhlmann, I., Corea, C., Grant, J.: Non-automata based conformance checking of declarative process specifications based on ASP. In: De Weerdt, J., Pufahl, L. (eds.) BPM. LNCS, vol. 492, pp. 396\u2013408. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-50974-2_30"},{"key":"28_CR36","doi-asserted-by":"publisher","first-page":"103369","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)","journal-title":"Artif. Intell."},{"key":"28_CR37","unstructured":"Li, J., Zhang, L., Pu, G., Vardi, M.Y., He, J.: LTLf satisfiability checking. In: ECAI. Frontiers in Artificial Intelligence and Applications, vol.\u00a0263, pp. 513\u2013518. IOS Press (2014)"},{"key":"28_CR38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-24658-7","volume-title":"Answer Set Programming","author":"V Lifschitz","year":"2019","unstructured":"Lifschitz, V.: Answer Set Programming. Springer, Cham (2019)"},{"issue":"2","key":"28_CR39","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1017\/S1471068411000640","volume":"13","author":"M Manna","year":"2013","unstructured":"Manna, M., Ricca, F., Terracina, G.: Consistent query answering via ASP from different perspectives: theory and practice. Theory Pract. Log. Program. 13(2), 227\u2013252 (2013)","journal-title":"Theory Pract. Log. Program."},{"issue":"4","key":"28_CR40","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/s10601-013-9146-2","volume":"18","author":"A Morgado","year":"2013","unstructured":"Morgado, A., Heras, F., Liffiton, M.H., Planes, J., Marques-Silva, J.: Iterative and core-guided MaxSAT solving: a survey and assessment. Constraints An Int. J. 18(4), 478\u2013534 (2013)","journal-title":"Constraints An Int. J."},{"key":"28_CR41","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October\u20131 November 1977, pp. 46\u201357. IEEE Computer Society (1977)","DOI":"10.1109\/SFCS.1977.32"},{"issue":"4","key":"28_CR42","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1145\/1183278.1183279","volume":"7","author":"TC Son","year":"2006","unstructured":"Son, T.C., Baral, C., Nam, T.H., McIlraith, S.A.: Domain-dependent knowledge in answer set planning. ACM Trans. Comput. Log. 7(4), 613\u2013657 (2006)","journal-title":"ACM Trans. Comput. Log."},{"key":"28_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/978-3-030-91384-7_2","volume-title":"Model Checking, Synthesis, and Learning","author":"Y-K Tsay","year":"2021","unstructured":"Tsay, Y.-K., Vardi, M.Y.: From linear temporal logics to\u00a0B\u00fcchi automata: the\u00a0early and\u00a0simple principle. In: Olderog, E.-R., Steffen, B., Yi, W. (eds.) Model Checking, Synthesis, and Learning. LNCS, vol. 13030, pp. 8\u201340. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-91384-7_2"}],"container-title":["Lecture Notes in Computer Science","Logic Programming and Nonmonotonic Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-74209-5_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,11]],"date-time":"2025-01-11T17:03:44Z","timestamp":1736615024000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-74209-5_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,9]]},"ISBN":["9783031742088","9783031742095"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-74209-5_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,9]]},"assertion":[{"value":"9 October 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"LPNMR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Logic Programming and Nonmonotonic Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dallas, TX","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"lpnmr2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/lpnmr2024.demacs.unical.it","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}