Method for translating ladder diagrams to ordinary Petri nets
Xue-Kun Chen, Jiliang Luo, Pengfei Qi · 2012
Programmable logic controllers (PLCs) have been widely used in safe-critical systems, such as railway, nuclear power stations and petrochemical plants. Hence, the reliability and correctness of PLC programs are so important that formal methods are required to guarantee them. An algorithm is proposed to translate a Ladder Diagram (LD) to an ordinary Petri net (PN) system. Consequently, the PN theory can be used to simulate and analyze LD programs to verify whether PLC systems are live, reversible, and free of race and deadlocks.