Strategy logic with imperfect information
Raphaël Berthon, Bastien Maubert, Aniello Murano, Sasha Rubin, Moshe Y. Vardi · 2017
We introduce an extension of Strategy logic for the imperfect-information setting, called SLii, and study its model-checking problem. As this logic naturally captures multi-player games with imperfect information, the problem turns out to be undecidable. We introduce a syntactical class of “hierarchical instances” for which, intuitively, as one goes down the syntactic tree of the formula, strategy quantifications are concerned with finer observations of the model. We prove that model-checking SLiirestricted to hierarchical instances is decidable. This result, because it allows for complex patterns of existential and universal quantification on strategies, greatly generalises previous ones, such as decidability of multi-player games with imperfect information and hierarchical observations, and decidability of distributed synthesis for hierarchical systems. To establish the decidability result, we introduce and study QCTLii*, an extension of QCTL (itself an extension of CTL with second-order quantification over atomic propositions) by parameterising its quantifiers with observations. The simple syntax of QCTLii* allows us to provide a conceptually neat reduction of SLiito QCTLii* that separates concerns, allowing one to forget about strategies and players and focus solely on second-order quantification. While the model-checking problem of QCTLii* is, in general, undecidable, we identify a syntactic fragment of hierarchical formulas and prove, using an automata-theoretic approach, that it is decidable. The decidability result for SLiifollows since the reduction maps hierarchical instances of SLiito hierarchical formulas of QCTLii*.