Secret Protection in Labeled Petri Nets
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912695980130304 |
|---|---|
| author | Haar, Stefan Masopust, Tomáš Večeřa, Jakub |
| author_facet | Haar, Stefan Masopust, Tomáš Večeřa, Jakub |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_06135 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Secret Protection in Labeled Petri Nets Haar, Stefan Masopust, Tomáš Večeřa, Jakub Formal Languages and Automata Theory Systems and Control 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. |
| title | Secret Protection in Labeled Petri Nets |
| topic | Formal Languages and Automata Theory Systems and Control |
| url | https://arxiv.org/abs/2511.06135 |