Weak, strong, and strong cyclic planning via symbolic model checking

By A. Cimatti, Marco Pistore, Marco Roveri, Paolo Traverso. Artificial Intelligence, 2003

439 citations recorded by the source corpus.

Planning in nondeterministic domains yields both conceptual and practical difficulties. From the conceptual point of view, different notions of planning problems can be devised: for instance, a plan might either guarantee goal achievement, or just have some chances of success. From the practical point of view, the problem is to devise algorithms that can effectively deal with large state spaces. In this paper, we tackle planning in nondeterministic domains by addressing conceptual and practical problems. We formally characterize different planning problems, where solutions have a chance of success ("weak planning"), are guaranteed to achieve the goal ("strong planning"), or achieve; the goal with iterative trial-and-error strategies ("strong cyclic planning"). In strong cyclic planning, all the executions associated with the solution plan always have a possibility of terminating and, when they do, they are guaranteed to achieve the goal. We present planning algorithms for these problem classes, and prove that they are correct and complete. We implement the algorithms in the MBP planner by using symbolic model checking techniques. We show that our approach is practical with an extensive experimental evaluation: MBP compares positively with state-of-the-art planners, both in terms of expressiveness and in terms of performance.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Software

View Paper: https://www.semanticscholar.org/paper/245b7d74e5ed741cea804f6237a9f0ec4651046d

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

In Software

Citations in the corpus

A review of generalized planning (2019, background): “When actions have non-deterministic eﬀects plan validation becomes more complex since it requires proving that all the possible plan executions reach the goals [14].”
Automated Composition of Semantic Web Services into Executable Processes (2004, positive): “We can thus exploit the “Planning as Model Checking” approach based on symbolic model checking techniques [14, 9, 6, 11, 4], which has been shown to provide a practical solution to the problem of planning with nondeterministic actions, partial observability, and complex goals, and which has been sho”
Automated composition of Web services via planning in asynchronous domains (2005, background): “, strong and strong cyclic reachability goals (Cimatti et al. 2003), LTL and CTL goals (Pistore & Traverso 2001), and the most relevant for our purposes, EAGLE goals (Dal Lago, Pistore, & Traverso 2002)).”
Automated Planning and Acting (2016, background): “A full formal account and an extensive experimental evaluation of the symbolic model checking approach has been presented in [121].”