Verification of action theories in ASP: A complete bounded model checking approach

Temporal logics are well suited for reasoning about actions, as they allow for the specification of domain descriptions including temporal constraints as well as for the verification of temporal properties of the domain. This paper focuses on the verification of action theories formulated in a temporal extension of answer set programming which combines ASP with a dynamic linear time temporal logic. The paper proposes an approach to bounded model checking (BMC) which exploits the Büchi automaton construction while searching for a counterexample, with the aim of achieving completeness. The paper provides an encoding in ASP of the temporal action domains and of BMC of DLTL formulas.