Dependences in Strategy Logic

TL;DR

This paper investigates strategy dependences in Strategy Logic, refining existing models, and identifies a large fragment where model checking is feasible within 2EXPTIME, addressing complexity and semantics issues.

Contribution

It introduces refined dependence types in SL and proves that model checking for a significant fragment is decidable in 2EXPTIME.

Findings

Different dependence types lead to distinct satisfaction relations.

A large fragment of SL with strategy observation dependence admits 2EXPTIME model checking.

Refined dependence analysis improves understanding of SL semantics and verification complexity.

Abstract

Strategy Logic (SL) is a very expressive logic for specifying and verifying properties of multi-agent systems: in SL, one can quantify over strategies, assign them to agents, and express properties of the resulting plays. Such a powerful framework has two drawbacks: first, model checking SL has non-elementary complexity; second, the exact semantics of SL is rather intricate, and may not correspond to what is expected. In this paper, we focus on strategy dependences in SL, by tracking how existentially-quantified strategies in a formula may (or may not) depend on other strategies selected in the formula. We study different kinds of dependences, refining the approach of [Mogavero et al., Reasoning about strategies: On the model-checking problem, 2014], and prove that they give rise to different satisfaction relations. In the setting where strategies may only depend on what they have observed, we identify a large fragment of SL for which we prove model checking can be performed in 2EXPTIME.