Star-Topology Decoupled State Space Search
Final Report Abstract
Planning is one of the fundamental sub-areas of AI. Its technology allows to solve any problem that can be modeled in terms of finding paths in large transition systems, and can drastically simplify problem solving: instead of 1000s of lines of program code, one writes/maintains 10s of lines of model code. A major obstacle in making planning systems capable of handling large-scale problem instances is the state explosion problem. Given a compact model description, the resulting state space has a size that is exponential in the size of the model. Many techniques have been developed in the past decades that attempt to tackle the state explosion problem. Star-topology decoupled state-space search is a novel addition to this set of techniques that has been developed in this project. Decoupled search decomposes a given factored state representation, i.e., state variables in planning or synchronized automata in model checking, to exploit conditional independence of parts of the model. Thereby, decoupled search avoids the blow-up that results from enumerating all possible combinations of assignments to these independent parts. This is done by searching only over sequences of transitions that synchronize components, i.e., the center actions in planning, and enumerating, for each of a set of leaf components, the set of component states reachable along the synchronizing transition sequence. The project developed decoupled search in the context of classical AI planning and model checking. Following two initial works published before the project by the research group of the principal investigator, the concept of decoupled search was thoroughly investigated. An essential part is the comparison to existing work previously introduced to tackle the state explosion problem. As a main results of the project, it turned out that decoupled search is orthogonal to all known state space reduction techniques, most prominently partialorder reduction methods, symmetry breaking, symbolic state representation, and Petri-net unfolding. Decoupled search was established as a state-of-the-art approach to solve AI planning problems using heuristic search, the currently most popular way of solving planning problems. The properties of the decoupled state space have been investigated in detail, leading to a well-performing planning system. As part of the first project phase, building on the orthogonality of decoupled search with existing approaches, adaptations of several of these methods to the decoupled state space have been developed, leading to search algorithms that inherit the advantages of both methods. In model checking, decoupled search has been very successfully applied to the verification of safety and liveness properties, resulting in a verifier that outperforms the SPIN model checker on instances with several interacting model components. The project was a resounding success in terms of scientific output, with 2 papers in major journals and 14 papers in major international conferences published on the project topics by the principal investigator’s research group.
