TY - GEN
T1 - Achieving completeness in bounded model checking of action theories in ASP
AU - Giordano, Laura
AU - Martelli, Alberto
AU - Dupré, Daniele Theseider
PY - 2012
Y1 - 2012
N2 - 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 Büchi 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.
AB - 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 Büchi 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.
UR - https://www.scopus.com/pages/publications/84893423427
M3 - Conference contribution
AN - SCOPUS:84893423427
SN - 9781577355601
T3 - Proceedings of the International Conference on Knowledge Representation and Reasoning
SP - 618
EP - 622
BT - 13th International Conference on the Principles of Knowledge Representation and Reasoning, KR 2012
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 13th International Conference on the Principles of Knowledge Representation and Reasoning, KR 2012
Y2 - 10 June 2012 through 14 June 2012
ER -