In this paper, we report on a preliminary study on the feasibility of applying techniques and tools for finding errors in programs, or prove them entirely correct, to effectively explore the large state space of instances of the automated planning problem (AP). To leverage the recent advancements in the symbolic program analysis, we design a simple reduction from AP to the configuration reachability problem of programs and then use off-the-shelf program verification tools. We evaluate the feasibility of our approach on the Agricola-sat18 benchmark used at IPC’18.

Automated Planning Through Program Verification

Salvatore La Torre
;
2021

Abstract

In this paper, we report on a preliminary study on the feasibility of applying techniques and tools for finding errors in programs, or prove them entirely correct, to effectively explore the large state space of instances of the automated planning problem (AP). To leverage the recent advancements in the symbolic program analysis, we design a simple reduction from AP to the configuration reachability problem of programs and then use off-the-shelf program verification tools. We evaluate the feasibility of our approach on the Agricola-sat18 benchmark used at IPC’18.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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/11386/4770977
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact