ATL +的博弈语义及其在模型检测中的应用
Game-Theoretic Semantics for ATL+ with Applications to Model Checking
摘要：
我们开发了完整的交替时间时态逻辑ATL* 的片段ATL+的博弈论语义（GTS），基本上扩展了最近推出的GTS ATL。我们首先表明，新的博弈论语义是等价的ATL+的标准语义（基于完美的召回策略）。然后，我们提供了一个分析，基于新的语义，模型检查ATL+所需的内存和时间资源。基于此，我们确定仅使用非常有限的内存量的策略就足以满足ATL+的需求。此外，使用GTS，我们提供了一个新的算法模型检查的ATL+和确定一个自然的层次结构的易处理的片段ATL+扩展ATL。
英文摘要：
We develop game-theoretic semantics (GTS) for the fragment ATL+ of the full Alternating-time Temporal Logic ATL*, essentially extending a recently introduced GTS for ATL. We first show that the new game-theoretic semantics is equivalent to the standard semantics of ATL+ (based on perfect recall strategies). We then provide an analysis, based on the new semantics, of the memory and time resources needed for model checking ATL+. Based on that, we establish that strategies that use only a very limited amount of memory suffice for ATL+. Furthermore, using the GTS we provide a new algorithm for model checking of ATL+ and identify a natural hierarchy of tractable fragments of ATL+ that extend ATL.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
