Decidable Model Checking with Uniform Strategies

Abstract

The logic of strategic ability Resource-Bounded Alternating Time Syntactic Epistemic Logic (RB+-ATSEL) has a decidable model-checking problem for coalition uniform strategies. A strategy is coalition uniform if agents in a coalition select the same joint action in all states where the knowledge of the coalition is the same. However, this presupposes free and unbounded communication between the agents in the coalition before every action selection. In this paper we present a modified version of RB+-ATSEL, RB+-ATSELc, with explicit (and explicitly costed) communication actions. RB+-ATSELc is interpreted on communication models which have an explicit communication step before every action selection. We show that, unlike standard ATL under imperfect information, the model checking problem for RB+-ATSELc is decidable under perfect recall uniform strategies. Our decidability result also applies to ATL with imperfect information and perfect recall when interpreted on communication models