Probabilistic Obstruction Temporal Logic: a Probabilistic Logic to Reason about Dynamic Models

TL;DR

This paper introduces Probabilistic Obstruction Temporal Logic (POTL), a new formalism that extends Obstruction Logic with probabilistic reasoning to analyze dynamic models involving strategic attacker-defender interactions.

Contribution

It presents a novel probabilistic logic framework, POTL, that is expressive and computationally feasible for reasoning about probabilistic behaviors in security contexts.

Findings

POTL extends Obstruction Logic with probabilistic elements.

Model checking complexity of POTL is comparable to PCTL.

POTL is suitable for cybersecurity and privacy applications.

Abstract

In this paper, we propose a novel formalism called Probabilistic Obstruction Temporal Logic (POTL), which extends Obstruction Logic (OL) by incorporating probabilistic elements. POTL provides a robust framework for reasoning about the probabilistic behaviors and strategic interactions between attackers and defenders in environments where probabilistic events influence outcomes. We explore the model checking complexity of POTL and demonstrate that it is not higher than that of Probabilistic Computation Tree Logic (PCTL), making it both expressive and computationally feasible for cybersecurity and privacy applications.