Coalition Obstruction Temporal Logic: A New Obstruction Logic to Reason About Demon Coalitions
Coalition Obstruction Temporal Logic: A New Obstruction Logic to Reason About Demon Coalitions
Davide Catta, Jean Leneutre, Vadim Malvone, James Ortiz
Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence
Main Track. Pages 21-28.
https://doi.org/10.24963/ijcai.2025/3
In multi-agent systems, especially in cybersecurity, the dynamic interplay between attackers and defenders is crucial to the security and resilience of the system. Traditional methods often assume static game models and fail to account for the strategic adaptation of the environment to the actions of the players. This paper presents Coalition Obstruction Temporal Logic (COTL), a formal framework for analyzing defender coalitions in dynamic game scenarios. Within this framework, defenders, conceptualized as demons, can actively obstruct attackers by selectively disabling certain actions in response to perceived threats. We establish the formal semantics of COTL and propose a model checking algorithm to verify complex security properties in systems with evolving adversarial dynamics. The utility of the framework is demonstrated through its application to a coalition of defenders that collaboratively defend a system against coordinated attacks.
Keywords:
Agent-based and Multi-agent Systems: MAS: Formal verification, validation and synthesis
Agent-based and Multi-agent Systems: MAS: Agent theories and models
Agent-based and Multi-agent Systems: MAS: Applications
Agent-based and Multi-agent Systems: MAS: Coordination and cooperation
