Big, but not unruly: Tractable norms for anonymous game structures

TL;DR

This paper introduces a new logical framework, NCHATL, for efficiently verifying norm compliance in anonymous concurrent game structures, enabling polynomial-time model checking even with complex normative systems.

Contribution

It presents a compact representation for anonymous game structures and proves that model checking normative formulas remains tractable under these conditions.

Findings

Model checking is polynomial-time for anonymous game structures.

Compact representation avoids exponential model sizes.

Normative systems with agent-specific norms are efficiently verifiable.

Abstract

We present a new strategic logic NCHATL that allows for reasoning about norm compliance on concurrent game structures that satisfy anonymity. We represent such game structures compactly, avoiding models that have exponential size in the number of agents. Then we show that model checking can be done in polynomial time with respect to this compact representation, even for normative systems that are not anonymous. That is, as long as the underlying game structures are anonymous, model checking normative formulas is tractable even if norms can prescribe different sets of forbidden actions to different agents.