Programmable Logic Controller(PLC) has been widely used in flexible manufacturing system(FMS), railway system and others ask for great safety. So the applications of practical have rigorous require on the correctness of the PLC program. Due to the ladder diagram is most widely use programming languages of PLC, research on the validation techniques of ladder diagram program received widespread attention. Although, the grammar errors of ladder diagram can be detected by the PLC compiler, yet for some logic errors that hidden within the program(especially the race condition of ladder diagram), the PLC compiler doesn’t work.The main content of this paper is about the race detection of ladder diagram. It includes use the relation graph to detect race and the Petri nets with inhibitor arcs to detect the race of ladder diagram.In the first part, the relation graph is defined, and a method is presented to transform ladder diagrams into relation graphs. As a result, the logical expressions in a ladder diagram are graphically described by relation graph structures. It is proved that races depend on loop structures in a relation graph. Lastly, a criterion is presented to judge whether a ladder diagram is free of race, and its computational complexity is polynomial.In the second part, the Petri nets with inhibitor arcs are used for the ladder diagram modeling. Meanwhile consider the cycle scan which the work principle of PLC, adding the places of sequential control to the Petri nets with inhibitor arcs. An improvement of reachability graph algorithm is proposed, relying on the structure of reachability graph to determine whether a ladder diagram is exist race. Generally, Due to the different of the initial state, there are many different of the reachability graphs. When all of reachability graph is no exist loop structure, it can judge the corresponding ladder diagram is free of race.Finally, several examples are given in this paper to prove the validity of the conclusions. |