Name
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. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.4204/EPTCS.51.2 | SecCo |
Keywords | Field | DocType |
secure computation,petri net | Control theory,Petri net,Computer science,Computer security,Algorithm,Decidability,Theoretical computer science,Process architecture,Stochastic Petri net,Equivalence (measure theory),Transitive relation,Undecidable problem | Journal |
Volume | ISSN | Citations |
51 | EPTCS 51, 2011, pp. 16-33 | 9 |
PageRank | References | Authors |
0.53 | 7 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Eike Best | 1 | 93 | 6.86 |
| Philippe Darondeau | 2 | 715 | 77.04 |
| Roberto Gorrieri | 3 | 2297 | 184.63 |