AAAI Publications, Thirteenth International Conference on the Principles of Knowledge Representation and Reasoning

Font Size: 
Achieving Completeness in Bounded Model Checking of Action Theories in ASP
Laura Giordano, Alberto Martelli, Daniele Theseider Dupre'

Last modified: 2012-05-17


Temporal logics can be used in reasoning about actions for specifying constraints on domain descriptions and temporal properties to be verified. In this paper, we exploit Bounded Model Checking (BMC) techniques in the verification of Dynamic Linear Time Temporal Logic (DLTL) properties of an action theory, which is formulated in a temporal extension of Answer Set Programming (ASP). To achieve completeness, we propose an approach to BMC which exploits the Buechi automaton construction while searching for a counterexample. We provide an encoding in ASP of the temporal action domain and of Bounded Model Checking of DLTL formulas.


Temporal Logic, Bounded Model Checking, Action Theory Verification, Answer Set Programming

Full Text: PDF