Secret Protection in Labeled Petri Nets

TL;DR

This paper extends the secret protection problem from finite automata to labeled Petri nets, analyzing its computational complexity and demonstrating its ExpSpace-completeness.

Contribution

It introduces the secret protection problem for labeled Petri nets and establishes its computational complexity as ExpSpace-complete.

Findings

Both variants are solvable in exponential space.

Decision problems are ExpSpace-complete.

No polynomial-time algorithms exist for these problems.

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.