A modular Petri net to modeling and scenario analysis of a network of road traffic signals

The dynamic behavior of a group of traffic signals controlling a network of intersections is a complex discrete event system that can be modeled by Petri nets. The approach used in this paper proposes a components-based design, which increases modularity, reduces complexity and is a good practice according to modern Systems Engineering. The main system elements are specified based on the proposed Petri net component with time intervals associated to places. The specified models are simulated through the common token player algorithm, and formal analysis using invariants and theorem proving are applied to verify models' soundness and to reason on specific scenarios.