Non-interference analysis of bounded 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_ | 1866915564309446656 |
|---|---|
| author | Ran, Ning Wu, Zhengguang Zhang, Shaokang He, Zhou Seatzu, Carla |
| author_facet | Ran, Ning Wu, Zhengguang Zhang, Shaokang He, Zhou Seatzu, Carla |
| contents | This paper focuses on a fundamental problem on information security of bounded labeled Petri nets: non-interference analysis. As in hierarchical control, we assume that a system is observed by users at different levels, namely high-level users and low-level users. The output events produced by the firing of transitions are also partitioned into high-level output events and low-level output events. In general, high-level users can observe the occurrence of all the output events, while low-level users can only observe the occurrence of low-level output events. A system is said to be non-interferent if low-level users cannot infer the firing of transitions labeled with high-level output events by looking at low-level outputs. In this paper, we study a particular non-interference property, namely strong non-deterministic non-interference (SNNI), using a special automaton called SNNI Verifier, and propose a necessary and sufficient condition for SNNI. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_17582 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Non-interference analysis of bounded labeled Petri nets Ran, Ning Wu, Zhengguang Zhang, Shaokang He, Zhou Seatzu, Carla Formal Languages and Automata Theory This paper focuses on a fundamental problem on information security of bounded labeled Petri nets: non-interference analysis. As in hierarchical control, we assume that a system is observed by users at different levels, namely high-level users and low-level users. The output events produced by the firing of transitions are also partitioned into high-level output events and low-level output events. In general, high-level users can observe the occurrence of all the output events, while low-level users can only observe the occurrence of low-level output events. A system is said to be non-interferent if low-level users cannot infer the firing of transitions labeled with high-level output events by looking at low-level outputs. In this paper, we study a particular non-interference property, namely strong non-deterministic non-interference (SNNI), using a special automaton called SNNI Verifier, and propose a necessary and sufficient condition for SNNI. |
| title | Non-interference analysis of bounded labeled Petri nets |
| topic | Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2510.17582 |