Author(s)

M. dos Santos Soares & J. Vrancken

Abstract

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. 1 Introduction Traffic control in urban roads is a major area in which Intelligent Transportation Systems approaches can be applied. Traffic signals are one of the main approaches to control an intersection. They act regulating, warning and guiding transportation with the purpose of improving safety and effi- ciency for pedestrians and vehicles. Among the main advantages of traffic signals are the flexibility of the signaling scheme, the ability to provide priority treatment and the feasibility of coordinated control along streets. But when not well-designed, traffic signals may lead to excessive delays when cycle lengths are too long and increase the frequency of collisions. Petri nets [1] are a common tool applied to design, simulate and analyze discrete event systems, such as traffic signals. Some of the advantages are the graphical representation, the possibility of analyzing properties and the

Keywords