LTLf2ASP: LTLf Bounded Satisfiability in ASP

Finite variant of Linear Temporal Logic (LTLf) is increasingly popular in Artificial Intelligence (AI).Indeed, several AI applications rely on checking the satisfiability of temporal specifications expressed in LTLf (e.g., planning, and model-checking). This paper describes ltlf2asp, an ASP-based system for bounded satisfiability checking of LTLf formulae. The approach is based on a natural encoding in ASP of temporal operators that is inspired to SAT-based approaches. Experiments show that our system compares favourably to the state-of-the-art, and shows the ASP technology stack is a suitable alternative to SAT/SMT solvers for bounded satisfiability checking of LTLf formulae.