VŠB-TUO — School project · Parallel and Distributed Systems (PES)
A Petri Net model and analysis of a traffic light system for a two-direction road intersection, submitted for the PES (Parallel and Distributed Systems) course at VŠB-TUO.
The model represents a semaphore synchronization network covering north-south and east-west traffic flows. It demonstrates signal state transitions, vehicle queuing, and safety properties that prevent simultaneous green lights in conflicting directions. The report covers the formal Petri Net model, reachability analysis, and correctness proofs.
- Open the Petri Net Editor.
- Load the
.npnfile from theassets/net/directory of this repository. - Use the editor to step through states and evaluate traffic conditions.
A full exported analysis is available in the Releases section.
- Compile the document:
pdflatex main.tex
This project was created as a school assignment at VŠB-TUO.