Lecture
Jörg Hoffmann
Max-Planck-Institut für Informatik
Programming Logics Group
Room 616, Phone 9325-216
Email: hoffmann@mpi-sb.mpg.de
The lecture covers the known methods to solve the ``reachability problem'' in declaratively specified transition systems. Given a set of transition rules, an initial state, and a (non-temporal) goal formula, the reachability problem asks for the existence of a transition sequence that transforms the initial state into a state that satisfies the goal formula. This kind of problem arises naturally in various fields of computer science, for example in Model-Checking and in AI Planning. Solving the reachability problem is hard even for very restrictive classes of transition rules and goal formulas, and the focus of the lecture lies on the techniques that have most successfully been used to solve the problem efficiently. Throughout the lecture, we use a simple AI Planning formalism, named STRIPS, to introduce and demonstrate the techniques.