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

Research output: Contribution to journalConference articlepeer-review

Abstract

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.

Original languageEnglish
Pages (from-to)176-190
Number of pages15
JournalCEUR Workshop Proceedings
Volume857
Publication statusPublished - 2012
Event9th Italian Convention on Computational Logic, CILC 2012 - Rome, Italy
Duration: 6 Jun 20127 Jun 2012

Fingerprint

Dive into the research topics of 'Verification of action theories in ASP: A complete bounded model checking approach'. Together they form a unique fingerprint.

Cite this