Research Workshop of the Israel Science Foundation
MOCHAP - Workshop on Model-Checking and Automated Planning
There has been a lot of work on the exchanges between the two research areas of model checking and automated planning. From a high level perspective, model checking and planning problems are related in the sense that plans (found by a planning system) correspond to error traces (found by a model checker). For example, finding violations of properties that can be checked on a per-state basis (e.g., mutex properties) in model checking can be achieved by finding goal states in a correspondent planning problem.
Thus, if a plan is found by a planning system, it corresponds to an error trace that a model checker could return. The link can be exploited also in the other way around, using a model checker to search the state space of a planning problem, and stopping the search when a goal state is found. 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 hybrid systems.
The purpose of the workshop is to continue to promote a cross-fertilisation between research on planning and verification, incrementing the synergy between the two areas. This workshop is an ideal venue for discussing what can be shared in terms of techniques, tools, modelling languages and benchmark problems.
Proceedings
The full MOCHAP proceedings are available as a pdf file.
Schedule
The workshop will be held on June 7, 2015 in Room F.
08:45-09:00 | Welcome and Opening Remarks |
Session I | |
09:00-10:00 |
Keynote 1: Paolo Traverso 20 Years of Planning via Model Checking: From Theory to Practice |
10:00-10:30 | Coffee Break |
Session II | |
10:30-11:00 |
Dominik Winterer, Robert Mattmüller, Martin Wehrle Stubborn Sets for Fully Observable Nondeterministic Planning |
11:00-11:30 |
Jonas Thiem, Robert Mattmüller, Manuela Ortlieb Counterexample-Guided Abstraction Refinement for POND Planning |
11:30-12:00 |
Jorge Torres and Jorge Baier Compiling Away LTL Planning Goals in Polynomial Time |
12:00-12:30 |
Eleni Triantafillou, Jorge Baier, Sheila McIlraith A Unifying Framework for Planning with LTL and Regular Expressions |
12:00-14:00 | Lunch Break |
Session III | |
14:00-15:00 |
Keynote 2: Doron Peled Commutativity based search |
15:00-15:30 |
Dragan Bosnacki On Combining Symmetry with Partial Order Reduction |
15:30-16:00 | Coffee Break |
Session IV | |
16:00-16:30 |
Patrik Haslum Diagnosis, Planning, and Related Questions |
16:30-17:00 |
Giuseppe Della Penna, Benedetto Intrigila, Daniele Magazzeni, Fabio Mercorio UPMurphi Released: PDDL+ Planning for Hybrid Systems |
17:00-17:30 |
Sergiy Bogomolov Hybrid Systems: Guided Search, Abstractions, and Beyond |
17:30-18:00 | Panel Session |
Call for Papers
Topics of Interest
Topics of interest include - but are not limited to - the following topics:
- Planning as model checking
- Directed model checking
- Falsification
- Motion planning
- Hybrid systems
- Protocol Verification
- 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
Important Dates
- Submission deadline:
February 20, 2015EXTENDED: March 6, 2015 - Notification: March 20, 2015
- Final date for camera-ready copy: TBD
- Workshop date: June 7th , 2015
Submission Procedure
There are two types of submissions: original work and recently published papers.
- Original work: contributions may range from extended abstracts of one or two pages to full papers of eight pages. Note that the workshop proceedings are non-archival, and we particularly invite submissions of recent work and work in progress that is not yet fully elaborated.
- Previously published papers: in order to foster the exchange of ideas at MOCHAP-15, 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-15 EasyChair website https://www.easychair.org/conferences/?conf=mochap2015. Please format submissions in AAAI style. Refer to the author instructions on the AAAI web site for detailed formatting instructions and LaTeX style files (http://www.aaai.org/Publications/Author/author.php).
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 February 20th, 2015. Any additional questions can be directed towards the general workshop contact email: mochap2015@easychair.org
Organizers
- Sergiy Bogomolov (University of Freiburg, Germany)
- Daniele Magazzeni (King's College London)
- Martin Wehrle (University of Basel, Switzerland)
Programme committee
- Sergiy Bogomolov (University of Freiburg, Germany)
- Dragan Bosnacki (Eindhoven University of Technology, The Netherlands)
- Giuseppe Della Penna (University of L'Aquila, Italy)
- Stefan Edelkamp (University of Bremen, Germany)
- Georgios Fainekos (Arizona State University, USA)
- Goran Frehse (Verimag, France)
- Enrico Giunchiglia (University of Genova, Italy)
- Klaus Havelund (Jet Propulsion Laboratory, USA)
- Alan J. Hu (University of British Columbia, Canada)
- Alberto Lluch Lafuente (Technical University of Denmark, Denmark)
- Daniele Magazzeni (King's College London, UK)
- Fabio Mercorio (University of Milano Bicocca, Italy)
- Andrea Orlandini (CNR-ISTC, Italy)
- Doron Peled (Bar Ilan University, Israel)
- Erion Plaku (Catholic University of America, USA)
- Andreas Podelski (University of Freiburg, Germany)
- Sylvie Thiebaux (Australian National University, Australia)
- Enrico Tronci (University of Rome "La Sapienza", Italy)
- Martin Wehrle (University of Basel, Switzerland)