Recent research has addressed the problem of planning in non-deterministic domains. Classical planning has also been extended to the case of goals that can express temporal properties. However, the combination of these two aspects is not trivial. In non-deterministic domains, goals should take into account the fact that a plan may result in many possible different executions and that some requirements can be enforced on all the possible executions, while others may be enforced only on some executions. In this paper we address this problem. We define a planning algorithm that generates automatically plans for extended goals in non-deterministic domains, and prove that the algorithm is correct and complete. We provide an implementation of the planning algorithm by using symbolic model checking techniques, and show that it is effective in practice with some experimental results
Planning as Model Checking for Extended Goals in Non-deterministic Domains
Pistore, Marco;Traverso, Paolo
2001-01-01
Abstract
Recent research has addressed the problem of planning in non-deterministic domains. Classical planning has also been extended to the case of goals that can express temporal properties. However, the combination of these two aspects is not trivial. In non-deterministic domains, goals should take into account the fact that a plan may result in many possible different executions and that some requirements can be enforced on all the possible executions, while others may be enforced only on some executions. In this paper we address this problem. We define a planning algorithm that generates automatically plans for extended goals in non-deterministic domains, and prove that the algorithm is correct and complete. We provide an implementation of the planning algorithm by using symbolic model checking techniques, and show that it is effective in practice with some experimental resultsI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
