Prasanna, S.Gulati, A.Anagha, H.C.Prabhu, A.Das, M.Mohan, B.R.2026-02-0620242024 IEEE International Conference on Interdisciplinary Approaches in Technology and Management for Social Innovation, IATMSI 2024, 2024, Vol., , p. -https://doi.org/10.1109/IATMSI60426.2024.10502455https://idr.nitk.ac.in/handle/123456789/29076This paper introduces and analyses the performance of the Petri net model created to simulate a traffic control system using the Additive Increase Multiplicative Decrease (AIMD) algorithm. The Petri net model was designed using TimeNET [1] tool. The model was evaluated by analysing the Reachability Graph generated by a Depth First Search (DFS) and Backtracking based algorithm. Several criteria such as Stability, Boundedness, Deadlock, etc. were verified by our proposed algorithm. The model was then validated through a C++ code to ensure it performs correctly under different situations. All the related code, images, and tables used in this paper can be found at GitHub 1 © 2024 IEEE.BoundednessDeadlockDepth First SearchPetri NetReachability GraphSimulationPetri Net-Based Verification of Adaptive Traffic Light Control with AIMD Algorithm