On the Boundary of Behavioral Strategies

In the setting of multi-agent games, considerable effort has been devoted to the definition of modal logics for strategic reasoning. In this area, a recent contribution is given by the introduction of Strategy Logic (SL, for short) by Mogavero, Murano, and Vardi. This logic allows to reason explicitly about strategies as first order objects and express in a very natural and elegant way several solution concepts like Nash, resilient, and secure equilibria, dominant strategies, etc. The price that one has to pay for the high expressiveness of SL semantics is that agents strategies it admits may be not behavioral, i.e., a choice of an agent, at a given moment of a play, may depend on the choices another agent can make in another counterfactual play. As the latter moves are unpredictable, this kind of strategies cannot be synthesized in practice. In this paper, we investigate two syntactical fragments of SL, namely the conjunctive-goal and disjunctive-goal, called SL[CG] and SL[DG] for short, and prove that their semantics admit behavioral strategies only. These logics are obtained by forcing SL formulas to be only of the form of conjunctions or disjunctions of goals, which are temporal assertions associated with a binding of agents with strategies. As SL formulas with any Boolean combination of goals turn out to be non behavioral, we have that SL[CG] and SL[DG] represent the maximal fragments of SL describing agent behaviors that are synthesizable. As a consequence of the above results, the model-checking problem for both SL[CG] and SL[DG] is shown to be solvable in 2EXPTIME, as it is for the subsumed logic ATL*.