A Timed Obstruction Logic for Dynamic Game Models

TL;DR

The paper introduces Timed Obstruction Logic (TOL), an expressive extension of Obstruction Logic for specifying real-time objectives in two-player weighted timed automata with demonic edge-deactivation strategies. It develops a zone-graph–based model-checking approach and proves that TOL verification is PSPACE-complete, matching the complexity of classical timed logics while increasing expressiveness. The authors situate TOL relative to TCTL, $T_{\mu}$, and TATL via translations, and demonstrate practical applicability through case studies and a prototype implementation in the VITAMIN model checker with preliminary performance results. The work contributes a formal verification framework for cybersecurity-style dynamics (attacker/defender, MTD) in real-time, and outlines future directions including multi-player extensions, probabilistic enrichments, and imperfect-information considerations.

Abstract

Real-time cybersecurity and privacy applications require reliable verification methods and system design tools to ensure their correctness. Many of these reactive real-time applications embedded in various infrastructures, such as airports, hospitals, and oil pipelines, are potentially vulnerable to malicious cyber-attacks. Recently, a growing literature has recognized Timed Game Theory as a sound theoretical foundation for modeling strategic interactions between attackers and defenders. This paper proposes Timed Obstruction Logic (TOL), an extension of Obstruction Logic (OL), a formalism for verifying specific timed games with real-time objectives unfolding in dynamic models. These timed games involve players whose discrete and continuous actions can impact the underlying timed game model. We show that TOL can be used to describe important timed properties of real-time cybersecurity games. Finally, in addition to introducing our new logic and adapting it to specify properties in the context of cybersecurity, we provide a verification procedure for TOL and show that its complexity is PSPACE-complete, meaning that it is not higher than that of classical timed temporal logics like TCTL. Thus, we increase the expressiveness of properties without incurring any cost in terms of complexity.

Figures (6)

• Figure 1: A WTS where states $s_2,\, s_3$ and $s_5$ represents the goal states of the attacker.
• Figure 2: A WTA with two clocks $x$ and $y$.
• Figure 3: A WTA from CLM23 where states $s_1,\, s_3$ and $s_5$ represent the goals of the attacker and the blue nodes satisfy $r_s$, the red node satisfies both $a$ and $r_s$, and the white ones satisfy neither $r_s$ nor $a$.
• Figure 4: VITAMIN high-level architecture FerrandoMalvone2025.
• Figure 5: The pipeline model with $k=4$.

Theorems & Definitions (33)

• Definition 1: Weighted Transition Systems (WTS)
• Example 1
• Definition 2: Clock constraints and invariants
• Definition 3: Clock valuations
• Definition 4: Weighted Timed Automata (WTA)
• Definition 5: Semantics of WTA
• Definition 6
• Example 2
• Definition 7: Discrete and Time Predecessor
• Definition 8: Predecessor