Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | https://arxiv.org/abs/2508.19110 |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866914006879436800 |
|---|---|
| author | Piazza, Carla Romanello, Riccardo Rossi, Sabina |
| author_facet | Piazza, Carla Romanello, Riccardo Rossi, Sabina |
| contents | Persistent Stochastic Non-Interference (PSNI) was introduced to capture a quantitative security property in stochastic process algebras, ensuring that a high-level process does not influence the observable behaviour of a low-level component, as formalised via lumpable bisimulation. In this work, we revisit PSNI from a performance-oriented perspective and propose a new characterisation based on a refined behavioural relation. We introduce \emph{weak-exact equivalence}, which extends exact equivalence with a relaxed treatment of internal (\(τ\)) actions, enabling precise control over quantitative observables while accommodating unobservable transitions. Based on this, we define \emph{Exact PSNI} (EPSNI), a variant of PSNI characterised via weak-exact equivalence. We show that EPSNI admits the same bisimulation-based and unwinding-style characterisations as PSNI, and enjoys analogous compositionality properties. These results confirm weak-exact equivalence as a robust foundation for reasoning about non-interference in stochastic systems. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2508_19110 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Exact Persistent Stochastic Non-Interference Piazza, Carla Romanello, Riccardo Rossi, Sabina Performance Persistent Stochastic Non-Interference (PSNI) was introduced to capture a quantitative security property in stochastic process algebras, ensuring that a high-level process does not influence the observable behaviour of a low-level component, as formalised via lumpable bisimulation. In this work, we revisit PSNI from a performance-oriented perspective and propose a new characterisation based on a refined behavioural relation. We introduce \emph{weak-exact equivalence}, which extends exact equivalence with a relaxed treatment of internal (\(τ\)) actions, enabling precise control over quantitative observables while accommodating unobservable transitions. Based on this, we define \emph{Exact PSNI} (EPSNI), a variant of PSNI characterised via weak-exact equivalence. We show that EPSNI admits the same bisimulation-based and unwinding-style characterisations as PSNI, and enjoys analogous compositionality properties. These results confirm weak-exact equivalence as a robust foundation for reasoning about non-interference in stochastic systems. |
| title | Exact Persistent Stochastic Non-Interference |
| topic | Performance |
| url | https://arxiv.org/abs/2508.19110 |