Abstract
Timed Petri nets (TPNs) are useful for performance evaluation of discrete event systems due to their mathematical formalism. This paper focuses on their use to model the preemption of emergency vehicle systems. The advantage of the proposed approach is the clear presentation of traffic light behaviors in terms of conditions and events that cause the preemption of phases being changed. The resulting models allow one to identify and thus avoid urgent spectacles in such systems by conditions and events of the model that control the phase of traffic light alternations. Moreover, this work proposes a new emergency vehicle preemption policy to ensure that emergency vehicles can pass through intersections with no or less delay. The analysis is performed to demonstrate how the models enforce the phase of traffic transitions by a reachability graph with time information. The liveness and reversibility of the proposed model are verified. To our knowledge, this is the first work that employs TPNs to model an emergency vehicle preemption system and identify its urgent spectacles for the purpose of their complete avoidance. This helps advance the state-of-the-art in traffic safety related to the intersection of roadways.