Treffer: Automata-based LTLf Satisfiability Checking via ASP

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.