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

1 Introduction

Multi-Agent Systems (MAS) have become a crucial paradigm for modeling and analyzing complex systems, especially in critical domains such as cybersecurity [Lomuscio et al., 2009]. These systems involve multiple autonomous agents interacting with each other, often in dynamic and adversarial environments. In this context, game theory has proven to be a powerful tool for modeling strategic interactions between attackers and defenders, providing a formal framework to understand how coalitions of agents can achieve specific goals through cooperative actions. Temporal logics, such as Alternating-time Temporal Logic (ATL) [Alur et al., 2002], have been developed to reason about the strategic capabilities of coalitions of agents in these scenarios. ATL allows for the expression of properties like "a coalition of agents can ensure that a certain condition will eventually be met", which is crucial for the verification of systems where outcomes depend on the cooperative decisions of multiple agents. However, ATL and other traditional strategic logics, such as Strategy Logic (SL) [Mogavero et al., 2014], assume that the game model in which the players participate is static.

This means that while the actions of the players may affect their position within the game model, they do not alter the underlying structure of the game model itself. This assumption of a static game model limits the applicability of these logics in real-world scenarios where the environment can change dynamically in response to players' actions. For instance, in cybersecurity, defenders may deploy countermeasures that temporarily disable certain attack actions, effectively altering the game's landscape. Such dynamic interactions cannot be adequately captured by ATL or traditional logics, as CTL, LTL [Baier and Katoen, 2008]. To address this limitation, we propose Coalition Obstruction Temporal Logic (COTL), an extension of Obstruction Logic (OL) [Catta et al., 2023] that incorporates dynamic game models where defenders, or demons, obstruct attackers by deactivating edges in the game structure. In COTL, a coalition of defenders strategically obstructs paths available to attackers by disabling certain transitions. This logic is well-suited for security games, where defenders must cooperate to block attackers' objectives. Unlike traditional logics such as CTL, ATL, or SL, COTL expresses complex temporal properties that depend on both action sequences and strategic manipulation of the game structure by defenders. This makes COTL particularly relevant in cybersecurity, where dynamic games model interactions between attackers and defenders. Traditional approaches assume a static attack surface, but defenders must adapt their strategies in real-time to respond to emerging threats. By incorporating these dynamic elements, COTL provides a more accurate tool for verifying defense strategies in complex environments. Moreover, the logics we mentioned earlier assume that the set of paths relevant for evaluating a formula in a model is infinite. While this assumption is convenient from a computational perspective, it is unrealistic from a modeling standpoint. In cyber-attack models, like Attack Graphs (AG) [Kaynar, 2016], attack path are typically finite. Consequently, our logic does not assume paths are necessarily infinite, allowing for both finite and infinite paths. This approach brings the semantics of our logic closer to formalisms like ATLf [Belardinelli et al., 2018]. In addition to COTL, several other logics have been proposed to extend the capabilities of ATL in various directions. Timed Alternatingtime Temporal Logic (TATL) [Henzinger and Prabhu, 2006; Laroussinie et al., 2006] and Probabilistic Alternating-time Temporal Logic (PATL), extend ATL by introducing timing constraints and probabilistic outcomes. However, they assume static game models, making them less suitable for scenarios with dynamically changing environments like those addressed by COTL.

Our work builds on these advancements by integrating the concepts of dynamic games and obstruction into the ATL framework, resulting in a logic that is better equipped to handle the complexities of real-world systems, particularly in cybersecurity. This paper presents the formal semantics of COTL, defines the key concepts such as strategies, curses, and demonic obstruction, and illustrates the application of this logic through a series of examples. We also provide a model-checking algorithm for COTL, enabling the verification of security properties in dynamic game models.

Structure of the work. Theoretical background and syntax and the semantics of our new logic are in Section 2. In Section 3 we provide some important properties of our logic. In Section 4, we show our model checking algorithm and prove that for COTL is PTIME-Complete. In Section 5, we present our case study in the cybersecurity context. In Section 6, we analyze our logic in the imperfect information setting. In Section 7, we compare our approach to related work. Finally, Section 8 concludes and presents possible future directions.

2 Model and Logic

In this section, we will first discuss the basic notions used in this paper and then we will define the syntax and semantics of COTL. Let N be the set of natural numbers, we refer to the set of natural numbers containing 0 as N≥0 and Z the set of integers. Let X and Y be two sets and |X| denotes its cardinality. The set operations of intersection, union, complementation, set difference, and Cartesian product are denoted X ∩ Y , X ∪ Y , X, X \ Y , and X × Y , respectively. Inclusion and strict inclusion are denoted X ⊆ Y and X ⊂ Y , respectively. The empty set is denoted ∅. Let π = π1, . . . , πn be a countable sequence and i ≤ |π| , we denote by πi its i-th element, by π≤i the finite prefix π1, . . . , πi of π and by π≥i the (possibly infinite) suffix of π starting at πi. If π is a finite sequence, last(π) denotes the last element πn of π.

Now, we define the syntax and semantics of COTL. We begin by introducing, the model used to define the semantics of COTL formulas. A model consists of a directed graph, a set of actions, and a cost function that assigns a cost to each action at every state. These actions are carried out by a group of players called Demons. At each state, every action has a specific cost, and a combination of actions (one per Demon) can temporarily disable a set of adjacent edges to that state. The formal definition follows

Definition 1. Let Ap be an at most countable set of atomic formulas (or atoms) and D = {1, . . . , k} be a finite (non-empty) set of demons (whose subsets will be called legions). A model over Ap and D is a tuple M = ⟨S, s0,A, P,R, , $,L⟩ where:

• S is a non-empty, countable set of states,
• s0 is a distinguished state dubbed initial state,
• A is a finite, non-empty set of actions. A tuple of actions whose length is |D| will be called a curse, we denote the set of curses by C,
• P : D × S → 2A \ ∅ is the protocol function that assigns a non-empty set of actions to any demon and any state. We suppose that the idle action ⋆ is assigned by the protocol function to any demon at any state.
• R ⊆ S × S is a binary relation over S.
• : S × C → 2R is a function associating to any state s and any curse c such that c[i] ∈ P(i, s), a subset of the set of edges that are incident to s.
• $: S × D × A → N≥1 is a cost function associating a positive natural number to any triple composed of a state, a demon, and an action that is available to that demon at that state. We suppose that $(s, i, ⋆) = 0 for any state s and Demon i.
• L : S → 2Ap is the labeling function associating to any state a subset of Ap.

We use the adjective countable in its standard mathematical sense, i.e., it denotes an object that is either finite or that has the cardinality of N.

Given a model M, a path π over M is any nonempty countable sequence of states π = π1, π2, · · · such that ⟨πi, πi+1⟩ ∈ R for every i < |π|. We denote paths by the letters π, τ, ρ. A history h is any finite prefix of a path. We use H to denote the set of all histories over a model. Let Mbe a model, s is one of its states and G a legion, an action available for G at s is a function f : G → A such that f(i) ∈ P(i, s) for each i ∈ G. If f is any of these actions available at s for the legion G. We can say that a curse c extends f iff c[i] = f(i) for each i ∈ G. Let V(G, s) be the set of actions available at s and V(G,M) = ⋃s∈S V(G, s). Here, we will consider a coalition of demons acting rationally to modify the structure of the model, i.e., a legion can devise strategies to modify the model. Given a history h, a demonic strategy selects a subset of arcs that are adjacent to last(h). The arcs selected by demonic strategies are temporarily deleted from the set of arcs of the model. In this sense, the actions of the legion modify the structure of the graph. Given a threshold n, a strategy is said to be compatible with this threshold if the cost of any collective action selected by the strategy does not encompass n. We formally define the notion of demonic strategy as follows.

Definition 2. Let M be a model, n ∈ N be a natural number, and G be a legion. If f is an action available to G at some state s, we write Cost(s, G, f) for ∑i∈G $(s, i, f(i)). A n-strategy SnG for G (or G n -strategy) is a function SnG : H → V(G,M) that maps any history h to an action f available at last(h) and such that for any h and any h′ ⪯ h Cost(last(h′ ), G, S(h′ )) ≤ n. Let π be a path and SnG a G n - strategy, π is compatible with SnG iff for each i < |π|, there is a curse c extending SnG (π≤i) such that ⟨πi, πi+1⟩ /∈ (πi, c). Given a state s and a strategy SnG , we let Out(s, SnG ) denote the set of maximal paths compatible with SnG that starts at s, that is paths compatible with SnG that are not proper prefixes of any other path that is compatible with SnG starting at s.

Remark that Out(s,SnG ) can contain both finite and infinite path but it cannot be empty, since it always contains the trivial path s. Now, we present the syntax of our logic.

Definition 3. Let Ap be an at most countable set of atomic propositions (or atoms) and a finite (non-empty) set of demons D. Formulas of COTL are defined by the following grammar:

where p is an atomic formula, G is a legion (a subset of D), and n (the grade) is any number in N.

The boolean connectives ⊥, ∨ and → can be defined as usual and the temporal operators X (next), U (until), and R (release) together with their weak version ˜X. We can also define ⟨⟨G⟩⟩nFφ := ⟨⟨G⟩⟩n (⊤Uφ), ⟨⟨G⟩⟩nGφ := ⟨⟨G⟩⟩n (⊥Rφ), ⟨⟨G⟩⟩n (φWψ) := ⟨⟨G⟩⟩n (ψR(φ ∨ ψ)) and [[G]]nXφ := ¬⟨⟨G⟩⟩n ˜X¬φ. We have included the ˜X operator because the next operator X on finite traces is not self-dual, in contrast to the infinite trace situation. The size |φ| of a formula φ is the number of its connectives. The formula ⟨⟨G⟩⟩nφ with φ temporal formula is "there is a n-strategy SnG such that all paths of the graphs that are compatible with the strategy satisfy φ" where "n-strategy" means "a strategy for disabling arcs". Formulas of COTL will be interpreted over obstruction models.

Definition 4. The satisfaction relation between a model M, a state s of M, and a formula φ is defined by induction on the structure of φ:

• M, s |= ⊤ for all state s,
• M, s |= p iff p ∈ L(s),
• M, s |= ¬φ iff not M, s |= φ (notation M, s ̸|= φ),
• M, s |= ⟨⟨G⟩⟩nXφ iff there is a n-strategy SnG for the legion G such that for all π ∈ Out(s, SnG ) with |π| ≥ 2, and we have that M, π2 |= φ,
• M, s |= ⟨⟨G⟩⟩n ˜Xφ iff there is a n-strategy SnG for the legion G such that for all π ∈ Out(s, SnG ) with |π| < 2, or we have that M, π2 ̸|= φ,
• M, s |= ⟨⟨G⟩⟩n (φUψ) iff there is a n-strategy SnG such that for all π ∈ Out(s,SnG ) there is a j ≤ |π| such that M, πj |= ψ and for all 1 ≤ k < j, M, πk |= φ,
• M, s |= ⟨⟨G⟩⟩n (φRψ) iff there is a n-strategy SnG such that for all π ∈ Out(s,SnG ) we have that either M, πi |= ψ for all i ≤ |π| or there is a k ≤ |π| such that M, πk |= φ and M, πi |= ψ for all 1 ≤ i ≤ k.

Two formulas φ and ψ are semantically equivalent (denoted by φ ≡ ψ) iff for any model M and state s of M, M, s |= φ iff M, s |= ψ.

3 COTL Properties

In this section, we study the formal properties of our logic. Here, we show that, as in ATL, the set of states that satisfies a formula of the form ⟨⟨G⟩⟩n (φ1 Uφ2) or ⟨⟨G⟩⟩n (φ1 Rφ2)

can be expressed as the fix-point of particular monotone functions. Given a formula φ and a model M, we let SatM(φ) denote the set of states ofMsatisfying φ, that is SatM(φ) = {s ∈ S | M, s |= φ}. We drop the superscript Mwhenever the model is contextually given. Given a curse c and a state s, we denote by post(c, s) the states that are incident to s after the execution of c that is:

Given a natural number n, a legion G, and a set of states X, we denote by ▼(n,X, G) the set of states Y ⊆ S such that for every y ∈ Y there is an available G-action f with Cost(G, y, f) ≤ n and such that, for any curse c extending f, the set post(c, s) is non-empty and included in X. We now prove that the set ▼(n, Sat(φ), G) characterize the set of states satisfying a formula of the form ⟨⟨G⟩⟩nXφ.

Proposition 1. Let M be a model, n a natural number and φ a formula. For every state s of Mwe have that M, s |= ⟨⟨G⟩⟩nXφ if and only if s ∈ ▼(n, Sat(φ), G)

Proof. Suppose thatM, s |= ⟨⟨G⟩⟩nXφ this means that there is a n-demonic strategy SnG such that for each path π ∈ Out(s,SnG ) we have both |π| ≥ 2 and π2 ∈ Sat(φ). Let f be the action that the strategy chooses on s, let c be any curse extending f, since |π| ≥ 2 for any π ∈ Out(s,SnG ) we cannot have that post(c, s) = ∅. Moreover, from the fact that π2 ∈ Sat(φ) for every π ∈ Out(s,SnG ) we conclude that post(c, s) ⊆ Sat(φ). For converse direction, let f be an action such that for each curse c that extends f, we both have post(c, f) ̸= ∅ and post(c, f) ⊆ Sat(φ). Define a strategy SnG for the legion G which outputs f on s and the action available for G is composed of idle actions on any other history. Consider a path π ∈ Out(s,SnG ). It is impossible that |π| < 2, this would mean that there is a curse c extending f, for which post(c, s) = ∅. Simarly it is impossible that π2 /∈ Sat(φ) because otherwise we will obtain that there is y ∈ post(c, s) such that y /∈ Sat(φ) for some c extending f. We thus conclude that if s ∈ ▼(n, Sat(φ), G) then M, s |= ⟨⟨G⟩⟩nXφ

Proposition 2. For any pair of formulas φ and ψ the following are true:

Proof. We only prove (1), the proof of (2) being entirely similar. For the (⇒) direction. Let Mbe any model and s any of its states, and suppose that s ∈ Sat(⟨⟨G⟩⟩n (φUψ)). By the definition of satisfaction, this means that there is a demonic n-strategy SnG such that for all π ∈ Out(s, SnG ) then there is a j ≤ |π| such that πj ∈ Sat(ψ) and πi ∈ Sat(φ) for each 1 ≤ i < j. If j = 1, then we can conclude, otherwise s ∈ Sat(φ) and we must show that s ∈ Sat(⟨⟨G⟩⟩nX ⟨⟨G⟩⟩n (φUψ))). Let π be a path that satisfies (φ U ψ) given the demonic n-strategy SnG . It is clear that π≥2 ∈ Out(π2,SnG ) and, since π1 /∈ Sat(ψ), that M, π≥2 |= φUψ. Moreover, π ∈ Out(s,SnG ) then we can conclude that M, s |= ⟨⟨G⟩⟩nX⟨⟨G⟩⟩n (φUψ). For the converse (⇐) direction. Suppose that s ∈ Sat(ψ ∨

(φ ∧ ⟨⟨G⟩⟩nX⟨⟨G⟩⟩n (φUψ))). If s ∈ Sat(ψ) then we are done. Otherwise s ∈ Sat(φ). From the fact that s satisfies ⟨⟨G⟩⟩nX ⟨⟨G⟩⟩n (φ U ψ), we obtain that there is a n-strategy S1G such that M, π2 |= ⟨⟨G⟩⟩n (φUψ) for every π ∈ Out(s, S1G ). By applying again the definition of satisfaction, we obtain that there is a demonic n-strategy S2G such that M, ρ |= (φUψ) for every ρ ∈ Out(π2, S2G ). Consider the n-demonic S⋆G defined by:

That is, S⋆G is obtained by composing S1G with S2G . By construction, for every π ∈ Out(s,S⋆G ) we have that M, π |= φUψ and we can thus conclude.

Let M be a model and φ, ψ be two formulas. Consider the two functions U n G,φ,ψ and R n G,φ,ψ from 2S to itself defined by:

we can prove the following.

Theorem 1. For every model M and pair of formulas φ and ψ:

Proof. We only prove (2). In virtue of the proposition 2, it is clear that ⟨⟨G⟩⟩n (φRψ) is a fix-point of the function in Equation 2. To prove that X = ⟨⟨G⟩⟩n (φRψ) is the greatest fix-point of the function, we consider another fix-point Y and show that Y ⊆ X.

If Y = ∅ there is nothing to do. Otherwise, let y ∈ Y : we have that y ∈ Sat(ψ) and either y ∈ Sat(φ) or y ∈ ▼(n, Y, G). If this last case holds, we have that there is an action f for G s.t. Cost(y, G, f) ≤ n . We define a strategy SnG :

where f ∈ V(G, last(h)) and post(c, last(h)) ⊆ Y for any curse c extending f. Remark that such an f exists if last(h) ∈ ▼(n, Y, G) and since there are finitely many actions, we can always pick one. It is easy to see that any path in the above-defined strategy verifies φRψ.

4 Model Checking

Here, we present our model checking algorithm for COTL. We show also that the model checking problem for COTL is decidable in PTIME-Complete. To show this result, we provide Algorithm 1 that given a model M and a formula φ returns the set of states ofMsatisfying φ, but the pre-image operator used for ATL[Alur et al., 2002] and OL[Catta et al., 2023] model checking is replaced by a coalition post operator on M.

Definition 5. Given a finite model M, a state s, and a COTL state formula φ, the model checking problem consists in determining whether M, s |= φ.

The model checking algorithm is based on the computation of the set Sat(φ) of all states satisfying a COTL formula φ. The most interesting part of our algorithm is the treatment of the formulas ψ = ⟨⟨G⟩⟩nXφ, ψ = ⟨⟨G⟩⟩n (φUψ), ψ = ⟨⟨G⟩⟩n (φRψ). Let us now prove the termination and correctness of the Algorithm 1.

Algorithm 1 COTL model checking Input: A model M and φ is a COTL formula Output: Sat(φ) ← {s ∈ S | M, s |= φ}

1: for all ψ ∈ Sub(φ) do 2: switch (ψ) do 3: case ψ = ⊤ 4: Sat(ψ) ← S 5: case ψ = p 6: Sat(ψ) ← {s ∈ S | p ∈ L(s)} 7: case ψ = ¬ψ1 8: Sat(ψ) ← S \ Sat(ψ) 9: case ψ = ψ1 ∧ ψ2 10: Sat(ψ) ← Sat(ψ1) ∩ Sat(ψ2) 11: case ψ = ⟨⟨G⟩⟩n X ψ1 12: Sat(ψ) ← ▼(n, sat(ψ1), G) 13: case ψ = ⟨⟨G⟩⟩n ˜X ψ1 14: Sat(ψ) ← ▼(n, sat(ψ1), G) 15: case ⟨⟨G⟩⟩n (φUψ) 16: X ← ∅; Y ← sat(ψ2) 17: while Y ̸=X do 18: X ← Y 19: Y ← sat(ψ2) ∪ (sat(ψ1) ∩ ▼(n, X, G)) 20: Sat(ψ) ← Y 21: case ψ = ⟨⟨G⟩⟩n (φ R ψ) 22: X ← ⊤ Y ← sat(ψ2) 23: while X ̸= Y do 24: X ← Y 25: Y ← sat(ψ2) ∩ (sat(ψ1) ∪ ▼(n, X, G)) 26: Sat(ψ) ← Y

Theorem 2. Let M be a model and φ be a COTL formula. Then, (i) Sat(φ) terminates and (ii) s ∈ Sat(φ) iff M, s |= φ.

We now, explore the computational complexity of model checking COTL.

4.1 Lower Bounds

We now provide the lower bounds for model checking COTL. In fact, the problem can be reduced from CTL model checking problem, which is known to be PTIME-hard [Clarke et al., 1983]. This establishes the PTIME-hardness of COTL.

We will reduce from CTL model-checking problem to the COTL model-checking problem by encoding CTL semantics within COTL, ensuring that every CTL formula can be checked by a corresponding COTL formula with equivalent semantics. A CTL formula φ can be translated to a COTL formula (φ)· and a model M′ in CTL can be translated to a model M in COTL add all transitions that are selected by the strategy, the cost function and for which the following holds:

Proposition 3. Given a model M, then for all s ∈ S and formula φ, we have that M′ , s |=CTL φ iff M, s |= (φ)· .

First, let us reduce the 0 part of COTL to be the set of COTL formulas in which the grade of each strategic formula is 0. Let (-)· be the function from CTL formulas to COTL formulas, which is the identity on atomic propositions and ⊤, which commutes with the boolean connective and such that:

We can easily show the following by remarking that Out(s,SnG ) contains all paths starting at s when SnG is a 0strategy.

4.2 Upper Bounds

To establish the upper bound, we can devise a polynomialtime algorithm for this problem. The algorithm 1 is derived from the CTL model checking algorithm presented in [Clarke et al., 1983], with a modification to the Post function. Specifically, for a set of D of demons and a set S of states and s ∈ S, post(c, s) computes the set of states reachable from s after executing c. Now, we can prove that our algorithm is polynomial in time complexity.

The complexity depends on the model size |M|, traditionally defined by the cardinality of the transition relation R of M, the formula size |φ|, representing the number of subformulas and temporal operators, and the size of the action set |A|, crucial for computing action profiles f : G → A. Additionally, the number of curses in the model, representing constraints or obstructions, impacts Post evaluation. The following theorem establishes the complexity of our model checking algorithms.

Theorem 3. Let M be a model, φ be a COTL formula and A be a set of actions. The model checking problem of COTL on M is PTIME-complete and can be solved in time O(|M| × |φ| × |A|) the problem is PTIME-hard even for a fixed formula.

5 Case Study

The Attack Graph (AG) [Kaynar, 2016] is a widely recognized and increasingly popular attack model. By leveraging an AG, it is possible to model interactions between an attacker and a defender who dynamically deploys Moving Target Defense (MTD) mechanisms [Cho et al., 2020]. MTD mechanisms, such as Address Space Layout Randomization (ASLR) [Marco-Gisbert and Ripoll Ripoll, 2019], are active defenses that use partial system reconfiguration to alter the attack surface and reduce the chances of success of the attack. However, activating an MTD countermeasure impacts system performance: during reconfiguration, system services may be partially or completely unavailable. Thus, it is crucial to select MTD deployment strategies that minimize both residual cybersecurity risks and the negative impact on system performance. In the following case study, we are going to use the AG. Below, we will model a scenario where multiple defenders cooperate to prevent an attacker from compromising critical system states. The defenders can selectively block certain actions or transitions. Their collective goal is to prevent the attacker from reaching a particular "bad" state. In this scenario (see Figure 1), we consider multiple interconnected infrastructures, each overseen by a distinct security team:

• Infrastructure 1 (I1): The general ICT infrastructure of company C1, managed by security team (ST1).
• Infrastructure 2 (I2): An industrial control system (ICS) infrastructure from company C1, managed by security team (ST2). To facilitate the management of the ICS, a secure connection between I1 and I2 is established, utilizing dedicated credentials (cryptographic keys).
• Infrastructure 3 (I3): The general ICT infrastructure of company C2. For maintenance, C2 engineers have secure access to I2 via a dedicated connection between I2 and I3 using dedicated credentials (cryptographic keys).

Now, consider an attacker X whose goal is to compromise a target (e.g., a server) within I3. To achieve this, X can execute various attack strategies by exploiting the interdependencies between the infrastructures, as represented in the attack graph in Figure 2. It is important to note that each security team (ST1, ST2, ST3) can only deactivate the edge of its infrastructure at any time, and the other teams are idle. Initially, starting in state s0, the attacker can launch an attack (a10 or a20 ) to gain access to infrastructure I1 (reaching state s1) or I3 (reaching state s3). After gaining access, the attacker can carry out several attacks (a1 or a2) to acquire credentials to access I2, transitioning to states s12 or s22 . For simplicity, attacks a1 and a2 actually represent a tuple of attacks. Each attack in the tuple can be associated with a coalition agent. Once connected to I2, X can launch additional attacks (a12 , b12 , a22 , b22 ) to compromise the target and reach state s32 . There are real-world examples of such attack scenarios that exploit vulnerabilities in interconnected infrastructures, as demonstrated in [Case, 2016]. From the point of view of defenders, we assume that each security team can detect attacks within its domain (using intrusion detection techniques) and can counter them when possible (using attack response mechanisms). In our model, this means temporarily deactivating an edge in the attack graph. For instance, security team ST1 can counter attack a1 by disabling the edge from s1 to s12 , provided the cost of countering this edge is within the budget allocated to ST1. Some attacks, however, may be non-counterable. In Figure 2, the edges corresponding to attacks a10 , a20 , b12 , and b22 are shown with double lines, indicating that these attacks cannot be deactivated because their associated costs exceed the security team's budget. Here, COTL proves useful for the analysis of cooperation strategies between security teams. Let's define a proposition q, which is true when X successfully reaches state s32 (i.e., compromises the target). We can express coaltion strategies using formulas like: ϕ1 = ⟨⟨ST1, ST2⟩⟩n (G¬q). This formula states that the coalition of security teams ST1 and ST2 can cooperate to prevent X from reaching state s32 . In this example, φ is not satisfied because X can still reach s32 using the sequence of attacks a20 , a2, b22 . However, if we add ST3 to the coalition of defenders, the formula ϕ1 becomes true. This demonstrates that cooperation among ST1, ST2, and ST3 can successfully prevent the attack. In addition, the formula: ϕ3 = ⟨⟨ST1, ST3⟩⟩n (G¬q) is also true, showing that ST1 and ST3 alone can block the attack. In all cases, collaboration and coordination between companies C1 and C2 and their security teams are essential to counter the attack.

6 Imperfect Information

We introduce a semantic variant of our logic, COTL, to handle imperfect information scenarios where defenders form a coalition to obstruct an attacker. In this framework, the coalition may have limited knowledge about the system's current state or the attacker's actions. This models real-world systems where defenders must collaborate and make decisions based on incomplete information, such as in cybersecurity or distributed systems. Here, incomplete information is represented by grouping the game states into equivalence classes: one for the agent and another for the coalition of defenders (or demons), where states within the same equivalence class are indistinguishable from their perspective.

Definition 6. Given a set of atomic propositions Ap and a finite legion G (a subset of demons D), an Imperfectinformation Model (iModel) over Ap and G is a tuple ⟨S, s0,A, P,R, , $,L, {∼g}g∈G⟩, where:

• M= ⟨S, s0,A, P,R, , $,L⟩ is aModel over Ap and G,
• For each g ∈ G, ∼g⊆ S × S is a demon's equivalence relation over S.

We will represent an iModel as a tuple iM = ⟨M, {∼g }g∈G ⟩.

6.1 Memoryless Uniform Strategies

We consider the problem of verifying the existence of uniform strategies in the presence of imperfect information. A strategy is uniform if, after indistinguishable histories, demon select the same strategy. Two states s and s′ are indistinguishable by demon g, denoted by s ∼g s′ means that the demon g cannon distinguish between s and s′ implying that from g′ s perspective, the two states are observationally equivalent. Two histories, h and h′ , and specific demon g ∈ G, we will say that h ≡g h′ if and only h and h′ have the same length n, and hj ∼g h′j (i.e., sj ∼g s′j ) for every j ≤ n. We now proceed to define uniform strategies for the coalition of demons.

Definition 7. Given an iModel iMand a coalition G, a demonic G n -strategy is an uniform demonic G n -strategy SnG such that, for every pair of histories h and h′ , if h ≡g h′ then (SnG (h))(i) = (SnG (h′ ))(i).

A demonic SnG strategy is termed memoryless if, for any two histories h and h′ , the condition last(h)=last(h′ ) implies that SnG (h) = SnG (h′ ). Now, let us introduce several variations of the satisfaction relation initially defined in Definition 4.

Definition 8. Let iM be an iModel, s be any state of iM, and φ be any formula, we write:

• iM, s |=iR φ for the satisfaction relation obtained by replacing, in Definition 4, every occurrence of "demonic SnG -strategy" with "uniform demonic SnG -strategy",
• iM, s |=ir φ for the satisfaction relation obtained by replacing, in Definition 4, every occurrence of "demonic SnG -strategy" with "uniform memoryless demonic SnG - strategy",

First, we provide a result for the worst case.

Theorem 4. The model-checking problem for COTL under the satisfaction relation |=iR is undecidable.

The bottom-up approach is a distinctive methodology used in strategic (and temporal) logics that simplifies the satisfiability checking of a formula containing multiple strategic operators by reducing it to the satisfiability of a formula with only one strategic operator. The procedure is as follows: given a model iM and a formula ϕ with multiple strategic operators, let ϕ1, · · · , ϕn be the strategic subformulas of ϕ, each containing exactly one strategic operator. For each subformula ϕi, we introduce a fresh atomic proposition pi. We then update the valuation function L(s) by adding pi whenever s satisfies ϕi in iM, resulting in a newmodel iM′ . Next, we form a modified formula ϕ′ by substituting each instance of ϕi with the corresponding proposition pi. The satisfiability of ϕ′ is then evaluated on the new model M′ . This process is repeated iteratively, reducing the complexity step by step until the final result is obtained. This approach provides a systematic way of breaking down the formula, making it easier to handle complex strategic reasoning within a model.

Theorem 5. The model checking problem for COTL under the satisfaction relation |=ir is in P NP .

6.2 Distributed Uniform Strategies

Here, we consider the problem of verifying the existence of distributed uniform strategies in the presence of imperfect information. A strategy is distributed uniform if agents in a coalition select the same joint action in all states that are indistinguishable to any agent within the coalition. A distributed indistinguihability equivalence relation over a coalition G is represent as ∼DG = ⋂g∈G ∼g. Similarly, we will use the notation h ≡DG h′ if and only if h and h′ have the same length n, and hj ∼DG h′j for every j ≤ n. We can now proceed to define distributed uniform strategies for the demons.

Definition 9. Given an iModel iM and a coalition G, a demonic G n -strategy is a distributed uniform demonic G n - strategy SDG such that, for all state s and s′ , if s ∼DG s′ then SDG (s) = SDG (s′ ).

∼G represents the coalition's indistinguishability relation, meaning that the entire coalition must act uniformly in any two states that are indistinguishable to any demon in the coalition.

Definition 10. Let iMbe an iModel, s be any state of iM, and φ be any formula, we write:

• iM, s |=ir for the satisfaction relation obtained by replacing, in Definition 4, every occurrence of "demonic SDG -strategy" with "distributed uniform memoryless demonic SnG -strategy".

Theorem 6. The model checking problem for COTL under the satisfaction relation |=ir is in P NP .

7 RelatedWork

The study of strategic interactions within multi-agent systems has led to the development of various temporal logics designed to capture the capabilities of coalitions of agents. In this section, we review key logics related to our work on COTL, focusing on logics that address similar challenges or extend the foundational concepts of ATL [Alur et al., 2002] and OL [Catta et al., 2023]. ATL is one of the seminal logics for reasoning about the strategic abilities of coalitions in multi-agent systems. It allows for the expression of properties like a coalition of agents can ensure that a certain state is reached, which is crucial for verifying systems where multiple agents must coordinate to achieve desired outcomes. However, ATL assumes a static game model, where the environment does not change based on the actions of agents, limiting its applicability in dynamic scenarios such as cybersecurity. Building on ATL, Strategy Logic (SL) [Mogavero et al., 2014] enhances strategic reasoning by quantifying over strategies. SL allows for complex specifications, including nested strategies and binding to variables, offering a richer language for strategic properties. However, despite its expressiveness, SL also assumes a fixed game model, making it less suitable for dynamic environments. Temporal logics like CTL and ATL are typically designed for infinite traces, reasoning about systems over potentially infinite executions. Extensions such as LTL with finite traces (LTLf ) [De Giacomo et al., 2014], CTL, and CTL∗ adapted to finite paths soon followed. Additional versions like ATLf and bounded ATL [Belardinelli et al., 2018] were developed for reasoning about finite traces. Notably, COTL remains the only obstruction logic specifically proposed for handling finite traces. In the domain of dynamic games, Sabotage Modal Logic (SML), introduced by van Benthem, allows players to alter the game structure by deleting edges in a graph. SML focuses on obstructing opponents' moves but lacks temporal and probabilistic reasoning. Subset Sabotage Modal Logic (SSML) refines this by allowing temporary edge deactivation, though it still lacks temporal operators and cost considerations. OL provides a framework for reasoning about two-player games on static weighted graphs where one player (the demon) obstructs the other by deactivating edges. Obstruction Alternating-Time Temporal Logic (OATL) [Catta et al., 2024] provides a framework for reasoning about multi-agents player games played on weighted and directed graphs, where players (demons) can obstruct the other by deactivating edges [Catta et al., 2024]. abbrvCOTL integrates the concept of dynamic games with strategic and temporal reasoning to build on these foundations. Unlike previous logics, COTL better reflects the complexity of real-world scenarios such as cybersecurity, where defenders must adapt strategies in real time.

8 Conclusions

In this paper, we presented COTL, a logic that extends OL by allowing reasoning about games where players, called demons, can locally and temporarily modify the game structure. This enables the modeling of dynamic systems where defenses and countermeasures can be taken immediately, particularly in the context of cybersecurity. We have shown how COTL can be used to express and analyze cybersecurity properties, such as coalitions between different defenders to prevent attackers from achieving their goals. Our work delves into the formal properties of COTL and its model checking problem under different semantics. In particular, COTL provides a flexible framework for studying the interaction between defenders (e.g., security teams) in a multiagent setting, and how they can work together to obstruct the attacker's progress. As future work, we aim to thoroughly investigate the possibility of introducing probabilistic operators into COTL, with the goal of being able to reason about complex, real-world scenarios involving uncertainty, making it a powerful formalism for analysing probabilistic attackdefence strategies in cybersecurity and other domains. We also aim to investigate semantic variants of COTL where the Demon and players use bounded memory strategies [Jamroga et al., 2019], which are more feasible in real-world applications. These strategies can limit the complexity of the decisions and make the logic more tractable for practical use.