Portsmouth, USA
June 21-26, 2014
24th International Conference on Automated Planning and Scheduling

WS 4: Workshop on Model Checking and Automated Planning (MOCHAP'14)

There has been a lot of work on the exchanges between the two research areas of Model Checking and Automated Planning, based on the observation that a model-checking problem can be cast as a planning problem, by setting as the goal to achieve a state violating the property to be verified in the model checking problem. Thus, if a plan is found by the planner, it corresponds to the error trace that a model checker would return (this paradigm is called directed model checking). The link can be exploited also in the other way around, using a model checker to search the planning state space, stopping the search when a goal state is found (this paradigm is called planning via model checking). Furthermore, there is a strong connection between hybrid-system falsification and motion planning as state-of-the art motion planners are used as the starting point for searching the continuous state spaces of a hybrid system.


08:45-09:00Welcome Message and Introduction
09:00-09:30 Dan Bryce
Improving counter-example explanations with planning and learning
09:30-10:00 Martin Wehrle
Directed Model Checking for Timed Systems
10:00-10:30 Coffee Break
10:30-11:00 Daniele Magazzeni
Model-Checking based Planning for Hybrid Domains
11:00-11:30 Sicun Gao
Delta-Complete Reachability Analysis for Hybrid Systems: a Planning Perspective
11:30-12:00 Erion Plaku
Motion Planning with Linear Temporal Specifications for Hybrid Systems
12:00-14:00 Lunch Break
14:00-14:30 Maria Fox
Hybrid Plans Validation using VAL
14:30-15:00 Saddek Bensalem, Klaus Havelund, Andrea Orlandini
Verification and Validation Meet Planning and Scheduling
15:00-15:30 Coffee Break
15:30-16:00 Robert Goldman, David Musliner
Employing AI Techniques in Probabilistic Model Checking
16:00-16:30 Stefan Edelkamp
Is Model Checking and Planning a Big Data Application?
16:30-17:00 Discussion and Closing Remarks

Objectives and Topics

The purpose of the workshop is to promote a cross-fertilisation between different but related research areas. This workshop is the ideal venue for researchers in AI planning, motion planning, model checking, robotics, hybrid systems, to discuss what can be shared in terms of techniques, tools, modelling languages and benchmark problems.

The workshop includes - but is not limited to - the following topics:

  • Planning as model checking
  • Directed model checking
  • Falsification
  • Motion planning
  • Hybrid systems
  • Novel benchmark problems
  • Validation and verification of domain models
  • Verification of plan executions
  • Symmetry reduction techniques
  • Partial order reduction techniques
  • Heuristic search
  • Symbolic search
  • Plan robustness
  • Plan validation

List of Talks

  • Verification & Validation Meet Planning & Scheduling
    Saddek Bensalem, Klaus Havelund and Andrea Orlandini.
  • Improving counter-example explanations with planning and learning.
    Dan Bryce.
  • Employing AI Techniques in Probabilistic Model Checking.
    Robert Goldman and David Musliner.
  • Delta-Complete Reachability Analysis for Hybrid Systems: A Planning Perspective.
    Sicun Gao.
  • Model-Checking based Planning in Hybrid Domains.
    Daniele Magazzeni.
  • Motion Planning with Linear Temporal Specifications for Hybrid Systems.
    Erion Plaku.
  • Directed Model Checking for Timed Systems.
    Martin Wehrle.


There are two types of submissions: original papers and recently published papers.

Original papers: we welcome full technical papers (8 pages plus up to one page of references) that report on new original research as well as short/position papers (4 pages plus up to one page of references) discussing novel ideas that are not yet fully developed, novel interesting benchmark problems or short experimental studies.

Previously published papers: in order to foster the exchange of ideas at MOCHAP-14, we encourage authors to submit papers describing new research which has been reported in other venues in the last two years.

Paper Submissions should be made through the MOCHAP-14 EasyChair website. Please format submissions in AAAI style.

Accepted original papers will be published on the workshop website and printed as a hard-copy. An extended abstract for previously published papers will be published in the proceedings.

Papers must be submitted by March 3rd, 2014. Any additional questions can be directed towards the general workshop contact email: mochap2014@easychair.org.

AI Communications Special Issue

We are very happy to announce that an extended version of selected papers will be included in the MOCHAP special issue in the AI Communications journal.

Important Dates

  • Paper submission: March 3rd, 2014
  • Notification of acceptance: March 20th, 2014
  • Camera-ready paper submission: TBD
  • Workshop date: June 23rd, 2014

Organizing Committee

  • Stefan Edelkamp (University of Bremen, Germany)
  • Daniele Magazzeni (King's College London, UK)
  • Erion Plaku (Catholic University of America, USA)

Program Committee

  • Calin Belta, Boston University, USA
  • Hana Chockler, King's College London, UK
  • Alessandro Cimatti, FBK-irst, Italy
  • Thao Dang, VERIMAG, France
  • Giuseppe De Giacomo, (University Of Rome "La Sapienza", Italy)
  • Giuseppe Della Penna, University of L'Aquia, Italy
  • Stefan Edelkamp, University of Bremen, Germany
  • Hector Geffner, ICREA & Universitat Pompeu Fabra, Spain
  • Enrico Giunchiglia, DIST - University of Genova, Italy
  • Patrik Haslum, ANU, Australia
  • Klaus Havelund, Jet Propulsion Laboratory, California Institute of Technology, USA
  • Alan Hu, University of British Columbia, USA
  • Sertac Karaman, Massachusetts Institute of Technology, USA
  • Alberto Lluch Lafuente, IMT Institute for Advanced Studies Lucca, Italy
  • Daniele Magazzeni, King's College London, UK
  • Robert Mattmüller, University of Freiburg, Germany
  • Fabio Mercorio, University of Milano Bicocca, Italy
  • Andrea Orlandini, ISTC-CNR, Italy
  • Erion Plaku, Catholic University of America , USA
  • Andreas Podelski, University of Freiburg, Germany
  • Armando Tacchella, University of Genova, Italy
  • Paolo Traverso, (FBK-ICT, Italy)
  • Enrico Tronci, University Of Rome "La Sapienza", Italy
  • Luca Viganò, King's College London, UK
  • Martin Wehrle, University of Basel, Switzerland
  • Anton Wijs, Eindhoven University of Technology, The Netherlands