In: Real-Time Systems, Vol. 9, No. 3, pages 241-263. 1995.
Abstract: In this paper interval timed colored Petri nets ((van der Aalst, 1993)) are used to model and analyze railway stations. We will show that this approach can be used to evaluate both station operating schedules and the infrastructure of a station. An interval timed colored Petri net (ITCPN) is a colored Petri net extended with time; time is in tokens and transitions determine a delay for each produced token. This delay is specified by an upper and lower bound, i.e. an interval. The ITCPN model allows for the modeling of the dynamic behavior of large and complex systems, without loosing the possibility of formal analysis. In addition to the existing analysis techniques for colored Petri nets, we use a new analysis method to analyze the temporal behavior of the net. This method constructs a reduced reachability graph and exploits the fact that delays are described by an interval. We will also discuss other (Petri net based) methods that can be used to analyze railway stations.
Keywords: colored Petri nets, interval Petri nets, railway station models.