Verifying Pushdown Multi-Agent Systems against Strategy Logics
Verifying Pushdown Multi-Agent Systems against Strategy Logics
复制标题
DOI：
--
复制
发表时间：
2016-07
期刊：
影响因子：
--
通讯作者：
Taolue Chen;Fu Song;Zhilin Wu
中科院分区：
文献类型：
--
作者：
Taolue Chen;Fu Song;Zhilin Wu
本文研究了基于下推博弈结构(PGSS)建模的下推多智能体系统中策略逻辑变体的模型检测算法。我们考虑了战略逻辑的各种片段，即SL[CG]、SL[DG]、SL[1G]和BSIL。我们证明了关于SL[CG]、SL[DG]和SL[1G]的PGSS上的模型检验问题是3EXTIME-完全的，这并不比包含逻辑ATL*的问题难。当涉及到BSIL时，模型检测问题变成2EXPTIME-完全问题。我们的算法是自动机理论的，基于饱和技术，易于实现。
In this paper, we investigate model checking algorithms for variants of strategy logic over pushdown multi-agent systems, modeled by pushdown game structures (PGSs). We consider various fragments of strategy logic, i.e., SL[CG], SL[DG], SL[1G] and BSIL. We show that the model checking problems on PGSs for SL[CG], SL[DG] and SL[1G] are 3EXTIME-complete, which are not harder than the problem for the subsumed logic ATL*. When BSIL is concerned, the model checking problem becomes 2EXPTIME-complete. Our algorithms are automata-theoretic and based on the saturation technique, which are amenable to implementations.