Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Secret Protection in Labeled Petri Nets

Stefan Haar, Tomáš Masopust, Jakub Večeřa

TL;DR

The paper addresses the Secret Protection Problem ($SPP$) for labeled Petri nets, introducing Parikh and indicator counting semantics for protected events. It adopts a worst-case complexity analysis by enumerating candidate policies and verifying $\chi$-validity via Yen's path logic, establishing membership in $ExpSpace$ and $ExpSpace$-completeness for the main variants. It shows that even under strong structural restrictions, the problem remains ExpSpace-hard, and that uniform and non-uniform variants are equivalent in cost. The results imply there is no polynomial-time or polynomial-space algorithm for $SPP$ on labeled Petri nets, and they motivate studying tractable fragments and practical synthesis methods.

Abstract

We study the secret protection problem (SPP), where the objective is to find a policy of minimal cost ensuring that every execution path from an initial state to a secret state contains a sufficient number of protected events. The problem was originally introduced and studied in the setting of finite automata. In this paper, we extend the framework to labeled Petri nets. We consider two variants of the problem: the Parikh variant, where all occurrences of protected events along an execution path contribute to the security requirement, and the indicator variant, where each protected event is counted only once per execution path. We show that both variants can be solved in exponential space for labeled Petri nets, and that their decision versions are ExpSpace-complete. As a consequence, there is no polynomial-time or polynomial-space algorithm for these problems.

Secret Protection in Labeled Petri Nets

TL;DR

The paper addresses the Secret Protection Problem () for labeled Petri nets, introducing Parikh and indicator counting semantics for protected events. It adopts a worst-case complexity analysis by enumerating candidate policies and verifying -validity via Yen's path logic, establishing membership in and -completeness for the main variants. It shows that even under strong structural restrictions, the problem remains ExpSpace-hard, and that uniform and non-uniform variants are equivalent in cost. The results imply there is no polynomial-time or polynomial-space algorithm for on labeled Petri nets, and they motivate studying tractable fragments and practical synthesis methods.

Abstract

We study the secret protection problem (SPP), where the objective is to find a policy of minimal cost ensuring that every execution path from an initial state to a secret state contains a sufficient number of protected events. The problem was originally introduced and studied in the setting of finite automata. In this paper, we extend the framework to labeled Petri nets. We consider two variants of the problem: the Parikh variant, where all occurrences of protected events along an execution path contribute to the security requirement, and the indicator variant, where each protected event is counted only once per execution path. We show that both variants can be solved in exponential space for labeled Petri nets, and that their decision versions are ExpSpace-complete. As a consequence, there is no polynomial-time or polynomial-space algorithm for these problems.

Paper Structure

This paper contains 7 sections, 9 theorems, 11 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Labeled Petri nets
  4. Secret Protection Problem
  5. Parikh-SPP
  6. Indicator-SPP
  7. Discussion and Conclusion

Key Result

Lemma 3

For every instance of Parikh-SPP, there is an instance of Parikh-SPP-U such that the costs of the respective Parikh-optimal protecting policies coincide.

Figures (4)

  • Figure 1: Sketch of the construction from the proof of Lemma \ref{['lemma2']} for $\gamma(a)=3$ (left) and the result of the construction with $\gamma(a)=1$ on the right.
  • Figure 2: Sketch of the construction from the proof of Theorem \ref{['Parikh-SPP-complexity-membership']}.
  • Figure 3: Sketch of the hardness construction from the proof of Theorem \ref{['Parikh-SPP-complexity']}.
  • Figure 4: Sketch of the reduction from the proof of Theorem \ref{['Indikator-SPP-complexity']}.

Theorems & Definitions (18)

  • Definition 1: $\chi$-optimal SPP ($\chi$-SPP)
  • Definition 2: Budget-constrained $\chi$-SPP (BC-$\chi$-SPP)
  • Lemma 3
  • proof
  • Theorem 4
  • proof
  • Corollary 5
  • Theorem 6
  • proof
  • Lemma 7
  • ...and 8 more