Analysis of railway stations by means of interval timed coloured Petri nets

In this paperinterval timed coloured Petri nets ((van der Aalst, 1993)) are used to model and analyse 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 coloured Petri net (ITCPN) is a coloured 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 modelling of the dynamic behaviour of large and complex systems, without loosing the possibility of formal analysis. In addition to the existing analysis techniques for coloured Petri nets, we use a new analysis method to analyse the temporal behaviour 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 analyse railway stations.