Reachability Analysis For Flexible Manufacturing Systems Using Petri Nets

In flexible manufacturing system,the internet of things,communication networks and other computer networks are required to be designed to ensure the transmission of data.However,there are some security problems in the transmission and sharing of those data.Therefore,in the process of network design,it is necessary to ensure that the information transmitted cannot be obtained by intruders.For the problem of information security transmission in flexible manufacturing system,researchers have put forward many formal researches to promote system security,including anonymity,noninterference and opacity.Those approaches involve the problem of system state reachability.State traversal is the basis of security research,since it is necessary to determine which state is not allowed to be intruded by traversing the whole states of the system.The opaque characteristic describes the lack of information flow.Specifically,in the process of state set calculation for a system,there are some states called "secret",which cannot be inferred by the intruder through the observed states.As a consequence,the significance of studying the opacity is to design an information transmission network,so that the intruders are not able to calculate the secret information that the system needs to hide under any observation of the system.In the discrete event system,the opacity mainly includes the current-state opacity and the initial-state opacity and in this paper,we mainly study the current-state opacity.Due to the limited number of sensors,observers usually cannot observe all the states of the system.So in the process of analyzing the current-state opacity,a flexible model is needed to model some observable discrete event systems.It is also necessary to consider the state explosion of the system,because for large-scale flexible manufacturing system,the communication network is often large and complex.It is not practical to calculate all the states of the system through exhaustive methods with the low efficiency,and the computer cannot store such a large number of states as well.Therefore,it is urgent to design a more efficient and reliable method or data structure to solve the problem of state explosion in the process of system analysis.In this paper,labeled Petri net is used to model discrete event system.Petri net is an effective mathematical and graphical tool for system modeling,while labeled Petri net can simulate the system with unobservable events.The main contribution of this paper is to propose an algorithm based on the data structure of multi-valued decision diagram to solve the problem of state estimation and the current-state opacity in labeled Petri nets,and to prove the effectiveness of this algorithm by comparing the experiment with the latest research.Finally,based on the summarizing the work of this paper,the future work of the research on opacity based on multi-valued decision diagrams is prospected.