TY - JOUR
AU - Acar, Erman
AU - Benerecetti, Massimo
AU - Mogavero, Fabio
PY - 2019/07/17
Y2 - 2022/12/03
TI - Satisfiability in Strategy Logic Can Be Easier than Model Checking
JF - Proceedings of the AAAI Conference on Artificial Intelligence
JA - AAAI
VL - 33
IS - 01
SE - AAAI Technical Track: Knowledge Representation and Reasoning
DO - 10.1609/aaai.v33i01.33012638
UR - https://ojs.aaai.org/index.php/AAAI/article/view/4112
SP - 2638-2645
AB - <p>In the design of complex systems, <em>model-checking</em> and <em>satisfiability</em> arise as two prominent decision problems. While model-checking requires the designed system to be provided in advance, satisfiability allows to check if such a system even exists. With very few exceptions, the second problem turns out to be harder than the first one from a complexity-theoretic standpoint. In this paper, we investigate the connection between the two problems for a non-trivial fragment of <em>Strategy Logic</em> (SL, for short). SL extends LTL with first-order quantifications over strategies, thus allowing to explicitly reason about the strategic abilities of agents in a multi-agent system. Satisfiability for the full logic is known to be highly undecidable, while model-checking is non-elementary.</p><p>The SL fragment we consider is obtained by preventing strategic quantifications within the scope of temporal operators. The resulting logic is quite powerful, still allowing to express important game-theoretic properties of multi-agent systems, such as existence of <em>Nash and immune equilibria</em>, as well as to formalize the <em>rational synthesis</em> problem. We show that satisfiability for such a fragment is PSPACE-COMPLETE, while its model-checking complexity is 2EXPTIME-HARD. The result is obtained by means of an elegant encoding of the problem into the satisfiability of <em>conjunctive-binding first-order logic</em>, a recently discovered decidable fragment of first-order logic.</p>
ER -