Automatic generation of Petri Net supervisors for interlocking design

Signalization and interlocking design is one of the most crucial components that provide safe travelling and transportation on railways. In order to satisfy the requirements of CENELEC (European Committee for Electrotechnical Standardization) standards that are used for railways, there is a need of formal methods. While providing these standards, Petri Net design method also brings simplicity on programming after the design stage. In this study, a Mathematica^© based programme that generates Petri Net supervisors automatically will be described.