With Multi-lane Spatial Logic (MLSL) a powerful approach to formally reason about and prove safety of autonomous traffic manoeuvres was introduced. Extended timed automata controllers using MLSL were constructed to commit safe lane change manoeuvres on highways. However, the approach has only few implementation and verification results. We thus strenghen the MLSL approach by implementing their lane change controller in UPPAAL and confirming the safety of the lane change protocol. We also detect the unlive behaviour of the original controller and thus extend it to finally verify liveness of the new lane change controller.


    Access

    Download


    Export, share and cite



    Title :

    Introducing Liveness into Multi-lane Spatial Logic lane change controllers using UPPAAL


    Contributors:

    Publication date :

    2018


    Remarks:

    In Proceedings SCAV 2018, arXiv:1804.03406
    EPTCS 269, 2018, pp. 17-31



    Type of media :

    Preprint


    Type of material :

    Electronic Resource


    Language :

    English





    LANE ASSIGNMENT METHOD AND SYSTEM USING MULTI-LANE DETECTION AND LANE CHANGE DETECTION

    KIM JUN MO / JUNG HEE CHUL / LEE HYUNG SEOK | European Patent Office | 2015

    Free access


    LANE CHANGE SYSTEM AND LANE CHANGE CONTROLLER

    ZHANG YU | European Patent Office | 2018

    Free access

    Lane change system and lane change controller

    ZHANG YU | European Patent Office | 2019

    Free access