Persistent Stochastic Non-Interference (PSNI) has been 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 exact lumpable bisimulation, 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 Exact PSNI (EPSNI), a variant of PSNI, characterised via exact lumpable bisimilarity. EPSNI admits the same bisimulation-based and unwinding-style characterisations as PSNI, and enjoys analogous compositionality properties. These results confirm exact lumpable bisimilarity as a robust foundation for reasoning about non-interference in stochastic systems.
Exact Persistent Stochastic Non-interference
Piazza C.;
2027-01-01
Abstract
Persistent Stochastic Non-Interference (PSNI) has been 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 exact lumpable bisimulation, 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 Exact PSNI (EPSNI), a variant of PSNI, characterised via exact lumpable bisimilarity. EPSNI admits the same bisimulation-based and unwinding-style characterisations as PSNI, and enjoys analogous compositionality properties. These results confirm exact lumpable bisimilarity as a robust foundation for reasoning about non-interference in stochastic systems.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
