On the liveness of guidepath-based, zone-controlled dynamically routed, closed traffic systems

Zone-controlled, guidepath-based, dynamically routed, closed traffic systems constitute the modelling abstraction for a large set of industrial and public transport systems. An important requirement for the traffic flow of these systems is that the vehicles maintain their ability to access every location in the underlying guidepath-network, throughout the entire, presumably infinite, length of the system operation. States in which the system preserves the aforementioned property are said to be live. This work provides a structural characterization of state liveness that: i) enables the identification of live states while foregoing an extensive enumeration of the underlying behavioral space and ii) facilitates the design of computationally efficient liveness-enforcing supervisors.