提出新方法，让智能体满足更复杂的概率安全约束。
Synthesis of Safety Specifications for Probabilistic Systems
- 构建CPCTL框架，将全局安全约束转化为局部可处理条件
- 基于价值迭代算法求解，支持更广泛PCTL性质的合成
- 理论完备且适用于高风险场景中的智能体安全设计
在安全关键环境中，确保智能体满足安全规范至关重要。现有控制器合成方法通常仅支持概率规避类约束，表达能力有限。本文提出一种新方法，支持以概率计算树逻辑（PCTL）表达的更一般时序安全规范。贡献有二：首先，建立安全-PCTL规范的理论框架，通过将全局规范满足性归约为局部约束，定义了安全-PCTL的一个子集CPCTL，证明其在合成问题中的适用性；其次，基于该理论，提出一种基于值迭代的算法来求解此类更复杂时序性质的合成问题，并证明了方法的正确性与完备性。
原文摘要 · Abstract (English)
Ensuring that agents satisfy safety specifications can be crucial in safety-critical environments. While methods exist for controller synthesis with safe temporal specifications, most existing methods restrict safe temporal specifications to probabilistic-avoidance constraints. Formal methods typically offer more expressive ways to express safety in probabilistic systems, such as Probabilistic Computation Tree Logic (PCTL) formulas. Thus, in this paper, we develop a new approach that supports more general temporal properties expressed in PCTL. Our contribution is twofold. First, we develop a theoretical framework for the Synthesis of safe-PCTL specifications. We show how the reducing global specification satisfaction to local constraints, and define CPCTL, a fragment of safe-PCTL. We demonstrate how the expressiveness of CPCTL makes it a relevant fragment for the Synthesis Problem. Second, we leverage these results and propose a new Value Iteration-based algorithm to solve the synthesis problem for these more general temporal properties, and we prove the soundness and completeness of our method.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。