Scenario analysis of a network of traffic signals designed with Petri nets

The Petri net formalism is a powerful tool to model and analyze discrete event systems. The dynamic behavior of traffic signals is a discrete model and is one of the most important and effective methods of controlling traffic at intersections. In this paper, Petri nets are applied to model a network of intersections and the formal proof is based on the sequent calculus of Linear Logic. The approach can prove that unsafe states are not reached, and that desirable states are reached. This is done using the equivalence between Petri nets reachability and the proof of a set of sequents in Linear Logic. The approach is illustrated by an example of a network of intersections controlled by traffic signals.