Temporal planning is an active research area of Artificial Intelligence because of its many applications ranging from robotics to logistics and beyond. Traditionally, authors focused on the automatic synthesis of plans given a formal representation of the domain and of the problem. However, the effectiveness of such techniques is limited by the complexity of the modeling phase: it is hard to produce a correct model for the planning problem at hand. In this paper, we present a technique to simplify the creation of correct models by leveraging formal-verification tools for automatic validation. We start by using the ANML language, a very expressive language for temporal planning problems that has been recently presented. We chose ANML because of its usability and readability. Then, we present a sound-and-complete, formal encoding of the language into Linear Temporal Logic over predicates with infinite-state variables. Thanks to this reduction, we enable the formal verification of several relevant properties over the planning problem, providing useful feedback to the modeler.

Validating Domains and Plans for Temporal Planning via Encoding into Infinite-State Linear Temporal Logic

Cimatti, Alessandro;Micheli, Andrea;Roveri, Marco
2017

Abstract

Temporal planning is an active research area of Artificial Intelligence because of its many applications ranging from robotics to logistics and beyond. Traditionally, authors focused on the automatic synthesis of plans given a formal representation of the domain and of the problem. However, the effectiveness of such techniques is limited by the complexity of the modeling phase: it is hard to produce a correct model for the planning problem at hand. In this paper, we present a technique to simplify the creation of correct models by leveraging formal-verification tools for automatic validation. We start by using the ANML language, a very expressive language for temporal planning problems that has been recently presented. We chose ANML because of its usability and readability. Then, we present a sound-and-complete, formal encoding of the language into Linear Temporal Logic over predicates with infinite-state variables. Thanks to this reduction, we enable the formal verification of several relevant properties over the planning problem, providing useful feedback to the modeler.
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/11582/310620
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact