Dagstuhl Seminar 14482
Automated Planning and Model Checking
( Nov 23 – Nov 28, 2014 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/14482
Organizers
- Alessandro Cimatti (Bruno Kessler Foundation - Trento, IT)
- Stefan Edelkamp (Universität Bremen, DE)
- Maria Fox (King's College London, GB)
- Erion Plaku (CUA - Washington, US)
Coordinator
- Daniele Magazzeni (King's College London, GB)
Contact
- Susanne Bach-Bernhard (for administrative matters)
Shared Documents
- Dagstuhl Materials Page (Use personal credentials as created in DOOR to log in)
Schedule
In the area of formal methods, model checking deals with the problem of fully-automated property validation and correctness verification. Given a formal model of a system and a property specification, the task is to explore the state space and verify whether or not the property is satisfied by the model. In artificial intelligence, automated planning deals with the automatic generation of plans for achieving a goal. Given the description of the initial state, the goal state, and the set of possible actions, a planner uses heuristic search to look for a sequence of actions that transforms the initial state into the goal state.
There has been a lot of work on the exchanges between the two areas (automated planning and model checking), based on the observation that a model-checking problem can be cast as a planning problem, where the goal state is 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 error trace that a model checker would return (this paradigm is called directed model checking). The link can also be exploited 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).
The general aim of this Dagstuhl Seminar is to increase the synergy between the two research communities. This involves sharing views, thoughts and contributions across the following streams:
-
* Techniques and Tools: The seminar will consider the most recent advances
in automated planning and model checking and explore the possibility of using recent planning tools (heuristic search, sampling-based motion-planning algorithms,
symbolic search algorithms, ...) for system falsification (particularly in challenging domains such as hybrid systems) and for boosting the use of model checking systems for finding plans.
-
* Modelling Languages: One of the goals of the seminar is to consider the family of PDDL languages and the formalisms for describing verification problems and discuss how to make the communication between the two areas easier, exploring the possibility of common languages or translation between existing formalisms.
-
* Benchmarks Development: The seminar will bring together people from academia as
well as from industry, in order to highlight current challenges in modelling and
solving real-world planning and verification problems. Therefore, another goal of the
seminar will be to establish the basis for designing a set of benchmark problems, to be shared between the planning and model checking communities, that will help push forward the state of the art and the links with the industry and will allow an easier comparison of the performance of the different approaches.
In the area of formal methods, model checking deals with the problem of fully-automated property validation and correctness verification. Given a formal model of a system and a property specification, the task is to explore the state space and verify whether or not the property is satisfied by the model. In artificial intelligence, automated planning deals with the automatic generation of plans for achieving a goal. Given the description of the initial state, the goal state, and the set of possible actions, a planner uses heuristic search to look for a sequence of actions that transforms the initial state into the goal state.
There has been a lot of work on the exchanges between the two areas (automated planning and model checking), based on the observation that a model-checking problem can be cast as a planning problem, where the goal state is 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 error trace that a model checker would return (this paradigm is called directed model checking). The link can also be exploited 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).
The general aim of this Dagstuhl Seminar was to increase the synergy between the two research communities. This involved sharing views, thoughts and contributions across the following streams:
- Techniques and Tools: During the seminar we considered the most recent advances in automated planning and model checking and explored the possibility of using recent planning tools (heuristic search, sampling-based motion-planning algorithms, symbolic search algorithms, ...) for system falsification (particularly in challenging domains such as hybrid systems) and for boosting the use of model checking systems for finding plans.
- Modelling Languages: One of the goals of the seminar was to consider the family of PDDL languages and the formalisms for describing verification problems and discuss how to make the communication between the two areas easier, exploring the possibility of common languages or translation between existing formalisms.
There were a number of talks on "X" Modulo Theories, where "X" ranged from SAT and Search to Planning. These talks explored the relationship between generic solution methods and different proof systems, leading to discussions about the relative benefits of viewing problems from the perspectives of the different generic methods. This fostered an improved understanding of each other's perspectives and modelling approaches.
Discussions also focused on relationships between hybrid planning and hybrid model-checking. There were tutorials on the modelling languages used in the two paradigms, and their semantics, and the discrepancies between these led to lively discussion. In hybrid planning using PDDL, a key semantic issue is the use of epsilon time to separate inter-dependent actions, in order to prevent the planner from relying on synchronised activity. For example, if an action, A, achieves the precondition of another action, B, the validity of the plan depends on A being ordered strictly before B, by at least epsilon time. This is because the state following the co-occurrence of these two actions is indeterminate. The model-checking community does not require this epsilon. In hybrid model-checking a partial order on events is maintained, and there was an extended discussion about why planning forces an ordering using epsilon separation when this is not necessary in model-checking. From this discussion the following distinction emerged: model-checking simply requires there to be a single ordering of events that is consistent with the constraints, as this provides the required counter-example to the correctness of the model. In planning, by contrast, all orderings of events must be consistent with the constraints, requiring exponential work to check the validity of a partially ordered plan. Once this point was understood there was a greater common understanding between the planning and model-checking proponents, and greater appreciation of the crossover between modelling languages and methods.
Other topics covered by the contributed talks include:
- directed model checking and falsification
- plan validation
- heap and other data structures
- GPU-based state space exploration
- hybrid systems
- heuristic search
- planning and verification on real-world scenarios
The program featured the following components:
- On Monday we started with 7 tutorial-type introductory talks about plans validation, planning in hybrid systems through model checking, guided search for hybrid systems, falsification of hybrid systems through motion planning, planning via symbolic model checking, directed model checking of timed systems, heap implementations. The purpose of these tutorials was to familiarise members of the different communities with the basics of the other fields and with the existing synergies between the fields.
- From Tuesday, each day featured one or two long talks plus a number of short talks, with enough time for discussion after each talk.
- On Tuesday and Thursday afternoon we had two open discussion sessions.
- Wednesday afternoon featured a hike.
A feature of this seminar was the very high level of engagement and interaction between the participants, leading to a lively and productive week. The decision not to formalise discussions into panels or break-out sessions proved to be a good one, allowing more flexible response to topics as they arose. Similarly, the decision to leave some of the talk slots open allowed spontaneous pursuit of ideas that came out of discussions. The mixture of long and short talks also encouraged this. The workshop ended on a high note, with many new ideas for collaboration having been identified.
Creative Commons BY 3.0 Unported license
Alessandro Cimatti and Stefan Edelkamp and Maria Fox and Daniele Magazzeni and Erion Plaku
- Sergiy Bogomolov (Universität Freiburg, DE) [dblp]
- Dragan Bosnacki (TU Eindhoven, NL) [dblp]
- Ronen I. Brafman (Ben Gurion University - Beer Sheva, IL) [dblp]
- Alessandro Cimatti (Bruno Kessler Foundation - Trento, IT) [dblp]
- Stefan Edelkamp (Universität Bremen, DE) [dblp]
- Georgios Fainekos (Arizona State University - Tempe, US) [dblp]
- Maria Fox (King's College London, GB) [dblp]
- Malte Helmert (Universität Basel, CH) [dblp]
- David Hsu (National University of Singapore, SG) [dblp]
- Alan Hu (University of British Columbia - Vancouver, CA) [dblp]
- Hanna Kurniawati (The University of Queensland - Brisbane, AU) [dblp]
- Derek Long (King's College London, GB) [dblp]
- Daniele Magazzeni (King's College London, GB) [dblp]
- Sheila McIlraith (University of Toronto, CA) [dblp]
- Bernhard Nebel (Universität Freiburg, DE) [dblp]
- Doron A. Peled (Bar-Ilan University - Ramat Gan, IL) [dblp]
- Erion Plaku (CUA - Washington, US) [dblp]
- Andreas Podelski (Universität Freiburg, DE) [dblp]
- Franco Raimondi (Middlesex University, GB) [dblp]
- Sylvie Thiébaux (Australian National University, AU) [dblp]
- Martin Wehrle (Universität Basel, CH) [dblp]
- Anton Wijs (RWTH Aachen, DE) [dblp]
- Brian C. Williams (MIT - Cambridge, US) [dblp]
- Paolo Zuliani (University of Newcastle, GB) [dblp]
Classification
- artificial intelligence / robotics
- verification / logic
Keywords
- Model Checking
- Automated Planning
- State Explosion Problem
- Heuristic Search
- Symbolic Search
- Motion Planning
