Hyper Strategy Logic
This work addresses the limitation of existing strategy logics in multi-agent systems by enabling hyperproperty-based reasoning, which is incremental but expands the scope to capture more complex strategic interactions.
The paper introduces Hyper Strategy Logic (HyperSL), a temporal logic that extends Strategy Logic to compare multiple strategy profiles using hyperproperties, enabling expression of properties like non-interference and quantitative Nash equilibria that were previously inexpressible. It presents a decidable model-checking algorithm for an expressive fragment, with a prototype implementation and encouraging experimental results.
Strategy logic (SL) is a powerful temporal logic that enables strategic reasoning in multi-agent systems. SL supports explicit (first-order) quantification over strategies and provides a 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, including non-interference, quantitative Nash equilibria, optimal adversarial planning, and reasoning under imperfect information. On the algorithmic side, we identify an expressive fragment of HyperSL with decidable model checking and present a model-checking algorithm. We contribute a prototype implementation of our algorithm and report on encouraging experimental results.