Modeling and supervisory control of railway networks using Petri nets

In this paper we deal with the problem of modeling railway networks with Petri nets so as 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 first ensure safeness and local liveness imposing both Generalized Mutual Exclusion Constraints and constraints also involving the firing vector. The detailed model used in this first step can be abstracted, considering a higher-level description of a railway network that belongs to the class of ES2PR (Extended Simple Sequential Process with Resources) nets and show that global liveness may be enforced by adding appropriate monitor places designed using siphon analysis. In our approach this can be done without an exhaustive computation of all siphons and we can characterize the cases in which the procedure can be recursively applied, giving a simple test for closed loop net to remain an ES2PR net.