带过去时态的无主体交替认知度量时态逻辑：模型检查与复杂性
Agent-Alternation-Free Epistemic Metric Temporal Logic with Past: Model Checking and Complexity
浏览论文内容
中文总结 AI 辅助
研究带过去时态的无主体交替认知度量时态逻辑的模型检查，通过结合时态测试自动机与完美回忆观察者进行分析，证明其模型检查为EXPSPACE完全，给出了该逻辑在特定条件下的复杂性结论。
中文摘要 AI 辅助
我们研究了带过去时态的认知度量时态逻辑的模型检查，该逻辑在同步完美回忆下对有限Büchi自动机进行解释。该逻辑受基于观察的验证问题（如诊断和不透明性）的推动，在这些问题中，观察者只能看到执行的投影并推断可能更早发生的事件。这些要求不涉及不同主体知识之间的交替。因此，我们考虑无主体交替片段，其中嵌套的知识运算符必须引用同一主体。我们证明该片段的模型检查是EXPSPACE完全的。即使只有一个主体、一个知识运算符出现且没有非平凡度量界限，下界也成立。对于上界，我们将时态测试自动机与完美回忆观察者相结合。由于过去公式在以相同系统状态结束的不可区分历史上可能具有不同的真值，观察者除了跟踪系统状态外，还必须跟踪时态自动机状态。
英文摘要
We study model checking for an epistemic metric temporal logic with past, interpreted over finite Büchi automata under synchronous perfect recall. The logic is motivated by observation-based verification problems such as diagnosis and opacity, where an observer sees only a projection of an execution and reasons about events that may have occurred earlier. These requirements use no alternation between different agents' knowledge. We therefore consider the agent-alternation-free fragment, in which nested knowledge operators must refer to the same agent. We show that model checking for this fragment is EXPSPACE-complete. The lower bound already holds with one agent, one occurrence of the knowledge operator, and no non-trivial metric bounds. For the upper bound, we combine temporal test automata with perfect-recall observers. Because past formulas may have different truth values on indistinguishable histories ending in the same system state, the observer must track temporal automaton states in addition to system states.
