<![CDATA[This study aims to examine the traffic light model for a five-arm intersection. Two types of traffic light models were studied, namely the standard type and the modified Norwegian type. Traffic lights have a fixed phase scheduling sequence. The traffic light modeling method uses Petri nets to graphically represent the behavioral structure of mathematical modeling symbols in distributed discrete systems. The results of the study show that the Occurrence Graph of the standard traffic light and the modified Norwegian traffic light meet the Coverability Tree requirements for all possible finite states. The Coverability Tree method also includes the properties of boundedness and conservation, along with all transition sequences that fire. The Petri net model satisfies the live property because it never enters a deadlock or a state where no transition can fire. The Petri net model has also satisfied the Invariants property, which represents signal behavior that does not change over time. The Petri net model is declared correct and valid because it satisfies all required properties. The model can present the structure of traffic light behavior at a five-arm intersection.]]>
Copyrights © 2026
