Achieving completeness in bounded model checking of action theories in ASP

Risultato della ricerca: Capitolo in libro/report/atti di convegnoContributo a conferenzapeer review

Abstract

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.

Lingua originaleInglese
Titolo della pubblicazione ospite13th International Conference on the Principles of Knowledge Representation and Reasoning, KR 2012
EditoreInstitute of Electrical and Electronics Engineers Inc.
Pagine618-622
Numero di pagine5
ISBN (stampa)9781577355601
Stato di pubblicazionePubblicato - 2012
Evento13th International Conference on the Principles of Knowledge Representation and Reasoning, KR 2012 - Rome, Italy
Durata: 10 giu 201214 giu 2012

Serie di pubblicazioni

NomeProceedings of the International Conference on Knowledge Representation and Reasoning
ISSN (stampa)2334-1025
ISSN (elettronico)2334-1033

???event.eventtypes.event.conference???

???event.eventtypes.event.conference???13th International Conference on the Principles of Knowledge Representation and Reasoning, KR 2012
Paese/TerritorioItaly
CittàRome
Periodo10/06/1214/06/12

Fingerprint

Entra nei temi di ricerca di 'Achieving completeness in bounded model checking of action theories in ASP'. Insieme formano una fingerprint unica.

Cita questo