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. The article deals with verification of action theories defined in a temporal extension of answer set programming which combines ASP with a dynamic linear time temporal logic (DLTL). The article proposes an approach to bounded model checking that exploits the Büchi automaton construction while searching for a counterexample, with the aim of achieving completeness. The article provides an encoding in ASP of the temporal action domains and of Bounded Model Checking of DLTL formulas. The article also deals with reasoning about epistemic knowledge and incomplete states.

Achieving completeness in the verification of action theories by Bounded Model Checking in ASP

GIORDANO, Laura;MARTELLI, Alberto;THESEIDER DUPRE', Daniele
2015

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. The article deals with verification of action theories defined in a temporal extension of answer set programming which combines ASP with a dynamic linear time temporal logic (DLTL). The article proposes an approach to bounded model checking that exploits the Büchi automaton construction while searching for a counterexample, with the aim of achieving completeness. The article provides an encoding in ASP of the temporal action domains and of Bounded Model Checking of DLTL formulas. The article also deals with reasoning about epistemic knowledge and incomplete states.
25
6
1307
1330
http://logcom.oxfordjournals.org/content/25/6/1307
Answer set programming, model checking, linear time temporal logic.
L. GIORDANO; A. MARTELLI; D. THESEIDER DUPRE'
File in questo prodotto:
File Dimensione Formato  
JLC2015.pdf

Accesso aperto

Descrizione: articolo principale
Tipo di file: PREPRINT (PRIMA BOZZA)
Dimensione 538.28 kB
Formato Adobe PDF
538.28 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/2318/145906
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? 0
social impact