标记有限状态自动机的二阶既往状态不透明性

在本文中，我们形式化如下场景：一个智能体永远无法确信另一个智能体能基于其在当前及任何过去时刻对该自动机的观测唯一确定其状态，将此性质称为二阶既往状态不透明性。基于我们的并发复合与经典观测器，我们导出一种在双指数时间内验证该性质的工具。这一结果的意义在于，我们将有限自动机的推断从单一智能体扩展至两个有序智能体。