A Verification Framework for Obstruction, Probability, and Time

Verifying strategic behaviour in real-time multi-agent systems under uncertainty is vital for safety- and security-critical domains. Existing obstruction logics treat either adversarial timing (TOL) or probabilistic risk (POTL), but real scenarios require both. We introduceProbabilisticTimedObstructionTemporalLogic (PTOTL), which unifies dense time, probabilities, and cost-bounded obstruction for real-time security games. Interpreted over Weighted Probabilistic Timed Automaton (WPTA), PTOTL models attacker–defender interactions where discrete actions evolve and time elapses, and the defender may disable transitions under a per-step budget. We give syntax and semantics and a symbolic model-checking procedure on a probabilistic zone graph. Despite the added strategic and probabilistic features, verification remains PSPACE, not higher than PTCTL or PTATL, while offering greater temporal expressiveness. An automotive Moving Target Defense (MTD) case study demonstrates practicality as a specification and verification language.

Authors

• Wissal Dahani Télécom Paris, IP Paris
• Jean Leneutre Télécom Paris, IP Paris
• Vadim Malvone Télécom Paris
• James Ortiz Université Paris-Est Créteil, LACL
• Axel Oscar Télécom Paris, IP Paris

Keywords

• Strategic reasoning
• Cybersecurity
• Model checking
• Quantitative verification
• Security games
• Moving Target Defense mechanisms