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

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

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 im...

Full description

Bibliographic Details
Main Author: Maike Schwammberger
Format: Article
Language:English
Published: Open Publishing Association 2018-04-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1804.04346v1
id doaj-4c2b03b0feea4b5288a993390ee994b3
record_format Article
spelling doaj-4c2b03b0feea4b5288a993390ee994b32020-11-25T01:49:22ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802018-04-01269Proc. SCAV 2018173110.4204/EPTCS.269.3:3Introducing Liveness into Multi-lane Spatial Logic lane change controllers using UPPAALMaike Schwammberger0 University of Oldenburg 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.http://arxiv.org/pdf/1804.04346v1
collection DOAJ
language English
format Article
sources DOAJ
author Maike Schwammberger
spellingShingle Maike Schwammberger
Introducing Liveness into Multi-lane Spatial Logic lane change controllers using UPPAAL
Electronic Proceedings in Theoretical Computer Science
author_facet Maike Schwammberger
author_sort Maike Schwammberger
title Introducing Liveness into Multi-lane Spatial Logic lane change controllers using UPPAAL
title_short Introducing Liveness into Multi-lane Spatial Logic lane change controllers using UPPAAL
title_full Introducing Liveness into Multi-lane Spatial Logic lane change controllers using UPPAAL
title_fullStr Introducing Liveness into Multi-lane Spatial Logic lane change controllers using UPPAAL
title_full_unstemmed Introducing Liveness into Multi-lane Spatial Logic lane change controllers using UPPAAL
title_sort introducing liveness into multi-lane spatial logic lane change controllers using uppaal
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2018-04-01
description 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.
url http://arxiv.org/pdf/1804.04346v1
work_keys_str_mv AT maikeschwammberger introducinglivenessintomultilanespatiallogiclanechangecontrollersusinguppaal
_version_ 1725006990856421376

Similar Items