Planning as Model Checking
- AIPS'02 Hands-On Tutorial -

Piergiorgio Bertoli, Marco Pistore and Marco Roveri

ITC-IRST
Via Sommarive 18, 39055 Povo (TN) - Italy
{bertoli,pistore,roveri}@irst.itc.it

This tutorial is sponsored by PLANET, the European Network of Excellence in AI Planning.

Motivations.

More recently, the same idea has been applied to Planning with remarkable success. The ``Planning as Model Checking'' approach [8,12,16] formulates a planning problem in a logical context, while the symbolic representation techniques allow for handling complex domains. In Planning as Model Checking, a planning domain is formalized as a specification of possible models for plans. Goals are formalized as logical requirements about the desired behavior for plans. The planning problem (i.e., finding a plan that achieves the goal) is solved by searching through the state space, checking that there exists a plan that satisfies the goal.

Several planning systems are based on different kinds of Model Checking techniques for different purposes. Some of them use explicit-state Model Checking to embed control strategies in the search (TLPlan [2] and TalPlan [23]) or to allow for temporally extended goals (e.g., SimPlan [22]). Other systems use Model Checking with timed automata to verify plans that should meet timing constraints (CIRCA [17]). A wide range of systems exploit Symbolic Model Checking techniques for obtaining an efficient search in large deterministic (MIPS [14], Proplan [15], BDDPlan [19]) or non-deterministic domains (MBP [3], UMOP [20]). Symbolic representation techniques have been also applied to MDP-based planning (SPUDD [18]).

Papers on Planning as Model Checking regularly appear in the most important planning conferences and successful workshops are organized on this topic (see e.g. [7]). Recent contributions also show the practical impact of Planning as Model Checking in real planning domain, e.g., in the design of controllers for safety-critical and on-board autonomous systems [1].

This tutorial is motivated by the strong interest in the Planning as Model Checking paradigm. The tutorial is intended to provide the participants with an overview of Planning as Model Checking and with a detailed description of Planning as Symbolic Model Checking. Moreover, the tutorial is designed to be ``hands-on''. The MBP planner [3] will be used to show actual solutions of planning problems. During a practical session, the participants will confront with increasingly complex assignments using MBP.

Outline of covered topics.

• Background on Model Checking
• Introduction on Planning as Model Checking
• Theoretical aspects and algorithmic techniques for Planning as Symbolic Model Checking:
  • Planning for Reachability.
  • Planning with Extended Goals.
  • Planning under Partial Observability.
• Practical session using MBP
• Advanced topics on Planning as Model Checking

In the first introductory phases, the basic theory of Model Checking is presented, with a focus on Symbolic Model Checking. Moreover, the different aspects and approaches to Planning as Model Checking are reviewed and put into the frame of the existing approaches to Planning (e.g., classical search, MDPs, ...).

Then, the scope will restrict to Planning as Symbolic Model Checking. A theoretical foundation will be provided, and basic techniques and algorithms used in Planning as Model Checking will be presented. This includes discussing symbolic techniques for representing and handling sets of states (BDDs), and describing fixed-point algorithms for different planning problems (e.g., weak, strong, strong-cyclic planning algorithms [9,12]). Some more advanced planning algorithms will also be discussed, where limited sensing and complex temporal goals are taken into account [5,10,26,25].

In the third phase, we introduce the MBP planner, describing its features and input languages by means of explanatory examples that the participants will be able to test. The core of this phase revolves around a set of incrementally difficult planning problems that the participants will have to model and solve using MBP.

As a close-up, we will review a list of advanced topics, including adversarial multi-agent planning [20,21], planning with knowledge goals [11], and the combination of model-checking techniques with heuristic search [5,4,11]. For each of these topics, we will discuss in which way they can be tackled in the Planning as Model Checking framework.

Target audience.

• Master and PhD students interested in the Planning area are the main target for this tutorial. For them, Planning as Model Checking can be an appealing research field to focus their studies upon, and/or to compare with the current object of their studies in the area. The ``hands-on'' approach is particularly suited to a practical introduction of the issues in the field.
• Researchers in the planning community that did not yet work using the Planning as Model Checking paradigm. For them, the tutorial is very useful as an ``hands-on'' introduction to the field, and it can be the source of inspiration for combining their approaches with the Model Checking techniques.
• Researchers in the planning community that already work using the Planning as Model Checking paradigm. For them, the tutorial is appealing as it provides a survey of the state of the art in the field, of the recent advancements, and the possibility to compare their approaches with MBP.
• Researchers in the formal methods area. For them, the tutorial builds a bridge towards the planning field, and it can be the source of cross-fertilization between the two communities.

Material.

• You can download a Gzipped PostScript version of the slides of the tutorial here.
• A more compact PDF version is available here.
• An MBP system description can be found here.

Bibliography.

1

L. Aiello, A. Cesta, E. Giunchiglia, M. Pistore, and P. Traverso. Planning and verification techniques for the high-level programming and monitoring of autonomous devices. In Proc. ESA Workshop on ``On-Board Autonomy'', 2001.

2

F. Bacchus and F. Kabanza. Using temporal logic to express search control knowledge for planning. Artificial Intelligence 116(1-2):123-191, 2000.

3

P. Bertoli, A. Cimatti, M. Pistore, M. Roveri, and P. Traverso. MBP: a Model Based Planner. In Proc. IJCAI’01 Workshop on Planning under Uncertainty and Incomplete Information, 2001.

4

P. Bertoli, A. Cimatti, and M. Roveri. Heuristic Search + Symbolic Model Checking = Efficient Conformant Planning. In Proc. 7th International Joint Conference on Artificial Intelligence (IJCAI-01). AAAI Press, August 2001.

5

P. Bertoli, A. Cimatti, M. Roveri, and P. Traverso. Planning in Nondeterministic Domains under Partial Observability via Symbolic Model Checking. In Proc. 7th International Joint Conference on Artificial Intelligence (IJCAI-01). AAAI Press, August 2001.

6

J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic Model Checking: 10^20 States and Beyond. Information and Computation, 98(2):142-170, June 1992.

7

A. Cimatti, H. Geffner, E. Giunchiglia and J. Rintanen. Proceedings of Workshop on Planning under Uncertainty and Incomplete Information, 7th International Joint Conference on Artificial Intelligence (IJCAI-01), Seattle, August 2001.

8

A. Cimatti, E. Giunchiglia, F. Giunchiglia, and P. Traverso. Planning via Model Checking: A Decision Procedure for AR. In Proc. 4th European Conference on Planning (ECP-97), LNAI 1348. Springer-Verlag, 1997.

9

A. Cimatti, M. Pistore, M. Roveri, and P. Traverso. Weak, Strong, and Strong Cyclic Planning via Symbolic Model Checking. Technical Report 0104-1, ITC-IRST, April 2001.

10

A. Cimatti and M. Roveri. Conformant Planning via Symbolic Model Checking. Journal of Artificial Intelligence Research (JAIR), 13:305-338, 2000.

11

A. Cimatti, M. Roveri, and P. Bertoli. Searching Powerset Automata by Combining Explicit-State and Symbolic Model Checking. In Proc. 7th International Conference on Tools and Algorithms for the Construction of Systems, pages 313-327. Springer, April 2001.

12

A. Cimatti, M. Roveri, and P. Traverso. Automatic OBDD-based Generation of Universal Plans in Non-Deterministic Domains. In Proc. 5th National Conference on Artificial Intelligence (AAAI-98). AAAI-Press, 1998

13

E. M. Clarke and J. M. Wing. Formal methods: State of the art and future directions. ACM Computing Surveys, 28(4):626-643, December 1996.

14

S. Edelkamp and M. Helmert. On the implementation of MIPS. In AIPS Workshop on Model-Theoretic Approaches to Planning, 2000.

15

M. P. Fourman. Propositional planning. In AIPS Workshop on Model-Theoretic Approaches to Planning, 2000.

16

F. Giunchiglia and P. Traverso. Planning as Model Checking. In Proc. 5th European Conference on Planning (ECP-99), LNAI. Springer-Verlag, 1999.

17

R. P. Goldman, D. J. Musliner, and M. J. Pelican. Using Model Checking to Plan Hard Real-Time Controllers. In Proceeding of the AIPS2k Workshop on Model-Theoretic Approaches to Planning, Breckeridge, Colorado, April 2000.

18

J. Hoey, R. St-Aubin, A. Hu, and C. Boutilier. SPUDD: Stochastic Planning using Decision Diagrams. In Fifteenth Conference on Uncertainty in Artificial Intelligence (UAI-99), 1999.

19

S. Hölldobler and H.-P. Störr. Solving the entailment problem in the fluent calculus using binary decision diagrams. In Workshop on Model-Theoretic Approaches to Planning at AIPS2000. Beckenridge, April 2000.

20

R. Jensen and M. Veloso. OBDD-based Universal Planning for Synchronized Agents in Non-Deterministic Domains. Journal of Artificial Intelligence Research, 13:189-226, 2000.

21

R. Jensen, M. Veloso, and M. Browling. OBDD-Based Optimistic and Strong Cyclic Adversarial Plannung. In Proc. 6th European Conference on Planning (ECP-01), September 2001.

22

F. Kabanza, M. Barbeau, and R. St-Denis. Planning control rules for reactive agents. Artificial Intelligence, 95(1):67-113, 1997.

23

J. Kvarnströ, P. Doherty, and P. Haslum. Extending TALplanner with Concurrency and Resources. In Proc. of ECAI 2000, pages 501-505.

24

K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publ., 1993.

25

M. Pistore, R. Bettin, and P. Traverso. Symbolic Techniques for Planning with Extended Goals in Non-deterministic Domains. In Proc. 6th European Conference on Planning (ECP-01), September 2001.

26

M. Pistore and P. Traverso. Planning as model checking for extended goals in non-deterministic domains. In Proc. 7th International Joint Conference on Artificial Intelligence (IJCAI-01). AAAI Press, August 2001.