Star-Topology Decoupled State Space Search

• Applicant: Professor Dr. Jörg Hoffmann
• Subject Area: Image and Language Processing, Computer Graphics and Visualisation, Human Computer Interaction, Ubiquitous and Wearable Computing
• Term: from 2016 to 2022
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 289186625

State space search is a basic method to address analysis or decision-making problems formulated using large transition systems. States capture snapshots of some system or model at (discrete) time steps, transitions capture how states may be changed in the next step, and the task is to prove the presence or absence of transition paths with particular properties. This kind of problem occurs across several sub-areas of CS, including AI planning where an agent needs to select actions leading to its goal, and model checking analyzing the properties of some program or system model. A challenge common to all such applications is the state space explosion: The size of the transition system is exponential in the size of its description.Star-topology decoupling, devised by the author for AI planning in the work leading up to this project, is a new approach addressing that challenge. It views state space models as being composed of a single center component and several leaf components, where the center interacts with each leaf, but the leaves interact only via the center. Natural examples include client-server architectures and cooperative agents with shared resources. The decoupled search exploits a particular kind of "conditional independence" that arises in this context: Given a fixed path of transitions by the center, the possible center-compliant paths for each leaf are mutually independent of each other. We can thus search over center paths only, and maintain the center-compliant paths for each leaf separately. This can exponentially reduce state space size, and exponentially more so than known techniques like partial-order reduction and Petri net unfolding. Empirical results on benchmarks exhibit substantial, sometimes dramatic, performance improvements on examples with a pronounced star topology. Star-topology decoupling thus has the potential to become one of the basic methods for effective state space search, across CS sub-areas. The objective of this project is to realize that potential.During the first funding phase, we matured the algorithmic components through symbolic representations, decoupled-state dominance, partial-order reduction and symmetry reduction; we extended the structural scope from "fork" profiles to general star topologies; and we conducted an initial implementation and case studies in SPIN model checking. The proposed project renewal will: (1) Complete the investigation of basic methods through star-topology aware heuristic functions. (2) Comprehensively tackle SPIN model checking, including liveness properties and combination with complementary reduction methods. (3) Further broaden the technique's application scope, investigating its use for probabilistic model checking on a fragment of the Jani language, and investigating its use for privacy-preserving cooperative multi-agent planning with shared resources.

• DFG Programme: Research Grants
• International Connection: Czech Republic, Denmark, Switzerland
• Cooperation Partners: Professor Dr. Malte Helmert; Dr. Antonin Komenda; Professor Dr. Alberto Lluch-Lafuente