一句话：提出单目标策略逻辑 SL[1G]，证明其具有有界树模型性质且可满足性是 2ExpTime 可判定的。
策略逻辑（SL）将策略作为一阶对象显式推理，能统一 ATL、ATL* 等博弈逻辑，但表达力过强导致模型检测非初等、可满足性不可判定（Σ₁¹）。本文引入单目标策略逻辑 SL[1G]：它是 SL 的语法片段，要求公式处于前束范式，且每次对智能体进行策略量化时只涉及单个时序目标，严格包含 ATL*。作者证明 SL[1G] 具有有界树模型性质，并给出可满足性判定程序，其上界为 2ExpTime，与 ATL* 相同，从而在保持较强表达力的同时恢复可判定性。
Strategy Logic (SL, for short) has been introduced by Mogavero, Murano, and Vardi as a useful formalism for reasoning explicitly about strategies, as first-order objects, in multi-agent concurrent games. This logic turns out to be very powerful, subsuming all major previously studied modal logics for strategic reasoning, including ATL, ATL*, and the like. Unfortunately, due to its high expressiveness, SL has a non-elementarily decidable model-checking problem and the satisfiability question is undecidable, specifically Sigma_1^1. In order to obtain a decidable sublogic, we introduce and study here One-Goal Strategy Logic (SL[1G], for short). This is a syntactic fragment of SL, strictly subsuming ATL*, which encompasses formulas in prenex normal form having a single temporal goal at a time, for every strategy quantification of agents. We prove that, unlike SL, SL[1G] has the bounded tree-model property and its satisfiability problem is decidable in 2ExpTime, thus not harder than the one for ATL*.Comment: arXiv admin note: text overlap with arXiv:1112.6275, arXiv:1202.1309
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{MogaveroMPV16,
title = {Reasoning about Strategies: on the Satisfiability Problem},
author = {Fabio Mogavero and Aniello Murano and Giuseppe Perelli and Moshe Y. Vardi},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 1},
year = {2017},
doi = {10.23638/lmcs-13(1:9)2017}
}