Taming Strategy Logic: Non-Recurrent Fragments.

Strategy Logic (SL for short) is one of the prominent languages for reasoning about the strategic abilities of agents in a multi-agent setting. This logic extends LTL with first-order quantifiers over the agent strategies and encompasses other formalisms, such as ATL* and CTL*. The model-checking problem for SL and several of its fragments has been extensively studied. On the other hand, the picture is much less clear on the satisfiability front, where the problem is undecidable for the full logic. In this work, we study two fragments of One -Goal SL, where the nesting of sentences within temporal operators is constrained. We show that the satisfiability problem for these two logics, and for the corresponding fragments of ATL* and CTL*, is in EXPSPACE and PSPACE-COMPLETE, respectively.(c) 2023 The Author(s). Published by Elsevier Inc. This is an open access article under the CC BY license (http://creativecommons .org /licenses /by /4 .0/).