On the Decidability of Non Interference over Unbounded Petri Nets

Eike Best 1 Philippe Darondeau 2 Roberto Gorrieri 3
2 S4 - System synthesis and supervision, scenarios
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : Non-interference, in transitive or intransitive form, is defined here over unbounded (Place/Transition) Petri nets. The definitions are adaptations of similar, well-accepted definitions introduced earlier in the framework of labelled transition systems. The interpretation of intransitive non-interference which we propose for Petri nets is as follows. A Petri net represents the composition of a controlled and a controller systems, possibly sharing places and transitions. Low transitions represent local actions of the controlled system, high transitions represent local decisions of the controller, and downgrading transitions represent synchronized actions of both components. Intransitive non-interference means the impossibility for the controlled system to follow any local strategy that would force or dodge synchronized actions depending upon the decisions taken by the controller after the last synchronized action. The fact that both language equivalence and bisimulation equivalence are undecidable for unbounded labelled Petri nets might be seen as an indication that non-interference properties based on these equivalences cannot be decided. We prove the opposite, providing results of decidability of non-interference over a representative class of infinite state systems.
Type de document :
Communication dans un congrès
SecCo : International Workshop on Security Issues in Concurrency, Aug 2010, Paris, France. pp.16-33, 2011
Liste complète des métadonnées

https://hal.inria.fr/inria-00591568
Contributeur : Philippe Darondeau <>
Soumis le : lundi 9 mai 2011 - 15:45:12
Dernière modification le : mercredi 16 mai 2018 - 11:23:05

Lien texte intégral

Identifiants

  • HAL Id : inria-00591568, version 1
  • ARXIV : 1102.5585

Citation

Eike Best, Philippe Darondeau, Roberto Gorrieri. On the Decidability of Non Interference over Unbounded Petri Nets. SecCo : International Workshop on Security Issues in Concurrency, Aug 2010, Paris, France. pp.16-33, 2011. 〈inria-00591568〉

Partager

Métriques

Consultations de la notice

98