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.

Schedule

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.

Submission

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