A Behavioral Hierarchy of Strategy Logic

Starting from the seminal work introducing Alternating Temporal Logic, formalisms for strategic reasoning have assumed a prominent role in multi-agent systems verification. Among the others, Strategy Logic (SL) allows to represent sophisticated solution concepts, by treating agent strategies as first-order objects. A drawback from the high power of SL is to admit non-behavioral strategies: a choice of an agent, at a given point of a play, may depend on choices other agents can make in the future or in counterfactual plays. As the latter moves are unpredictable, such strategies cannot be easily implemented, making the use of the logic problematic in practice. In this paper, we describe a hierarchy of SL fragments as syntactic restrictions of the recently defined Boolean-Goal Strategy Logic (SL[BG]). Specifically, we introduce Alternating-Goal Strategy Logic (SL[AG]) that, by imposing a suitable alternation over the nesting of the Boolean connectives in (SL[BG]), induces two dual chains of sets of formulas, the conjunctive and disjunctive ones. A formula belongs to the level i of the conjunctive chain if it just contains conjunctions of atomic goals together with a unique formula belonging to the disjunctive chain of level i-1. The disjunctive chain is defined similarly. We formally prove that classic and behavioral semantics for (SL[ag]) coincide. Additionally, we study the related model-checking problem showing that it is 2ExpTime-complete.