Topic

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:

• New results in planning via model checking for deterministic or non-deterministic domains, concerning for instance:
  • handling search-control knowledge in dynamic environments,
  • handling temporally extended goals in the presence of uncertainty and/or partial observation,
  • handling hybrid (i.e. both discrete and continuously changing) variables and environments,
  • handling adversarial environments.
• New model checking techniques for planning, for instance:
  • abstraction techniques,
  • decentralised techniques,
  • hybrid heuristic/symbolic techniques,
  • optimization techniques.
• System architectures that integrate planning via model checking with other techniques, for instance:
  • prediction,
  • diagnosis,
  • plan validation,
  • plan recognition.
• Applications of planning via model checking, for instance, to:
  • Intelligent Tutoring Systems,
  • Robotics,
  • Network Supervision.

Submission guidelines

Organising committee