Linear Temporal Logic over finite traces (LTLf) stands as a prominent and highly valuable formalism with application in various areas, including AI, process mining, and model checking among many others. The key reasoning task for LTLf is satisfiability checking, which amounts to verifying whether an input formula admits temporal models. In this paper we propose a novel approach to satisfiability checking based on Answer Set Programming (ASP). The idea is to encode in an ASP program the search for a finite state automaton that recognizes (a subset of) the language of the LTLf formula given in input. An experimental analysis demonstrates the viability of our approach.

Cuteri, A., Mazzotta, G., Penaloza, R., Ricca, F. (2024). Automata-based LTLf Satisfiability Checking via ASP. In Proceedings of the International Workshop on Artificial Intelligence for Climate Change, Italian Workshop on Planning and Scheduling, RCRA Workshop on Experimental evaluation of algorithms for solving problems with combinatorial explosion, and SPIRIT Workshop on Strategies, Prediction, Interaction, and Reasoning in Italy (AI4CC-IPS-RCRA-SPIRIT 2024) co-located with 23rd International Conference of the Italian Association for Artificial Intelligence AIxIA 2024 (pp.142-145). CEUR-WS.

Automata-based LTLf Satisfiability Checking via ASP

Penaloza R.;
2024

Abstract

Linear Temporal Logic over finite traces (LTLf) stands as a prominent and highly valuable formalism with application in various areas, including AI, process mining, and model checking among many others. The key reasoning task for LTLf is satisfiability checking, which amounts to verifying whether an input formula admits temporal models. In this paper we propose a novel approach to satisfiability checking based on Answer Set Programming (ASP). The idea is to encode in an ASP program the search for a finite state automaton that recognizes (a subset of) the language of the LTLf formula given in input. An experimental analysis demonstrates the viability of our approach.
paper
Answer Set Programming; Linear Temporal Logic; Satisfiability Checking;
English
1st International Workshop on Artificial Intelligence for Climate Change, 12th Italian Workshop on Planning and Scheduling, 31st RCRA Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion, and SPIRIT Workshop on Strategies, Prediction, Interaction, and Reasoning in Italy, AI4CC-IPS-RCRA-SPIRIT 2024 - November 25-28th, 2024
2024
Aineto, D; De Benedictis, R; Maratea, M; Mittelmann, M; Monaco, G; Scala, E; Serafini, L; Serina, I; Spegni, F; Tosello, E; Umbrico, A; Vallati, M
Proceedings of the International Workshop on Artificial Intelligence for Climate Change, Italian Workshop on Planning and Scheduling, RCRA Workshop on Experimental evaluation of algorithms for solving problems with combinatorial explosion, and SPIRIT Workshop on Strategies, Prediction, Interaction, and Reasoning in Italy (AI4CC-IPS-RCRA-SPIRIT 2024) co-located with 23rd International Conference of the Italian Association for Artificial Intelligence AIxIA 2024
2024
3883
142
145
https://ceur-ws.org/Vol-3883/
open
Cuteri, A., Mazzotta, G., Penaloza, R., Ricca, F. (2024). Automata-based LTLf Satisfiability Checking via ASP. In Proceedings of the International Workshop on Artificial Intelligence for Climate Change, Italian Workshop on Planning and Scheduling, RCRA Workshop on Experimental evaluation of algorithms for solving problems with combinatorial explosion, and SPIRIT Workshop on Strategies, Prediction, Interaction, and Reasoning in Italy (AI4CC-IPS-RCRA-SPIRIT 2024) co-located with 23rd International Conference of the Italian Association for Artificial Intelligence AIxIA 2024 (pp.142-145). CEUR-WS.
File in questo prodotto:
File Dimensione Formato  
Cuteri-2024-CEUR-VoR.pdf

accesso aperto

Descrizione: This volume and its papers are published under the Creative Commons License Attribution 4.0 International (CC BY 4.0).
Tipologia di allegato: Publisher’s Version (Version of Record, VoR)
Licenza: Creative Commons
Dimensione 458.2 kB
Formato Adobe PDF
458.2 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10281/536221
Citazioni
  • Scopus 1
  • ???jsp.display-item.citation.isi??? ND
Social impact