Deadlock avoidance algorithm for FMS

Deadlock must be avoided via the shop controller during the Flexible Manufacturing System (FMS) performing. Considering the complexity of the FMS, various models have been tried for the analysis and design of shop controller. Petri net is suitable to describe the dynamic behavior of the discrete event system. The verification of the system behavior needs structure analysis with complex theoretical proof method. Temporal logic Model Checking has important advantages over traditional theorem prover. It is fully automatic and can produce possible counter-example that is particularly important in finding subtle error in complex transition systems. In this paper, a new method for the deadlock avoidance based on Petri net and Temporal Logic model checking is presented. The specification in the Temporal Logic is expressed according to some result of structure analysis of the Petri net. The model checking is employed to execute the formal verification, which will conduct an exhaustive exploration of all possible behaviors.