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.
