Bisimulation non-interference analysis of bounded Petri nets

In the hierarchical control, a system could be monitored by high-level and low-level users, who may obtain different information even if both know the structure of the system. Low-level users can only observe the occurrence of a subset of events, while high-level users can observe the occurrence of all the events affecting the system dynamics. A system is said bisimulation strong non-deterministic non-interferent (BSNNI) if low-level users can neither infer the occurrence of high-level transitions, nor infer the nonoccurrence of high-level transitions. In this paper, we focus on BSNNI analysis and enforcement of bounded Petri nets. We show that, under the assumption of acyclicity of the high-level subnet, the notions of basis marking and basis reachability graph (BRG) allow to solve such problems with clear advantages in terms of computational complexity since they prevent exhaustive marking enumeration.