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.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.