arXiv 1010.02252010-10cs.LO

S5和sub-S5认知时态逻辑中使用下一步时态算子刻画完全召回

Characterizing perfect recall using next-step temporal operators in S5 and sub-S5 Epistemic Temporal Logic

Andreas Witzel

摘要：

我们回顾了解释系统，博弈论和认知逻辑的文献中的完美回忆的概念。在认知时态逻辑（ETL）的背景下，我们给了（据我们所知）一个新的框架条件完美的回忆，这是本地的，可以直接翻译成一个定义公式的语言，只有下一步的时间运营商。这个框架条件也产生了一个完整的公理化的S5 ETL框架与完美的召回。然后，我们考虑如何扩展和巩固的概念，完美的回忆在sub-S5设置，讨论的各种概念不再是等同的。

英文摘要：

We review the notion of perfect recall in the literature on interpreted systems, game theory, and epistemic logic. In the context of Epistemic Temporal Logic (ETL), we give a (to our knowledge) novel frame condition for perfect recall, which is local and can straightforwardly be translated to a defining formula in a language that only has next-step temporal operators. This frame condition also gives rise to a complete axiomatization for S5 ETL frames with perfect recall. We then consider how to extend and consolidate the notion of perfect recall in sub-S5 settings, where the various notions discussed are no longer equivalent.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

具有同步和完全回忆语义的认知μ演算的模型检验

Model-checking an Epistemic μ-calculus with Synchronous and Perfect Recall Semantics

我们证明了模型检验问题对于认知μ演算的一个片段是可判定的。该片段允许自由变量的范围内的认知模态的限制形式，避免构建公式体现任何形式的共同知识。我们的演算包含已知的可判定的片段的认识CTL/LTL。它的模态变体可以表示两人博弈中的获胜策略，其中一个玩家具有不完美信息和不可观察的目标，并且，通过适当的编码，具有不完美信息和完美召回的ATL的模型检验问题的可判定实例可以编码为这种认知μ-演算的模型检验问题的实例。

2012-07-14cs.LO

具有同步和完全回忆语义的认知μ演算的模型检验

Model Checking an Epistemic mu-calculus with Synchronous and Perfect Recall Semantics

我们确定了一个子问题的模型检查问题的认知μ演算是可判定的。在这个子问题的实例中，公式允许在认知模态的范围内以限制的形式存在自由变量，以避免体现任何形式的共同知识。我们的子问题包含已知的可判定片段的认知CTL/LTL，可以表示获胜策略，在两个玩家的游戏中，一个玩家有不完美的信息和不可观察的目标，并与一个合适的编码，可判定的实例的模型检查问题的ATLiR。

2013-10-23cs.GTcs.LO

模型检验概率时间认知逻辑的不可判定案例（扩展摘要）

Undecidable Cases of Model Checking Probabilistic Temporal-Epistemic Logic (Extended Abstract)

我们调查的时间，知识和概率的模型检查逻辑的可判定性，相对于两个认知语义：时钟和同步完美召回部分观察离散时间马尔可夫链的语义。可判定性的结果是已知的某些限制逻辑关于这些语义，受到各种各样的限制，要么是无法解释的，或涉及一个长期未解决的数学问题。我们表明，温和的推广已知的可判定的情况下，足以使模型检验问题明确不可判定。特别地，对于同步完美召回，从有限到达的时态算子到无限到达的算子的推广使得模型检验不可判定。时钟语义的情况下是密切相关的时间和概率的一元二阶逻辑，已知是可判定的，除了一组测量零。我们表明，这种逻辑的两个不同的扩展，使模型检验不可判定。其中之一涉及概率项的多项式组合，另一个涉及到概率算子范围内的一元二阶量化。这些结果解释了以前工作中的一些限制。

2016-06-24cs.LO

概率时间认知逻辑中模型检验的不可判定情形

Undecidable Cases of Model Checking Probabilistic Temporal-Epistemic Logic

2015-11-10cs.LO

使用过去时间时态认知逻辑的并发组合验证

Compositional Verification of Concurrency Using Past-Time Temporal Epistemic Logic

KTH Royal Institute of Technology（皇家理工学院）

提出一种过去时间时态认知逻辑，用于形式化共享内存并发中的基于局部视图的推理，并在Peterson互斥算法上验证其有效性，同时展示该逻辑如何嵌入依赖-保证推理。

2026-06-24cs.LO

统一超时间逻辑和认知时间逻辑

Unifying Hyper and Epistemic Temporal Logic

在文献中，已经提出了两个强大的时序逻辑形式主义表达信息流的安全性要求，在一般情况下，超越常规的属性。一个是经典的，基于认知逻辑的知识模态。另一个，所谓的超逻辑，是最近的，包括许多建议，从文献中，它是基于明确的和同时量化多个路径。为了更好地理解这些逻辑如何相互比较，我们考虑了逻辑KCTL*（CTL* 的知识模态和同步完美回忆语义的扩展）和HyperCTL*。我们首先确定KCTL* 和HyperCTL* 在表达上是不可比的。其次，我们引入并研究了HyperCTL* 的自然线性过去扩展，以统一KCTL* 和HyperCTL*;事实上，我们表明KCTL* 可以很容易地在线性时间内转换为所提出的逻辑。此外，我们证明了这种新的逻辑的模型检测问题是可判定的，我们提供了它的确切的计算复杂性方面的一个新的措施的路径量词的交替。为此，我们解决了开放的复杂性问题，无限制的量化命题时序逻辑。

2014-09-09cs.LO

更多相关论文收起更多论文

带过去时态的无主体交替认知度量时态逻辑：模型检查与复杂性

Agent-Alternation-Free Epistemic Metric Temporal Logic with Past: Model Checking and Complexity

Université Paris-Saclay（巴黎萨克雷大学）；CNRS（法国国家科学研究中心）；ENS Paris-Saclay（巴黎萨克雷高等师范学校）；LMF（拉格兰日数学实验室）；Institut Universitaire de France（法兰西学院）；Direction Générale de l’Armement（法国国防总局）

研究带过去时态的无主体交替认知度量时态逻辑的模型检查，通过结合时态测试自动机与完美回忆观察者进行分析，证明其模型检查为EXPSPACE完全，给出了该逻辑在特定条件下的复杂性结论。

2026-07-16cs.FLcs.LO

描述成功的公式：多代理案例

Characterizing Successful Formulas: the Multi-agent Case

公告逻辑中成功公式的刻画是动态认知逻辑中的一个著名的开放问题。最近，Holliday和ICard给出了单主体情形的完整刻画.然而，对于多智能体情况的问题是开放的。本文给出了这个问题的部分解决方案，刻画了由一元运算符构成的语言子类，并讨论了给出完整解决方案的方法。

2012-09-05cs.LOcs.MA

认知逻辑和条件逻辑的集合论完备性

Set-Theoretic Completeness for Epistemic and Conditional Logic

在哲学和数学文献中，逻辑的标准方法是定义一种语言，这种方法也被计算机科学所采用（语法），一个适当的模型类以及语言中公式的解释（语义学），公理和推理规则的集合，表征推理（证明理论），然后通过可靠性和完整性结果将证明理论与语义联系起来。在这里，我们考虑一种在经济学文献中更常见的方法，它纯粹在语义，集合论层面上工作。我们提供了一些认知和条件逻辑的集合论完备性结果，并对比了句法和集合论方法的表达能力

2000-05-30cs.AIcs.LO

认知时间逻辑中的变化观察

Changing Observations in Epistemic Temporal Logic

ENS Rennes（雷恩高等师范学院）；University of Naples “Federico II”（那不勒斯费德里科二世大学）

我们研究了知识和时间逻辑中主体观察力的动态变化。我们认为CTL*K，扩展CTL* 与知识运营商，并丰富它与一个新的运营商，模拟一个代理的方式观察系统的变化。我们扩展了经典的语义知识的完美召回代理占观察的变化，我们表明，这个新的运营商严格增加了CTL*K的表达能力。我们减少模型检查问题，我们的逻辑CTL*K，这是已知的可判定的。这为我们的逻辑提供了模型检查问题的解决方案，但其复杂性不是最佳的。事实上，我们提供了一个更好的复杂性直接决策过程。

2018-09-03cs.AIcs.LOcs.MA

知道如何计划

Knowing How to Plan

Nankai University（南开大学）；Peking University（北京大学）

在最近的文献中，已经研究了各种基于规划的专有技术逻辑。在本文中，我们使用这样的逻辑做专有技术为基础的规划，通过模型检验。特别是，我们可以处理涉及专有技术公式作为目标的高阶认知规划，例如，找到一个计划来确保p，这样对手就不知道如何在未来使p为假。给出了有限认知迁移系统上模型检验问题的PTIME算法，并在完全召回假设下公理化了该逻辑。

2021-06-22cs.AIcs.LO

多智能体系统一阶逻辑中知识与时间的相互作用：完备性结果

Interactions between Knowledge and Time in a First-Order Logic for Multi-Agent Systems: Completeness Results

Imperial College London（伦敦帝国理工学院）

研究了一类用于多智能体系统推理的一阶时间认知逻辑。我们编码系统的典型属性，包括完美的回忆，同步性，无学习，并具有独特的初始状态的变量的量化解释系统，解释系统的一阶扩展。我们确定了几个单音节片段的一阶时间认知逻辑，并显示其完整性相对于其相应的类的量化解释系统。

2014-01-23cs.AIcs.LOcs.MA

分布式系统中的因果关系、知识与协调

Causality, Knowledge and Coordination in Distributed Systems

在分布式系统中实现跨远程站点的协调是分布式计算的重要组成部分，也是一个固有的挑战。1978年，Leslie Lamport提出了异步系统中的通信分析。Lamport的分析确定了时间优先的概念，这是一种弱时间概念，在异步系统中是缺失的。这一概念已被广泛用于各种应用中。然而，分析仅限于异步系统。在这篇论文中，我们超越了研究因果关系的同步系统。在这样的系统中，因果影响的边界并不完全由信息传递来划定。在这里，时间本身，对所有过程来说，都以一种统一的（或几乎统一的）速率流逝，也是一种媒介，因果影响可以通过它扇出。本论文研究，并描述，时间和信息传递的组合，在同步系统中的因果关系的影响。事实证明，基于知识的分析[FHMV]提供了一个定制的正式框架内，因果概念可以研究。正如我们所展示的，知识的形式概念非常适合于用信息流来表征因果影响，扩展了Chandy和Misra在[ChM]中的分析。我们定义了几个通用类的协调问题，对参与进程提出了各种时间顺序的要求。这些协调问题提供了现实生活需求的自然概括。然后，我们分析的因果关系的条件下，这些问题的适当解决方案。分析分两个阶段进行：第一，时间顺序的要求减少到认知条件。然后，这些认知条件的特点是因果关系的沟通模式，是必要的和足够的，使他们。

2011-12-19cs.DCcs.LO