Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Jean Leneutre, Vadim Malvone, James Ortiz

TL;DR

The model checking complexity of POTL is explored and it is demonstrated 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.

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.

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

TL;DR

The model checking complexity of POTL is explored and it is demonstrated 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.

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.

Paper Structure

This paper contains 16 sections, 3 theorems, 9 equations, 2 figures, 1 table, 3 algorithms.

Table of Contents

  1. Introduction
  2. Structure of the work.
  3. Background
  4. General Concepts.
  5. Probability Distribution and Space.
  6. Attack Graphs and Moving Target Defense Mechanisms.
  7. Kripke Structure and Markov Chain.
  8. Path.
  9. Cylinder.
  10. Predecessors and Successors.
  11. Model and Logic
  12. Strategy and Outcomes.
  13. Model Checking
  14. Illustration Example
  15. Related Work
  16. ...and 1 more sections

Key Result

Lemma 1

For each $\textsf{POTL}$ path formula $\varphi$ and state $q$ of a model $\mathcal{M}$, the set $\{ \pi \in \textsf{Out}(q,\mathfrak{S}) | \ \mathcal{M}, \pi \models \varphi\}$ is measurable.

Figures (2)

  • Figure 1: Example of an AG$\mathcal{G}$ from IMZ16.
  • Figure 2: The POTS$\mathcal{M}$ from $\mathcal{G}$.

Theorems & Definitions (14)

  • Definition 1: Kripke Structure
  • Definition 2: Markov Chain
  • Definition 3: Probabilistic Kripke Structure
  • Definition 4: Probabilistic Obstruction Temporal Structure
  • Definition 5
  • Definition 6
  • Lemma 1
  • proof
  • Definition 7
  • Definition 8: Obstruction Predecessor
  • ...and 4 more