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.


    Access

    Access via TIB

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Road traffic signals modeling and analysis with Petri nets and linear logic


    Contributors:


    Publication date :

    2007


    Size :

    6 Seiten, 20 Quellen



    Type of media :

    Conference paper


    Type of material :

    Print


    Language :

    English




    Modeling Traffic Signal Control Using Petri Nets

    List, G.F. | Online Contents | 2004


    Modeling traffic signal control using Petri nets

    List, G.F. / Cetin, M. | IEEE | 2004


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

    dos Santos Soares, M. / Vrancken, J. | British Library Conference Proceedings | 2007


    Logic control design with Petri nets

    Ferrarini, L. / Maffezzoni, C. / Associazione Nazionale Italiana per l'Automazione | British Library Conference Proceedings | 1993


    A logic for Petri nets

    Pradier-Chezalviel, B. / Valette, R. | British Library Online Contents | 1997