证明了基于正则表达式的知识推理问题为2EXPTIME完全。
Reasoning About Knowledge on Regular Expressions is 2EXPTIME-complete
- 用正则表达式建模知识更新机制，刻画观察与预期匹配过程。
- 首次证明该逻辑的可满足性问题在2EXPTIME复杂度下可解且难于求解。
- 适合多智能体系统、认知规划领域的理论研究者阅读。
用于多智能体系统中知识与行动推理的逻辑已在多个领域得到应用，包括认知规划。基于对环境观察而产生的知识变化是此类规划场景的核心。公共观察逻辑（Public Observation Logic, POL）是一种基于公开宣告逻辑的变体，用于描述知识随公开观察结果更新。在每个可能世界（即克里普克模型中的状态）中，都配备一组预期观察值。当实际观察与预期匹配时，状态随之演化。本文证明，POL 的可满足性问题是 2EXPTIME 完全的。
原文摘要 · Abstract (English)
Logics for reasoning about knowledge and actions have seen many applications in various domains of multi-agent systems, including epistemic planning. Change of knowledge based on observations about the surroundings forms a key aspect in such planning scenarios. Public Observation Logic (POL) is a variant of public announcement logic for reasoning about knowledge that gets updated based on public observations. Each state in an epistemic (Kripke) model is equipped with a set of expected observations. These states evolve as the expectations get matched with the actual observations. In this work, we prove that the satisfiability problem of $\POL$ is 2EXPTIME-complete.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。