Timed Obstruction Logic: A Timed Approach to Dynamic Game Reasoning

Real-time cybersecurity and privacy applications require reliable verification methods and system design tools to ensure their correctness. 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), 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, 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 additional complexity.