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), pp. 3547-3554. (Intervento presentato al convegno Thirty-First AAAI Conference on Artificial Intelligence tenutosi a San Francisco, California, USA. nel February 4-9, 2017).

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

Cimatti Alessandro;Micheli Andrea;Roveri Marco
2017-01-01

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.
2017
Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence
USA
AAAI Press
Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco
Validating Domains and Plans for Temporal Planning via Encoding into Infinite-State Linear Temporal Logic / Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco. - (2017), pp. 3547-3554. (Intervento presentato al convegno Thirty-First AAAI Conference on Artificial Intelligence tenutosi a San Francisco, California, USA. nel February 4-9, 2017).
File in questo prodotto:
File Dimensione Formato  
AAAI-17-PV.pdf

Solo gestori archivio

Tipologia: Versione editoriale (Publisher’s layout)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 711.54 kB
Formato Adobe PDF
711.54 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: https://hdl.handle.net/11572/258714
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 7
  • ???jsp.display-item.citation.isi??? 4
social impact