We consider the problem of planning in environments where the state is fully observable, actions have non-deterministic effects, and plans must generate infinite state trajectories for achieving a large class of LTL goals. More formally, we focus on the control synthesis problem under the assumption that the LTL formula to be realized can be mapped into a deterministic Büchi automaton. We show that by assuming that action non-determinism is fair, namely that infinite executions of a nondeterministic action in the same state yield each possible successor state an infinite number of times, the (fair) synthesis problem can be reduced to a standard strong cyclic planning task over reachability goals. Since strong cyclic planners are built on top of efficient classical planners, the transformation reduces the non-deterministic, fully observable, temporally extended planning task into the solution of classical planning problems. A number of experiments are reported showing the potential benefits of this approach to synthesis in comparison with state-of-the-art symbolic methods.

Fair LTL synthesis for non-deterministic systems using strong cyclic planners / Patrizi, Fabio; N., Lipovetzky; H., Geffner. - In: IJCAI. - ISSN 1045-0823. - ELETTRONICO. - (2013), pp. 2343-2349. (Intervento presentato al convegno 23rd International Joint Conference on Artificial Intelligence, IJCAI 2013 tenutosi a Beijing; China nel 3 August 2013 through 9 August 2013).

Fair LTL synthesis for non-deterministic systems using strong cyclic planners

PATRIZI, FABIO;
2013

Abstract

We consider the problem of planning in environments where the state is fully observable, actions have non-deterministic effects, and plans must generate infinite state trajectories for achieving a large class of LTL goals. More formally, we focus on the control synthesis problem under the assumption that the LTL formula to be realized can be mapped into a deterministic Büchi automaton. We show that by assuming that action non-determinism is fair, namely that infinite executions of a nondeterministic action in the same state yield each possible successor state an infinite number of times, the (fair) synthesis problem can be reduced to a standard strong cyclic planning task over reachability goals. Since strong cyclic planners are built on top of efficient classical planners, the transformation reduces the non-deterministic, fully observable, temporally extended planning task into the solution of classical planning problems. A number of experiments are reported showing the potential benefits of this approach to synthesis in comparison with state-of-the-art symbolic methods.
2013
23rd International Joint Conference on Artificial Intelligence, IJCAI 2013
Classical planning; Control synthesis; Infinite numbers
04 Pubblicazione in atti di convegno::04b Atto di convegno in volume
Fair LTL synthesis for non-deterministic systems using strong cyclic planners / Patrizi, Fabio; N., Lipovetzky; H., Geffner. - In: IJCAI. - ISSN 1045-0823. - ELETTRONICO. - (2013), pp. 2343-2349. (Intervento presentato al convegno 23rd International Joint Conference on Artificial Intelligence, IJCAI 2013 tenutosi a Beijing; China nel 3 August 2013 through 9 August 2013).
File allegati a 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/11573/516156
 Attenzione

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

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