Road Traffic Signals Modeling and Analysis with Petri nets and Linear Logic

The purpose of this paper is to model and analyze road intersection traffic signals by means of Petri nets and Linear Logic. The dynamic behavior of traffic signals is a discrete model. Several approaches have been applied to model and analyze traffic signals control, such as Petri nets. The Petri net formalism can be used to model an intersection that can be represented as a shared resource. Normally, the reachability tree is used to analyze the model in order to evaluate some good properties, such as absence of deadlocks and the return to the initial phase. The problem of this approach is the possibility of state-space explosion due to the high number of states that can be reached. The purpose of this paper is to model and formally analyze the good properties of traffic signals controlling a road intersection. A formal proof based on the sequent calculus of Linear Logic is done in order to analyze the properties of the model for a given scenario. The approach can prove that unsafe states, such as two greens in a shared road intersection, are not reached. This is done using the equivalence between Petri nets reachability and the proof of a set of sequents in Linear Logic.