Planning as Model Checking
- AIPS'02 Tutorial -
Marco Pistore and
Via Sommarive 18, 39055 Povo (TN) - Italy
||This tutorial is sponsored by PLANET, the European
Network of Excellence in AI Planning.
This tutorial will be held at AIPS'02 on April, 24.
Please look at this
page for further information on the AIPS'02 tutorials.
In the last few years, Model Checking has been shown to be a very
effective approach to Planning.
In Model Checking [6,13], a formal model of a system is compared
against a logical specification of its requirements to discover
Very efficient techniques have been developed, during the course of
more than one decade, to deal with increasingly complex hardware and
Symbolic Model Checking [6,24] is a particular form of Model Checking
that allows to analyze extremely large finite-state systems by means
of symbolic representation techniques (e.g., Binary Decision Diagrams
and propositional satisfiability).
(Symbolic) Model Checking is the core technique for several industrial
verification tools and is the main research topic in the area of
hardware and software verification.
More recently, the same idea has been applied to Planning with
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  and TalPlan )
or to allow for temporally extended goals (e.g., SimPlan ).
Other systems use Model Checking with timed automata to verify
plans that should meet timing constraints (CIRCA ).
A wide range of systems exploit Symbolic Model Checking techniques for
obtaining an efficient search in large deterministic (MIPS ,
Proplan , BDDPlan ) or non-deterministic domains
(MBP , UMOP ).
Symbolic representation techniques have been also applied to
MDP-based planning (SPUDD ).
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. ).
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 .
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
planner  will be used to show actual solutions of planning
problems. During a practical session, the participants will confront
with increasingly complex assignments using
Outline of covered topics.
The tutorial will cover the following 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
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
As a close-up, we will review a list of advanced topics, including
adversarial multi-agent planning [20,21], planning with
knowledge goals , 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
The tutorial targets different classes of 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.
- You can download a Gzipped PostScript version of the slides of the tutorial
- A more compact PDF version is available here.
- An here.
- 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.
- F. Bacchus and F. Kabanza. Using temporal
logic to express search control knowledge for planning.
Artificial Intelligence 116(1-2):123-191, 2000.
- 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,
- 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.
- 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.
- 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,
- 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.
- 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.
- 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.
- A. Cimatti and M. Roveri. Conformant Planning via
Symbolic Model Checking. Journal of Artificial
Intelligence Research (JAIR), 13:305-338, 2000.
- 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.
- 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
- 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.
- S. Edelkamp and M. Helmert. On the implementation of
MIPS. In AIPS Workshop on Model-Theoretic Approaches to
- M. P. Fourman. Propositional planning. In AIPS Workshop on Model-Theoretic Approaches to Planning, 2000.
- F. Giunchiglia and P. Traverso. Planning as Model
Checking. In Proc. 5th European Conference on
Planning (ECP-99), LNAI. Springer-Verlag, 1999.
- 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,
- 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.
- 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.
- 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.
- 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.
- F. Kabanza, M. Barbeau, and R. St-Denis.
Planning control rules for reactive agents.
Artificial Intelligence, 95(1):67-113, 1997.
- J. Kvarnströ, P. Doherty, and P. Haslum. Extending
TALplanner with Concurrency and Resources. In Proc. of
ECAI 2000, pages 501-505.
- K.L. McMillan. Symbolic Model Checking.
Kluwer Academic Publ., 1993.
- 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.
- 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.
Last Edited: 2002-03-12 (Marco Pistore)