关于具有不完美信息的可折叠下推竞技场上的策略推理

不完美信息策略逻辑（SLiR）是一种极具表达力的逻辑，用于表述分布式系统中战略能力的复杂性质。先前关于SLiR的工作聚焦于有限系统，并表明当系统控制状态的信息在玩家或系统组件间呈层次化时——即玩家或组件可依据各自对状态的了解全序排列——模型检测问题是可判定的。我们表明，在栈内容可见这一自然限制下，从有限系统转向由可折叠（高阶）下推系统生成的无限系统可保持可判定性。证明思路与有限系统情形一致，但需要使用（可折叠）交替下推树自动机。此类自动机不可判定，但半交替下推树自动机被提出并证为可判定，用以研究双玩家下推系统上的策略问题。为处理具有层次化信息的多玩家情形，我们进一步精炼这些自动机：定义方向引导的（可折叠）下推树自动机，并证明其关于投影、非确定化与收窄运算保持封闭。对于后者（用于处理不完美信息），在可见栈系统中使用时所满足的某些假设下封闭性成立。我们随后利用这些自动机证明了主要结果。