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

Gennaro Parlato
2021-01-01

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: https://hdl.handle.net/11695/100660
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact