并发多玩家博弈中联盟目标分配的时序逻辑
计算机科学中的逻辑
2022-02-24 v3 计算机科学与博弈论
多智能体系统
摘要
我们引入并研究了交替时序逻辑 (ATL) 的一种自然扩展，称为联盟目标分配时序逻辑 (TLCGA)。它仅具有一个但极具表达力的联盟策略算子，即联盟目标分配算子，该算子基于一个映射，该映射为博弈中的每个玩家集合分配其联盟目标，该目标由 TLCGA 语言的一条路径公式形式化，即以时序算子 X、U 或 G 为前缀的公式，表示相应联盟的时序化目标，描述了满足该目标的那些游走路径的性质。我们在 TLCGA 的 mu-演算扩展中建立了时序目标分配的不动点特征，讨论了其表达能力并通过一些示例加以说明，证明了其针对适当定义的互模拟概念的互模拟不变性和 Hennessy-Milner 性质，为 TLCGA 构建了一个可靠且完备的公理系统，并利用有限模型性质获得了其可判定性。
引用
@article{arxiv.2012.14195,
title = {The temporal logic of coalitional goal assignments in concurrent multi-player games},
author = {Sebastian Enqvist and Valentin Goranko},
journal= {arXiv preprint arXiv:2012.14195},
year = {2022}
}