Hyper Strategy Logic
Raven Beutner, Bernd Finkbeiner
Strategy logic (SL) is a powerful temporal logic that enables strategic reasoning in multi-agent systems. SL supports explicit (first-order) reasoning over strategies and provides a natural logical framework to express many important properties such as Nash equilibria, dominant strategies, etc. While in SL the same strategy can be used in multiple strategy profiles, each such profile is evaluated w.r.t. a path-property, i.e., a property that considers the single path resulting from a particular strategic interaction. In this paper, we present Hyper Strategy Logic (HyperSL), a strategy logic where the outcome of multiple strategy profiles can be compared w.r.t. a hyperproperty, i.e., a property that relates multiple paths. We show that HyperSL can capture important properties that cannot be expressed in SL – such as non-interference, quantitative Nash equilibria, optimal adversarial planning, and reasoning under imperfect information – and subsumes many existing logics. On the algorithmic side, we identify an expressive fragment of HyperSL with decidable model checking and present a novel model-checking algorithm. We contribute a prototype implementation of our algorithm and report on encouraging experimental results.
23rd International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS 2024).