LCPN: a method for modelling ladder diagrams by colored Petri nets and its use in race detection

We propose a method for modelling of ladder diagrams named LCPN (Ladder Colored Petri Net). This method accepts a ladder diagram and generates its colored Petri net. By LCPN, not only the logic of ladder diagrams could be simulated but also the scanning paradigm which includes reading inputs, evaluating rungs, updating outputs could be modeled. Besides, the resulted Petri net proved to have a finite state space which makes it suitable for analyzing. In addition, we will describe an algorithm for checking the presence of race condition in a ladder diagram based on the state space of the colored Petri net. Furthermore, LCPN has been compared with other modelling techniques and its competitiveness in many aspects will be shown. In order to show the applicability of our algorithm we implemented it and did some tests on it. The results confirm our assertions.