Non-interference enforcement in bounded Petri nets

In this paper we first extend an approach recently presented by the authors, to check non-interference in discrete event systems modeled using Petri nets. The proposed technique is based on the solution of integer linear programming optimization problems. A new version of the analysis result is given in this paper, which does not require anymore the acyclicity of the subnet induced by the low-level transitions. Then, the main contribution of this paper, an algorithm that enforces non-interference by selecting offline the smallest subset of high-level transitions to be disabled, is presented.