LTLf2ASP: LTLf Bounded Satisfiability in ASP
摘要
Finite variant of Linear Temporal Logic (LTL \(_\text {f}\) ) is increasingly popular in Artificial Intelligence (AI).Indeed, several AI applications rely on checking the satisfiability of temporal specifications expressed in LTL \(_\text {f}\) (e.g., planning, and model-checking). This paper describes ltlf2asp, an ASP-based system for bounded satisfiability checking of LTL \(_\text {f}\) 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 LTL \(_\text {f}\) formulae.