PaperlayerView exact revision on arXiv

Source-linked AI summary

Reasoning About Strategies: On the Model-Checking Problem

Fabio Mogavero, Aniello Murano, Giuseppe Perelli, Moshe Y. Vardi

arXiv:1112.6275v2cs.LOcs.MAmath.LO

TL;DR

The paper addresses limitations in explicit strategy reasoning for multi-agent systems by introducing SL for concurrent games and studying tractable syntactic fragments. It proves decidable but highly complex model checking for SL, while showing that SL[1G] achieves 2EXPTIME-completeness and strictly extends ATL∗.

  • Problem

    CHP-SL explicitly quantifies over strategies but is limited to two-agent turn-based games and weak strategy commitment, motivating a more general framework.

  • Method

    The paper introduces SL for concurrent multi-agent games and analyzes the fragments SL[NG], SL[BG], and SL[1G] using automata-theoretic model-checking procedures.

  • Results

    SL model checking is decidable but non-elementary, while SL[1G] is 2EXPTIME-COMPLETE and SL[BG] includes CHP-SL.

  • Takeaways & Limitations

    SL provides a more general explicit strategy framework, while SL[1G] strictly subsumes ATL∗ without exceeding its stated model-checking complexity.

  • Takeaways & Limitations

    SL[BG] lacks an elementary model-checking procedure, and the paper leaves open whether one exists.

Abstract

from arXiv · show

In open systems verification, to formally check for reliability, one needs an appropriate formalism to model the interaction between agents and express the correctness of the system no matter how the environment behaves. An important contribution in this context is given by modal logics for strategic ability, in the setting of multi-agent games, such as ATL, ATL\star, and the like. Recently, Chatterjee, Henzinger, and Piterman introduced Strategy Logic, which we denote here by CHP-SL, with the aim of getting a powerful framework for reasoning explicitly about strategies. CHP-SL is obtained by using first-order quantifications over strategies and has been investigated in the very specific setting of two-agents turned-based games, where a non-elementary model-checking algorithm has been provided. While CHP-SL is a very expressive logic, we claim that it does not fully capture the strategic aspects of multi-agent systems. In this paper, we introduce and study a more general strategy logic, denoted SL, for reasoning about strategies in multi-agent concurrent games. We prove that SL includes CHP-SL, while maintaining a decidable model-checking problem. In particular, the algorithm we propose is computationally not harder than the best one known for CHP-SL. Moreover, we prove that such a problem for SL is NonElementarySpace-hard. This negative result has spurred us to investigate here syntactic fragments of SL, strictly subsuming ATL\star, with the hope of obtaining an elementary model-checking problem. Among the others, we study the sublogics SL[NG], SL[BG], and SL[1G]. They encompass formulas in a special prenex normal form having, respectively, nested temporal goals, Boolean combinations of goals and, a single goal at a time. About these logics, we prove that the model-checking problem for SL[1G] is 2ExpTime-complete, thus not harder than the one for ATL\star.

1. INTRODUCTION

The paper develops Strategy Logic (SL) to reason explicitly about strategies in concurrent multi-agent games, addressing expressive limitations of CHP-SL. It establishes decidability and studies fragments that retain greater tractability, especially SL[1G].

  • Background: ATL∗ reasons about coalition strategies in concurrent games, but treats strategies implicitly through strategic modalities.Its model-checking and satisfiability problems are 2EXPTIME-COMPLETE.
  • Limitations of CHP-SL: CHP-SL makes strategies explicit through first-order quantification, but is restricted to two-player turn-based games and weak strategy commitment.It cannot let different players share one strategy or let one agent change strategy independently during a play.
  • Strategy Logic: SL extends LTL with existential and universal strategy quantifiers plus agent binding for concurrent multi-agent games.These constructs select strategies and bind agents to them, including bindings that require multiple agents to share a strategy.
  • Strategy Logic: SL model checking is decidable, with complexity PTIME in the model size and NONELEMENTARYTIME in the specification size.The automata-theoretic procedure uses alternating parity tree automata; eliminating strategy quantifiers causes repeated exponential blow-ups.
  • Syntactic fragments: The paper studies SL[NG], SL[BG], and SL[1G], restricting formulas to nested goals, Boolean combinations of goals, and one temporal goal at a time.These fragments are designed to subsume ATL∗ while seeking better model-checking complexity.
  • Syntactic fragments: SL[1G] model checking is 2EXPTIME-COMPLETE, while SL[NG] is NONELEMENTARYTIME- and NONELEMENTARYSPACE-hard and SL[BG] includes CHP-SL.The SL[1G] result matches the stated complexity bound for ATL∗ model checking.

2. STRATEGY LOGIC

Strategy Logic (SL) extends LTL with explicit strategy quantification and agent binding over concurrent multi-agent games. Its syntax supports strategic properties, including equilibria, that ATL* and CHP-SL cannot express.

  • Underlying framework: SL is interpreted over concurrent game structures, where agents choose actions concurrently as functions of play history.A CGS generalizes Kripke structures and labeled transition systems for multi-agent games.
  • Underlying framework: A CGS contains propositions, agents, actions, states, labeling, an initial state, and a transition function over joint decisions.Joint decisions assign one action to each agent, and transitions map states plus decisions to successor states.
  • Syntax: SL extends LTL with existential and universal strategy quantifiers plus agent binding to strategy variables.These constructs separately quantify strategies and associate them with agents.
  • Syntax: SL characterizes quantifier alternation because the number of strategy-quantifier switches affects the complexity of fragment decision problems.The syntax defines fragments SL[k-alt] by bounding alternation across subformulas.
  • Strategic properties: SL can express deterministic concurrent multi-player Nash equilibria and stable equilibria through explicit strategy assignments and deviations.In the prisoner’s dilemma example, mutual defection forms a stable equilibrium, while mutual cooperation forms an unstable equilibrium.
  • Strategic properties: The paper presents SL properties that are expressible in SL but neither in ATL* nor in CHP-SL.This illustrates the additional strategic expressiveness targeted by explicit strategy reasoning.

3. MODEL-CHECKING HARDNESS

This section establishes non-elementary lower bounds for SL model checking by reducing QPTL satisfiability to model checking on a constant-size, one-agent CGS. The reduction yields k-EXPSPACE hardness for formulas with alternation number k.

  • QPTL: QPTL formulas use Boolean and temporal operators together with existential and universal proposition quantifiers.The grammar includes X, F, G, ∃p, and ∀p, while temporal and propositional truth evaluations define satisfaction.
  • Reduction: The hardness proof reduces QPTL satisfiability to SL model checking through a one-agent, constant-size concurrent game structure.The reduction uses the turn-based CGS GRdc and a translation from QPTL formulas into SL formulas.
  • Reduction: The translation preserves formula alternation number and establishes equivalence between QPTL satisfiability and satisfaction of the corresponding SL formula on GRdc.The induction relates proposition valuations to strategies assigned to variables in the constructed game structure.
  • Proof: The proof presents the atomic-proposition and proposition-quantifier induction cases, while leaving Boolean and temporal cases straightforward.The existential and universal cases connect proposition truth evaluations with strategy assignments.
  • Hardness result: k-EXPSPACE-HARDNESS holds for TB-SL[k-alt] and SL[k-alt] model checking.The bound follows from the corresponding QPTL[k-alt] satisfiability hardness and applies for alternation number k.

4. STRATEGY QUANTIFICATIONS

This section defines syntactic SL fragments and develops dependence-map and elementariness results that explain when elementary model checking is possible. It establishes strict expressiveness beyond ATL* and identifies SL[1G] as the fragment with elementary complexity.

  • Syntactic fragments: SL[NG], SL[BG], and SL[1G] restrict formulas to nested goals, Boolean combinations of goals, and one goal per temporal formula, respectively.SL[BG] avoids nested goals sharing variables from one quantification prefix, while SL[1G] uses a separate prefix for each goal.
  • Syntactic fragments: SL[1G] is strictly more expressive than ATL*, with an SL[1G, 3-ag, fvs, 2-alt] sentence having no ATL* equivalent.The separation uses two concurrent game structures that ATL* cannot distinguish but the SL[1G] sentence can.
  • Dependence Maps: Dependence maps capture how existentially quantified strategies may depend on preceding universal variables, formalized by the dependence pairs induced by a quantification prefix.The strategy-quantification theorem characterizes satisfaction using a dependence map applied uniformly across universal assignments.
  • Dependence Maps: Non-elementary dependence maps exist, while prefixes with an existential block followed by a universal block admit only elementary dependence maps.The latter class is maximal among the stated prefix classes with this guarantee.
  • Elementariness and non-elementariness: Elementary semantics restrict existential strategy choices to depend only on same-track values of previously quantified strategies, excluding future and parallel-track choices.For SL[NG], elementary satisfiability implies ordinary satisfiability; for SL[1G], the two semantics coincide.
  • Elementariness and non-elementariness: SL[BG] can contain satisfiable prenex sentences that are not elementarily satisfiable, a phenomenon already present for CHP-SL.This shows that ordinary satisfiability and elementary satisfiability need not coincide in the broader fragments.

5. MODEL-CHECKING PROCEDURES

The paper develops automata-theoretic model-checking procedures for SL and its fragments, establishing non-elementary complexity for SL and elementary complexity for SL[1G].

  • The procedures reduce SL model checking to emptiness problems for alternating parity tree automata and use bottom-up labeling of CGS states by satisfied subsentences.The construction recursively handles principal subsentences, leaving LTL temporal goals inside Boolean combinations and goal nesting.
  • The automata framework defines alternating tree automata with positive Boolean transitions, runs over labeled trees, and parity or co-Büchi acceptance conditions.An alternating automaton can send multiple copies to the same successor, while parity acceptance depends on states recurring infinitely often along branches.
  • APT direction projection transforms an alternating parity tree automaton into a nondeterministic parity tree automaton with m · 2^O(k·n·log n) states and index O(k · n · log n).The transformation preserves acceptance after augmenting tree labels with the distinguished-direction information.
  • SL Model Checking: SL model checking is PTIME-COMPLETE in model size and NONELEMENTARYTIME in specification size.The resulting automaton has |StG| · (2 ↑↑m m) states and index 2 ↑↑m m, yielding the stated specification complexity.
  • SL[NG] Model Checking: SL[NG] model checking is PTIME-COMPLETE in model size and (k+1)-EXPTIME in specification size, where k is the maximum quantifier alternation.The bottom-up procedure verifies each principal subsentence at every model state.
  • SL[1G] Model Checking: SL[1G] uses universal co-Büchi automata and elementary dependence-state encodings to obtain an elementary procedure for single-goal principal sentences.The construction evaluates local strategy quantifications through action dependence maps and converts the resulting automata using direction projection.
  • SL[1G] Model Checking: SL[1G] model checking is PTIME-COMPLETE in model size and 2EXPTIME-COMPLETE in specification size.The overall bottom-up procedure requires time |StG|2^O(lng(ϕ)).

6. CONCLUSION

The paper presents SL as a powerful framework for strategic behavior in multi-agent concurrent games and identifies both its strongest fragment and unresolved extensions. SL[1G] strictly extends ATL* while retaining a 2EXPTIME-COMPLETE model-checking problem, whereas SL[BG] leaves elementary decidability open.

  • SL is introduced as a powerful formalism for reasoning about strategic behaviors in multi-agent concurrent games.
  • SL[1G] restricts formulas to one temporal goal at a time and strictly extends ATL* while preserving its positive properties.
  • 2EXPTIME-COMPLETE model checking makes SL[1G] no harder than ATL*.
  • SL[BG] expresses properties such as Nash equilibrium, but its elementary model-checking status remains unresolved.
  • SL provides a potential unifying basis for studying logics about strategic behavior and their relationships in multi-agent scenarios.

A. MATHEMATICAL NOTATION

This appendix establishes notation for words, trees, classical set constructions, relations, and functions used throughout the work.

  • Classic objects: It introduces natural-number intervals, cardinality, and powersets as standard set-theoretic constructions.The notation includes finite and half-open intervals, the numerable infinity ω, and 2X for the powerset of X.
  • Relations: Relations are described through domains, codomains, ranges, inverses, composition, iteration, transitive closure, reflexive-transitive closure, and quotient sets.For an equivalence relation R, X/R denotes the set of its equivalence classes.
  • Functions: Functions are represented as relations assigning exactly one codomain element to each element of their domain, with notation for total, partial, restricted, and empty functions.Restriction f↾Z is defined on X ∩ Z and preserves f's values where the restriction is defined.
  • Words: The appendix defines finite and infinite words, prefixes, suffixes, first and last letters, and maximal common prefixes.Finite words are formed over an alphabet X, with X+ excluding the empty word ε.
  • Trees: A Δ-tree is prefix-closed; completeness respects a fixed strict total order on directions, while fullness means T = Δ∗.Nodes are elements of T, with the empty word ε as root and t·d as a successor of t.

B. PROOFS OF SECTION ??

The appendix proves properties of dependence maps used to analyze strategy quantifications, including common valuations, dualization, incidence, and adjointness.

  • Role in the paper: The appendix concludes by identifying these dependence-map lemmas as prerequisites for proofs concerning adjoint maps, dependence–valuation duality, and encasement characterization.These results connect the appendix's technical arguments to the main development.
  • Dependence-map properties: The appendix explains that arbitrary dual dependence maps can share common valuations, illustrated through explicit valuation examples.The examples identify valuations lying in the ranges of selected dependence maps.
  • Dependence incidence: Lemma B.1 establishes that two dependence maps share a valuation fixed by each map on the variables quantified by the prefix.The proof assumes an existentially starting prefix without loss of generality and handles the dual prefix otherwise.
  • Proof strategy: The proofs proceed by induction on quantification-prefix length or alternation number, with separate cases based on the prefix structure.Base cases use empty dependence maps or define valuations directly, while inductive cases split prefixes and construct extensions.
  • Dependence dualization: Lemma B.2 states that if every dependence map for a prefix reaches a valuation in P, then a dual dependence map also reaches a valuation in P.The proof constructs projections of P and applies induction to prefix extensions.
  • Adjoint dependence maps: Lemma B.3 characterizes adjoint dependence maps pointwise: a map is a dependence map exactly when each component of its adjoint is one.The proof verifies the two defining dependence-map conditions in both directions.
Loading 1112.6275v2…