Italiano (Italian) English (Inglese)
Thursday, 14 December 2017

Technical Reports

Technical Report Details
Authors:Laura Giordano
Alberto Martelli
Daniele Theseider Dupré
Scientific Area:Knowledge Representation
Logic-Based Reasoning
Temporal Reasoning
Title:Achieving completeness in bounded model checking of action theories in ASP
Published on:TR-INF-2011-12-04-UNIPMN
Publisher:Computer Science Department, UPO
Year:2011
URL:http://www.di.unipmn.it...R-INF-2011-12-04-UNIPMN.pdf
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. 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, in this paper, we propose an approach to BMC which exploits the Buechi automaton construction while searching for a counterexample. The paper provides an encoding in ASP of the temporal action domain and of bounded model checking of DLTL formulas.