Star-Topology Decoupled State Space Search

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

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.