Proceedings

Coalition Obstruction Temporal Logic: A New Obstruction Logic to Reason About Demon Coalitions

Davide Catta, Jean Leneutre, Vadim Malvone, James Ortiz

Download BibTeX Cite

Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence. Main Track. Pages 21-28.

https://doi.org/10.24963/ijcai.2025/3

Keywords

  • Agent-based and Multi-agent Systems: MAS: Agent theories and models
  • Agent-based and Multi-agent Systems: MAS: Formal verification, validation and synthesis
  • Agent-based and Multi-agent Systems: MAS: Applications
  • Agent-based and Multi-agent Systems: MAS: Coordination and cooperation

Abstract

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.

Davide Catta, Jean Leneutre, Vadim Malvone, and James Ortiz. 2025. Coalition Obstruction Temporal Logic: A New Obstruction Logic to Reason About Demon Coalitions. In Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence, IJCAI-25. IJCAI, 21–28. https://doi.org/10.24963/ijcai.2025/3
Welcome Future Conferences AI Journal Division IJCAI Proceedings About IJCAI IJCAI Awards