23.11.14 - 28.11.14, Seminar 14482

Automated Planning and Model Checking

Diese Seminarbeschreibung wurde vor dem Seminar auf unseren Webseiten veröffentlicht und bei der Einladung zum Seminar verwendet.


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.