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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

LTLf2ASP: LTLf Bounded Satisfiability in ASP

  • Valeria Fionda,
  • Antonio Ielo,
  • Francesco Ricca

摘要

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.