A Logic for Resource-Sensitive Coalition Games
摘要
Reasoning about strategic ability in multi-agent systems typically relies on strategic logics such as Coalition Logic and Alternating-time Temporal Logics, which model what groups of agents can achieve through coordinated action. However, these logics treat the system state as a monolithic whole, limiting support for modular verification. By contrast, resource logics such as Separation Logic, originally developed for sequential program verification, support compositional reasoning by partitioning state into disjoint regions, but they lack the means to express strategic interaction among agents. We present Separating Coalition Logic (SCL), a unified framework that combines strategic reasoning with resource-sensitive modularity. Built over ‘minimal’ interactive systems with local update rules and disjoint agent control, SCL supports both strategic guarantees and system decomposition along clean boundaries. A key feature is the Strategic Frame Rule, which lifts local properties into global guarantees even under adversarial conditions, enabling compositional proofs without reanalysis. We illustrate the framework via a case study in decentralized governance for Decentralized Autonomous Organizations, showing how SCL supports modular reasoning about both strategic interference and resource isolation.