Obstruction Alternating-time Temporal Logic: A Strategic Logic to Reason about Dynamic Models

Multi-Agent Systems (MAS) operating within dynamic models have been extensively studied in various domains, including cybersecurity and planning. In this paper, we introduce a dedicated logic for analyzing a specific category of MAS that involve strategic objectives within dynamic models. Within these MAS, there exists an agent known as the "Demon", which possesses the capability to modify the MAS model itself, while other agents operate as traditional MAS entities. We demonstrate that the model-checking problem for our logic is solvable in polynomial time. Furthermore, we showcase how this logic can be effectively employed to articulate significant properties within the realm of cybersecurity.