Star-Topology Decoupled State Space Search

星形拓扑解耦状态空间搜索

• 批准号: 289186625
• 负责人: Professor Dr. Jörg Hoffmann
• 金额: --
• 依托单位: Fachbereich Informatik
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2016
• 资助国家: 德国
• 起止时间: 2015-12-31 至 2021-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/289186625?language=en
• 关键词: Star; Topology; Decoupled; State; Space

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.

状态空间搜索是一种基本的方法来解决分析或决策问题制定使用大型过渡系统。状态捕获某些系统或模型在（离散）时间步的快照，转换捕获状态如何在下一步中改变，任务是证明具有特定属性的转换路径的存在或不存在。这种问题发生在CS的几个子领域，包括人工智能规划，其中代理需要选择导致其目标的动作，以及分析某些程序或系统模型属性的模型检查。所有这些应用程序的共同挑战是状态空间爆炸：转换系统的大小与其描述的大小呈指数关系。作者在本项目的前期工作中为AI规划设计的星形拓扑解耦是解决这一挑战的新方法。它将状态空间模型视为由单个中心组件和多个叶子组件组成，其中中心与每个叶子交互，但叶子仅通过中心交互。自然的例子包括客户端-服务器架构和共享资源的合作代理。解耦搜索利用了在这种情况下出现的一种特殊的“条件独立性”：给定中心的固定转换路径，每个叶子的可能的中心兼容路径相互独立。因此，我们可以只搜索中心路径，并分别为每个叶子维护中心兼容路径。这可以指数地减少状态空间的大小，并且比已知的技术如偏序约简和Petri网展开更指数地减少。基准测试的实证结果显示，在具有明显星星拓扑的示例中，性能得到了实质性的（有时是戏剧性的）改善。因此，星型拓扑解耦有可能成为有效的状态空间搜索的基本方法之一，跨CS子区域。在第一个资助阶段，我们通过符号表示、半状态支配、偏序约简和对称约简，使算法组件成熟;我们将结构范围从“fork”轮廓扩展到一般的星星拓扑;我们进行了SPIN模型检测的初步实现和案例研究。本计画将：（1）利用星型拓扑启发式函数完成基本方法的研究。(2)全面处理SPIN模型检查，包括活性属性和与互补约简方法的组合。(3)进一步扩大技术的应用范围，调查其使用的概率模型检查的一个片段的Jani语言，并调查其使用的隐私保护合作多代理规划共享资源。