wiki

ATL Model Building

2 min read

ATL Model Building

Context

Galimullin2025 - Changing the Rules of the Game introduces LAMB, a logic for reasoning about explicit modifications of concurrent game models while retaining ATL-style strategic modalities.

Formal Statement

A named concurrent game model is

where S is finite, tau:S x Act^Agt -> S maps complete action profiles to successor states, and L labels states with atomic propositions and nominals.

Hybrid ATL extends ATL with named states and formulas @_alpha phi.

LAMB adds update modalities [pi]phi with primitive updates:

  • p_alpha := psi: set proposition p at the state named alpha according to whether psi holds;
  • alpha -A-> beta: redirect the transition for action profile A from the state named alpha to the state named beta;
  • new(alpha): add a fresh self-looping state named alpha.

Bounded modification synthesis asks whether there is an update sequence pi of size at most n such that

Main complexity/expressivity results:

  • HATL is strictly more expressive than ATL;
  • substitution-only LAMB is expressively equivalent to HATL, though often more succinct;
  • arrow updates make the logic strictly more expressive;
  • LAMB model checking is P-complete;
  • bounded modification synthesis is NP-complete.

Derivation / Construction

  • Nominals let formulas target named states even after updates.
  • Arrow updates directly change strategic reachability by modifying transition outcomes for action profiles.
  • State-creation plus substitution and arrow updates can encode sanctioning norms and other institutional changes.
  • Model checking recursively evaluates ATL/HATL formulas and constructs updated models for update modalities.

Implications

  • LAMB provides a compact language for asking whether a multi-agent system can be repaired or redesigned by small explicit model changes.
  • Normative and mechanism-design updates can be represented as update sequences rather than external meta-operations.
  • The P-complete model-checking result makes the framework comparatively tractable among strategic logics.

Graph View

Backlinks