AIPS 2002 Workshop on

Planning via Model Checking

Toulouse, France, April 23, 2002

Sponsored by:

Call For Papers | Organising Committee | Preliminary Programme | Proceedings On-Line NEW!!

Call for Papers


Model checking is currently one of the hottest topics in computer science. It consists in comparing a model of a system against a logical requirement to discover inconsistencies. Traditionally, this idea has been used to verify the correctness of hardware circuits and network protocols. More recently, the same idea has been applied to planning with remarkable success, and has led to powerful planning systems such as MBP, MIPS, TALPLANNER, TLPLAN, and UMOP. In planning via model checking, a planning domain is formalized as a specification of possible models for plans; goals are formalized as logical requirements (e.g., in temporal logic) about the desired behavior for plans; the planning problem is solved by searching through plans, checking that there exists one that satisfies the goal. The same approach is used to control the search process by keeping its exploration away from irrelevant plans, using search-control strategies that are formalized as requirements over relevant plans. Symbolic representations inherited from the verification community such as ADDs and BDDs have proven an important tool to further limit the state explosion problem .

In the very last few years, there has been a striking increase in the work extending the basic planning via model checking framework to handling partial observability, concurrency and resources, increasingly complex goals and multi-agent domains. Current work on planning via model checking also largely intersects with other model-theoretic approaches to planning such as decision-theoretic planning, Markov decision processes, or controller synthesis, and relates to some recent frameworks for model-based prediction, diagnosis, repair, and reconfiguration.

Issues to be addressed by the workshop

The aim of this one day workshop is to bring together researchers working on outstanding issues related to planning via model-checking, with a view to discussing them, comparing their approaches, techniques or ideas, and letting these researchers take advantage of different perspectives on these issues. Topics of interest include but are not limited to:

Submission guidelines

Researchers wishing to participate in the workshop may submit either full papers (max 10 pages) which will be refereed by the workshop committee, or short position papers (1-2 pages) describing their interest in the workshop topic. Submissions should be in AAAI conference format (see AAAI instructions and macros ). We encourage the presention of both final results and work in progress. We welcome work submitted to the AIPS conference or elsewhere (KR, ECAI, AAAI, etc ...), although priority may be given to papers not appearing in the AIPS conference.

Important dates

Forward submissions to Froduald Kabanza ( Electronic submissions in postscript or PDF format are highly preferred.

Organising committee

Preliminary Programme

8.55 Welcome
9.00 Invited Talk: Model-Based Planning and Real-Time Execution in the CIRCA Framework
Robert Goldman

Talk inlcudes paper:
Planning Via Model-Checking in Dynamic Temporal Domains: Exploiting Planning Representations
Robert Goldman, David Musliner, Michael Pelican
10.00 Coffee Break
10.30 Probabilistic Plan Verification Through Acceptance Sampling
Hakan Younes, David Musliner
11.00 Solving Planning Problems Using Real-Time Model-Checking (Translating PDDL3 into Timed Automata)
Henning Dierks, Gerd Berhrmann, Kim Larsen
11.30 Partial State Progression: An Extension to the Bacchus-Kabanza Algorithm,with Applications to Prediction and MITL Consistency
Patrick Haslum
12.00 Preemptive Job-Shop Scheduling using Stopwatch Automata
Yasmina Abdeddaim, Oded Maler
12.30 Lunch Break
14.00 Plan Validation for Extended Goals under Partial Observability (preliminary report)
Piergiorgio Bertoli, Alessandro Cimatti, Marco Pistore, Paolo Taverso
14.30 SetA*: An Efficient BDD-Based Heuristic Search Algorithm
Rune Jensen, Randal Bryant, Manuela Veloso
15.00 Symbolic Exploration in Two-Player Games: Preliminary Results
Stefan Edelkamp
15.30 Tea Break
16.00 Invited Talk: Symbolic Model-Checking Techniques for Decision-Theoretic Planning
Eric Hansen

Talk inlcudes paper:
Symbolic LAO* Search for Factored Markov Decision Processes
Zhengzhu Feng, Eric Hansen
17.00 Solving Power Supply Restoration Problems with Planning via Symbolic Model-Checking
Piergiorgio Bertoli, Alessandro Cimatti, John Slaney, Sylvie Thiebaux
17.30 Wrap up
17.45 End

Proceedings On-Line

PDF, 1.6 Mb, formatted to fit A4 paper