After having modelled a system using Petri nets, the objective is to verify it satisfies some interesting properties. To do so, the construction of the reachability graph is introduced, which exhaustively explores all possible states of the system.