This paper discusses Timed Obstruction Temporal Logic (TOTL) and Probabilistic Obstruction Temporal Logic (POTL), extensions of Obstruction Logic for systems with critical timing and probabilistic behavior. TOTL focuses on real-time system properties, while POTL handles uncertainty and stochastic events alongside temporal constraints. These logics are especially useful in cybersecurity, where both time and probability are crucial. We demonstrate their applicability through case studies in cybersecurity games based on attack graphs.
Demon and the Traveler, who interact on a directed graph with edges associated with deactivation
costs. The Demon attempts to obstruct the Traveler by deactivating certain edges within a budget,
while the Traveler navigates the graph. The game progresses in rounds, with the Demon winning if
the Traveler’s path satisfies a specific temporal property. OL is particularly useful in cybersecurity,
where it can model scenarios involving attackers and defenders, enabling the design of dynamic defense
strategies using concepts like Attack Graphs (AG) [
To address these challenges, we discuss two extensions of the obstruction logic: Timed Obstruction Temporal Logic (TOTL) and Probabilistic Obstruction Temporal Logic (POTL). TOTL builds on the foundation of temporal logic by incorporating constructs that allow precise modeling of time-dependent behavior. This makes TOTL particularly suitable for real-time systems where the timing of actions and events must be meticulously managed. POTL, on the other hand, adds probabilistic reasoning to the framework. This allows for the analysis of systems where outcomes are influenced by both deterministic and stochastic factors. By integrating probability with temporal logic, POTL allows for a more nuanced understanding of system behavior under uncertainty. This is essential in domains such as cybersecurity, where the likelihood of certain events must be carefully assessed.
Together, TOTL and POTL provide a unified framework for reasoning about systems that are both time-sensitive and probabilistically complex. This paper explores the syntax and semantics of these logics and illustrates their power and flexibility with practical examples. Through examples, we show how these logics can be applied to real-world scenarios, such as the formal verification of security protocols and the optimization of defense strategies in the face of sophisticated cyber threats. By leveraging the capabilities of TOTL and POTL, system designers and security analysts can better manage the trade-ofs between time, probability, and system performance, ultimately leading to more secure and reliable digital infrastructures.
Structure of the work. In Section 2, we present the syntax and the semantics of our logics, called Timed Obstruction Logic (TOL) and Probabilistic Obstruction Temporal Logic (POTL). In Section 3, we present our case study in the cybersecurity context. In Section 4, we compare our approach to related work. Finally, Section 5 concludes and presents possible future directions.
In this section, we define the syntax and semantics of our Probabilistic Obstruction Temporal Logic (POTL) and Timed Obstruction Temporal Logic (TOTL).
Here, we introduce the Probabilistic Obstruction Temporal Structure (POTS), the type of model that we use to verify POTL properties. Let us start with some probabilistic concepts. A probability distribution over a finite set assigns probabilities to each element such that the total sum is 1. A probability space, which consists of a sample space, is a set of possible events (a -algebra), and a probability measure assigns probabilities to these events.
Definition 1 ( Markov Chain). A Markov Chain (MC) is a pair ℋ = (, P) where is a (countable)
set of states and P: × → [
Definition 2 (Probabilistic Kripke Structure (PKS)). A PKS over a set AP of atomic propositions is a tuple = ⟨, 0, P, ℒ⟩ where (, P) is a MC, 0 ∈ is the initial state, and ℒ : → 2AP is a labeling function assigning a set of atomic propositions to any state ∈ .
Definition 3 (Probabilistic Obstruction Temporal Structure). A POTS (model for short) is given by a tuple ℳ = (, 0, P, ℒ, C) where = (, 0, P, ℒ) is a PKS and C : × → N is a function assigning to any pairs (, ′) a natural number ∈ N.
A path over ℳ is a finite or infinite sequence of states = 0, 1, 2, . . . starting from the initial state 0, where each step satisfies P(, +1) > 0 for all ∈ N. We use to denote the -th state in , ≤ for the prefix 0, . . . , , and ≥ for the sufix , +1 . . .. The set of all finite paths from a state ∈ in the model ℳ is denoted by Paths+ℳ,, and the set of all infinite paths is Paths*ℳ,. A history ℎ is any finite path prefix, with denoting the set of all histories, and (ℎ) representing the last state of a history ℎ. Given a finite path ^ = 0, 1, . . . , of states, the cylinder set of ^, denoted Cyl(^) = { ∈ Paths*ℳ,0 | ^ ∈ Prefix( )}, is the set of infinite paths = 0, 1, · · · , , · · · , where ^ is a prefix of . The set of infinite paths is supposed to be equipped with the -algebra generated by the cylinder sets of the finite paths and the probability measure given by Pr0 (Cyl(^)) = ∏︀=−01 P(, +1). ℳ Definition 4. Let ℳ be a model, be states in ℳ, C is the function cost and be a natural number, a -strategy is a function S : → 2× that, given a history ℎ, returns a subset ∈ × , such that: (i) ⊂ E((ℎ)) and (ii) (∑︀∈ C()) ≤ . A memoryless n-strategy is a n-strategy S such that for all histories ℎ and ℎ′ if (ℎ) = (ℎ′) then S(ℎ) = S(ℎ′) and E((ℎ)) denotes its outgoing edges, where E() = { ∈ × | = (, ′) for some ′ ∈ and P(, ′) > 0}.
A path is compatible with an n-strategy S if for all ≥ 1 we have that ( , +1) ∈/ S( ≤ ). The set of outcomes of an -strategy S and state is denoted as Out(, S) and it returns the set of all paths that can result from a strategy S and a state .
Definition 5. Let AP be an at most countable set of atomic formulas (or atoms). Formulas of Probabilistic
Obstruction Temporal Logic (POTL, for short) are defined by the following grammar:
◁▷
::= ⊤ | | ¬ | ∧ | ⟨ ⟩
::= X | U ≤ | U | R ≤ | R
where ∈ AP is an atomic formula, ∈ [
In this syntax, state formulas are evaluated over states, and path formulas are evaluated over paths. Model properties are expressed as state formulas, with path formulas used only in the probabilistic path ◁▷⟩ . Temporal operators like (next), U ≤ (bounded until), U (until), R ≤ (bounded operator ⟨ release), and R (release), are allowed in path formulas. The parameter is the grade of the strategic operator. Boolean connectives ⊥, ∨, and → are defined as usual. The formula ⟨ ◁▷⟩ with means “there is a demonic strategy such that all paths compatible with the strategy satisfy with a probability ◁▷ ", where a demonic strategy disables arcs. POTL formulas are interpreted over POTS, and we can now define their semantics precisely.
Definition 6. The satisfaction relation between a model ℳ, a state of ℳ, and a formula is defined by induction on the structure of :
◁▷ if there is a n-strategy S such that Prℳ({ ∈ Out(, S) | ℳ, |= }) ◁▷ . • ℳ, |= ⟨ ⟩ The satisfaction relation ℳ, |= between a model ℳ, a path ∈ Paths*ℳ, of ℳ, and path formula is defined as follows: • ℳ, |= X if ℳ, 2 |= . • ℳ, |= 1 U ≤ 2 if there is an 0 ≤ ≤ such that ℳ, |= 2 and ℳ, |= 1 for all 0 ≤ < . • ℳ, |= 1 U 2 if there is an ≥ 0 such that ℳ, |= 2 and ℳ, |= 1 for all 0 ≤ < . • ℳ, |= 1 R ≤ 2 if either ℳ, |= 2 for all 0 ≤ ≤ or there is an 0 ≤ ≤ such that ℳ, |= 1 and ℳ, |= 2 for all 0 ≤ ≤ . • ℳ, |= 1 R 2 if either ℳ, |= 2 for all ≥ 0 or there is an ≥ 0 such that ℳ, |= 1 and ℳ, |= 2 for all 0 ≤ ≤ .
Let be a formula and ℳ be a model. Then Sat(, ℳ) denotes the set of states of ℳ that satisfy , i.e., Sat(, ℳ) = { ∈ | ℳ, |= }. Two formulas and are equivalent (denoted by ≡ ) if, for all models ℳ, Sat(, ℳ) = Sat(, ℳ). The semantics of the obstruction probabilistic operator ⟨ ◁▷⟩ refers to the probability for the sets of paths where a path formula holds. To ensure that this is well-defined, we need to establish that the events specified by POTL path formulas are measurable. Since the set { ∈ Out(, S) | ℳ, |= } for POTL path formula can be considered as a countable union of cylinder sets, its measurability is ensured. This follows from the following lemma. Lemma 1. For each POTL path formula and state of a model ℳ, the set { ∈ Out(, S)| ℳ, |= } is measurable.
Here, we present the Weighted Timed Automata (WTA), the type of model that we use to verify TOTL
properties. A WTA is an extension of a TA [
Clock invariants Δ(X) are clock constraints in which ∼∈ { <, ≤} .
Definition 8 (Clock valuations). Given a finite set of clocks X, a clock valuation function, : X → R≥ 0 assigning to each clock ∈ X a non-negative value (). We denote R≥0 the set of all valuations. For a clock valuation ∈ R≥0 and a time value d ∈ R≥ 0, + d is the valuation satisfied by ( + )() = () + for each ∈ X. Given a clock subset ⊆ , we denote [ ← 0] the valuation defined as follows: [ ← 0]() = 0 if ∈ and [Y ← 0]() = () otherwise.
Definition 9 (Clock valuations). Given a finite set of clocks X, a clock valuation function, : X → R≥ 0 assigning to each clock ∈ X a non-negative value (). We denote R≥0 the set of all valuations. For a clock valuation ∈ R≥0 and a time value d ∈ R≥ 0, + d is the valuation satisfied by ( + )() = () + for each ∈ X. Given a clock subset ⊆ , we denote [ ← 0] the valuation defined as follows: [ ← 0]() = 0 if ∈ and [Y ← 0]() = () otherwise.
Definition 10 (Weighted Timed Automata ( WTA)). Let be a finite set of clocks and AP a finite set of atoms. A WTA is a tuple = (, 0, , Σ, , , , ℒ, ), where: is a finite set of locations, 0 ∈ is an initial location, is a finite set of clocks, Σ is a finite set of actions, ⊆ × Σ × Φ() × 2 × is a finite set of edges (or transitions), : → Δ() is a function that associates to each location a clock invariant, : → N≥ 0 is a function that labels the elements of , ℒ : → 2AP is a labeling function for the locations, ⊆ is a set of goal locations.
In WTA, costs are explicitly defined in its syntax, however, they do not influence the discrete behavior of the system. Since there is no cost constraint, the semantics of a WTA is similar to that of a TA. It is thus given as a Timed Transition System (TTS). In a TTS() = (Q, q0, ΣΔ, , , ℒ, Q ), the states are pairs of locations and clock valuations, with initial state 0=(0, 0), where all clocks ∈ are initially 0, ΣΔ = Σ ⊎ R≥ 0, the transition relation includes discrete transitions (, →)− (′, ′) based on satisfying guards and clock resets, and delay transitions (, →)− (, + ) for valid time elapses, the labeling function ℒ assigns atomic propositions to states based on their location and clock valuations and ⊆ × R≥0.
A path in TTS() is an infinite sequence of consecutive delays and discrete transitions. A finite path fragment of is a run in TTS() starting from the initial state 0 = (0, 0), with delay and discrete transitions alternating along the path: = 0 →−0 1′ →−a00 1 →−1 2′ →−a11 2 . . . − →1−− − − 1 ′ →−− . . .. We write to denote the -th element = (, ) of , ≤ to denote the prefix 0, . . . , of , and ≥ to denote the sufix , +1 . . . of . A history is any finite prefix of some path. We use to denote the set of histories. Let be a WTA. Here, we will use ′ to indicate the set of deactivated edges in . We will also use ind( ′) to indicate the set of edges induced by the deactivated edges in ′ in the TTS(). Definition 11. Let be a WTA and be a natural number. Given a model TTS(), a -strategy is a function S : → 2 that, given a history ℎ, returns a subset ′ such that: (i) ′ ⊂ ((ℎ)), (ii) ind( ′) ⊂ ((ℎ)), and (iii) (∑︀∈ ′ C()) ≤ . A memoryless -strategy is a -strategy S such that for all histories ℎ and ℎ′ if (ℎ) = (ℎ′) then S(ℎ) = S(ℎ′).
A path is compatible with a -strategy if for all ≥ 1, ( , , +1) ∈/ S( ≤ ), where ∈ Σ.
Given a state = (, ) and a -strategy S, (, S) refers to the set of pathways starting from that are consistent with S.
Definition 12. Let be a WTA, AP a set of atomic propositions (or atoms), a set of clocks of , and a non-empty set of clocks of the formula, where ∩ = ∅. Formulas of Timed Obstruction Temporal Logic (TOTL) are defined by the following grammar:
::= ⊤ | | ¬ | 1 ∧ 2 | | ⟨ ⟩( 1 U 2) | ⟨ ⟩( 1 R 2) | . where ∈ AP is an atomic formula, ∈ , ∈ N≥ 0 represents the grade of the strategic operator, and ∈ Φ( ∪ ).
It is possible to compare a formula clock with an automata clock using clock constraints , which apply to both. Boolean connectives ⊥, ∨, and → are defined as usual. In the formula . , the clock is called freeze identifier, which means starts at 0 in the current state, and must hold from that point. This can express timing requirements like punctuality or bounded response. For example, .⟨ ⟩(( 1 ∧ ≤ 7) U 2) means there is a demonic strategy ensuring 1 holds until 2 becomes valid within 7 time units. The intuitive meaning of a formula ⟨ ⟩ with timed temporal formula is: there is a demonic strategy such that all paths of the TTS that are compatible with the strategy satisfy . Unlike OL, TOTL does not use the next operator because time is continuous, and there is no unique “next" time. However, TOTL allows timing constraints, called timed temporal formulas, which are interpreted over TTS. The semantics of TOTL formulas are now defined precisely.
Definition 13 ( TOTL Semantics). Let be a WTA, a set of clocks of , a non-empty set of clocks of the formula, ∈ AP, ∈ Φ( ∪ ), and ℳ = TTS(). An extended state over is a triple (, , ), where = (, ) ∈ is a WTS state and a valuation for the formula clocks in . The satisfaction relation between a TTS ℳ, TOTL formulas and , and an extended state = (, , )1 of the formula, is given inductively as follows (Boolean operators are omitted because they are defined as usual): • ℳ, |= if |= . • ℳ, |= ⟨ ⟩( U ) if there is a -strategy S such that for all ∈ (, S) there is a ∈ N such that ℳ, |= and for all 0 ≤ < , ℳ, |= . 1To facilitate reading, from this point onward we will use only the symbol for an extended state.
• ℳ, |= ⟨ ⟩( R ) if there is a -strategy S such that for all ∈ (, S) we have that either ℳ, |= for all ∈ N or there is a ∈ N such that ℳ, |= and ℳ, |= for all 0 ≤ ≤ .
• ℳ, |= . if ℳ, (, [ ← 0], ) |= .
Two formulas and are semantically equivalent (denoted by ≡ ) if for any model ℳ and extended state of ℳ, ℳ, |= if ℳ, |= . The relationship between WTA and TTS is defined as follows.
Proposition 1. Let be a WTA and ∈ TOTL, then |= if TTS() |= .
Let be a formula, the set of extended states satisfying is independent of the valuation for the formula clocks. Thus, for any state = (, ) in a TTS and valuations , ′ for the formula clocks, we can get that ℳ, (, , ) |= if ℳ, (, , ′) |= . Therefore, when is closed, it makes sense to talk about a state that satisfies . Let be any formula, ( ∪ ) a set of clocks (formula and automaton) and be a WTA, then Sat( ) denotes the set of extended states of ℳ = TTS() verifying, , i.e., Sat( ) = { ∈ | ℳ, |= }.
In this section, we consider two case study related to cybersecurity scenario.
Probability theory is well-suited for cybersecurity risk analysis because it provides a framework for understanding and quantifying uncertainty. To illustrate this, we will consider the following general cybersecurity scenario. Let be an AG and we want to check if there are MTD response strategies that will satisfy certain security goals.
!
S0 exploit(v1 )
S1 exploit(v2 ) 0.30 0.70 access( t )
S2 S3
Consider the AG in Fig. 1 with four states: 0, 1, 2, and 3. Each state represents a state of the attacker in the system. If the attacker is in 0 or 1, he can perform one or two of the following actions: exploit vulnerability 1, exploit vulnerability 2, and access device . If the attacker succeeds in exploiting 1, he will transition to state 1. Here, we assume that depending on the attacker’s preferences, there are 70% chance that the attacker will attempt to access equipment and a 30% chance that he will attempt to exploit 2. In Table 1, there are the three possible actions the attacker
exploit(1) access() exploit(2)
1 2 3
47.5%
22.5%
24.7%
can deploy, with their respective countermeasures, cost, and efectiveness. Let Fig. 2 depict the POTS
ℳ, constructed using the information from the attack graph presented in [
ℳ
S0 0.475
Let 2 and 3 be the atomic propositions for the states, 2 and 3. We can express, via POTL formulas, the following security objective: • There is a defender strategy with a cost 4 such that the attacker reaches the state satisfying 2 or the state satisfying 3 with a probability less than a given threshold 0.1. The following POTL formula captures the objective: 1 := ⟨ 4<0.1 ⟩F (2 ∨ 3). • There exists a defender strategy with cost 5 such that the probability that the attacker reaches state satisfying 3 is less than 0.2. The following POTL formula captures the objective: 1 := ⟨ 5<0.2 ⟩F 3.
Based on the concepts of AG presented in Section 1, we want to determine if there are MTD strategies that can satisfy specific security objectives. To do this, we assume: (1) The defender always knows the attacker’s current state in the AG. (2) At any moment, there is a unique current state for the attacker in the AG. (3) When the attacker’s state is detected, the defender can activate one or more MTDs to temporarily remove outgoing edges from that state. (4) The total cost of deactivated edges is below a given threshold. (5) If the attacker launches an attack from its current state and the corresponding edge hasn’t been removed, the attack succeeds, moving the attacker to the next state. (6) if the corresponding edge has been removed, the attack fails, and the attacker remains in the current state. In the model in Fig. 3 assume that reaching states 1, 3, or 5 gives the attacker root privileges on a critical server . In addition, if the attacker completes attack steps 6 or 7 (reaching state 5), then the defender will obtain information on the identity of the attacker. Let be an atomic proposition that expresses the fact that the identity of the attacker is known. Let be an atomic proposition expressing the fact that the attacker has root privilege on the server . We can express, via TOL formulas, the following security objectives: • The attacker will never be able to obtain root privileges on server s unless the defender can obtain information about his identity within 3 time units: that is, either we want the attacker to never reach a state satisfying or if the attacker reaches such a state, the defender wants to be able to identify it within 3 time units (). By using 1 as a variable, the following TOL formula captures the objective: 1 := .⟨ 1 ⟩G ( ∨ ( → ⟨ 1 ⟩F(j ≤ 3 ∧ ))). • While the defender has not obtained information about the attacker identity within 5 time units, the attacker has not root privilege on the server : that is, we want to be false until we have identified the attacker () within 5 time units, if such an identification ever happens. Thus, by using 2 as a variable for a given threshold, we can write our objective by using the until connective: 2 := .⟨ 2 ⟩(¬ ∧ ≤ 5 U ).
Suppose that 1 and 2 are respectively 3 and 4. Let ℳ = TTS(), we have that ℳ, 0 |= 1 ∧ 2. To satisfy 1 consider the 3-memoryless strategy S1 that associates {⟨1, 2⟩} to 1, {⟨3, 4⟩} to 3, and ∅ to any other state of ℳ. Remark that for any path ∈ (0, S1) and any ∈ N we have that ℳ, |= if ∈ {1, 3, 5}. Thus, we must establish that ℳ satisfies ⟨ 3⟩F( ≤ 3 ∧ ) on 1 (resp. 3 and 5). To do so, we remark that (1, S1) (resp. (3, S1) and (5, S1)) only contains the path 1, 3, 5 (resp. 3, 5 and ) and that ℳ, 5 |= . Thus, we have obtained that there is a 5 strategy (i.e. S1) such that for all ∈ (0, S1) and all ∈ N either ℳ, |= ¬ or if ℳ, |= then there is a strategy (S1 itself) such that ℳ, |= for some ≥ 1 and for all ∈ ( , S1), as we wanted. Remark that if 1 < 3 then it is impossible to satisfy 1 in ℳ at 0. For the specification 2 = .⟨ 4⟩(¬ ∧ ≤ 5 U ), consider the 4-memoryless strategy S2 that associates {⟨0, 1⟩} to 0, {⟨2, 1⟩, ⟨2, 3⟩} to 2, {⟨4, 3⟩} to 4 and ∅ to 5. The only path in (0, S⋆) is 0, 2, 4, 5 and since 5 satisfies and all the other do not satisfy we obtain the wanted result.
S0 a2, x≤ 2, x:= 0
2 a1, x> 1 3
3 a1, y> 1, y:= 0
S2 a2x,:x=<05, 2 a4, y> 1, y:= 0 4
S4 a4, x > 2, 1 4 a5, y < 5, 3 y:= 0 a7, x > 5, x:= 0 6 5 a6, y > 5, y:= 0 a8
S5
Many papers have focused on the strategic capabilities of agents playing within dynamic game models.
In this section, we compare our approach with some of these papers. Previous research on sabotage
games by van Benthem led to Sabotage Modal Logic (SML) for graph reachability problems, with a
PSPACE-complete model checking problem [
Timed Obstruction Temporal Logic (TOTL) and Probabilistic Obstruction Temporal Logic (POTL) provide
powerful frameworks for reasoning about systems where timing and probability are critical factors. By
extending traditional temporal logics to account for both timed constraints and probabilistic behaviors,
TOTL and POTL allow for the specification and verification of complex properties in systems like smart
grids, where security, reliability, and performance are paramount. In our case study, we demonstrated
how TOTL and POTL could be applied to analyze and enhance the security of a smart grid under
cyber-attack. The ability to model both time-sensitive and probabilistic aspects of defense strategies
enables system designers and security analysts to develop more robust and cost-efective solutions.
There are several directions we would like to explore for future work. First of all, extending TOTL and
POTL to support reasoning about multi-agent systems, where multiple defenders and attackers interact,
would provide a more comprehensive framework for analyzing complex, distributed environments.
Additionally, integrating TOTL and POTL with machine learning techniques could lead to more adaptive
and intelligent defense strategies. For example, reinforcement learning could be used to optimize the
selection of defense strategies based on real-time feedback from the system. Finally, we would like to
implement these two logics in the VITAMIN tool [