Safeness-enforcing supervisory control for railway networks

We deal with the problem of modeling railway networks with Petri nets in order to apply the theory of supervisory control for discrete event systems to automatically design the system controller. We provide a modular representation of railway networks in terms of stations and tracks including sensors and semaphores. We ensure safeness and local liveness by imposing both the generalized mutual exclusion constraints and constraints involving the firing vector