Obstruction Logic: A Strategic Temporal Logic to Reason About Dynamic Game Models

Games that are played in a dynamic model have been studied in several contexts, such as cybersecurity and planning. In this paper, we introduce a logic for reasoning about a particular class of games with temporal goals played in a dynamic model. In such games, the actions of a player can modify the game model itself. We show that the model-checking problem for our logic is decidable in polynomial-time. Then, using this logic, we show how to express interesting properties of cybersecurity games defined on attack graphs.