Cited By
View all- Schwammberger MHamarneh Q(2024)It’s Safe to Play While Driving: From a Spatial Traffic Logic Towards Traffic GamesBridging the Gap Between AI and Reality10.1007/978-3-031-75434-0_19(277-290)Online publication date: 30-Oct-2024
Verification of Fair Controllers for Urban Traffic Manoeuvres at Intersections
Pages 249 - 264
Abstract
Autonomous crossing manoeuvres at intersections are especially challenging. In related work, a crossing controller for provably safe autonomous urban traffic manoeuvres was introduced. We extend this controller by a decentralised communication procedure that ensures fair behaviour of the controller and also guarantees bounded liveness. We verify the correctness of our extension by an implementation and analysis with UPPAAL Stratego.
References
[1]
Hilscher M, Linker S, Olderog E-R, and Ravn AP Qin S and Qiu Z An abstract model for proving safety of multi-lane traffic manoeuvres Formal Methods and Software Engineering 2011 Heidelberg Springer 404-419
[2]
Hilscher M, Linker S, and Olderog E-R Liu Z, Woodcock J, and Zhu H Proving safety of traffic manoeuvres on country roads Theories of Programming and Formal Methods 2013 Heidelberg Springer 196-212
[3]
Schwammberger MAn abstract model for proving safety of autonomous urban trafficTheor. Comput. Sci.2018744143-1693852486
[4]
Schwammberger, M.: Introducing liveness into multi-lane spatial logic lane change controllers using UPPAAL. In: Gleirscher, M., Kugele, S., Linker, S. (eds.) Proceedings 2nd International Workshop on Safe Control of Autonomous Vehicles, SCAV@CPSWeek 2018. Volume 269 of EPTCS, pp. 17–31 (2018)
[5]
Behrmann G, David A, and Larsen KG Bernardo M and Corradini F A tutorial on Uppaal Formal Methods for the Design of Real-Time Systems 2004 Heidelberg Springer 200-236
[6]
David A, Jensen PG, Larsen KG, Mikučionis M, and Taankvist JH Baier C and Tinelli C Uppaal Stratego Tools and Algorithms for the Construction and Analysis of Systems 2015 Heidelberg Springer 206-211
[7]
Loos, S.M., Platzer, A.: Safe intersections: at the crossing of hybrid systems and verification. In: Yi, K. (ed.) Intelligent Transportation Systems, pp. 1181–1186 (2011)
[8]
Dresner K and Stone P A multiagent approach to autonomous intersection management J. Artif. Intell. Res. 2008 31 591-656
[9]
Naumann, R., Rasche, R., Tacken, J., Tahedl, C.: Validation and simulation of a decentralized intersection collision avoidance algorithm. In: Proceedings of Conference on Intelligent Transportation Systems, pp. 818–823. IEEE (1997)
[10]
Ferreira, M., Fernandes, R., Conceição, H., Viriyasitavat, W., Tonguz, O.K.: Self-organized traffic control. In: Proceedings of the Seventh ACM International Workshop on VehiculAr InterNETworking. VANET 2010, pp. 85–90. ACM (2010)
[11]
Li L and Wang F Cooperative driving at blind crossings using intervehicle communication IEEE Trans. Veh. Technol. 2006 55 1712-1724
[12]
Fathollahnejad, N., Villani, E., Pathan, R., Barbosa, R., Karlsson, J.: On reliability analysis of leader election protocols for virtual traffic lights. In: 43rd IEEE/IFIP Conference on Dependable Systems and Networks Workshop, pp. 1–12 (2013)
[13]
Asplund M Automatically proving the correctness of vehicle coordination ICT Express 2018 4 51-54
[14]
Alur R and Dill DLA theory of timed automataTheor. Comput. Sci.1994126183-2351271580
[15]
Kwiatkowska M, Norman G, Parker D, and Sproston J Larsen KG and Niebert P Performance analysis of probabilistic timed automata using digital clocks Formal Modeling and Analysis of Timed Systems 2004 Heidelberg Springer 105-120
[16]
Bischopink, C.: Moving hazards - reasoning about humand drivers in autonomous traffic. Master’s thesis, University of Oldenburg, Oldenburg (2018)
Index Terms
- Verification of Fair Controllers for Urban Traffic Manoeuvres at Intersections
Index terms have been assigned to the content through auto-classification.
Recommendations
Spatial and Timing Properties in Highway Traffic
Theoretical Aspects of Computing – ICTAC 2022AbstractWe introduce Timed Multi-Lane Spatial Logic (TMLSL), a logic to express spatial and timing properties in highway traffic. For this purpose, we combine State-Clock Logic (SCL) and Multi-Lane Spatial Logic with Scopes (MLSLS), using MLSLS formulae ...
An abstract model for proving safety of multi-lane traffic manoeuvres
ICFEM'11: Proceedings of the 13th international conference on Formal methods and software engineeringWe present an approach to prove safety (collision freedom) of multi-lane motorway traffic with lane-change manoeuvres. This is ultimately a hybrid verification problem due to the continuous dynamics of the cars. We abstract from the dynamics by ...
The Effect of Small Cars on the Capacity of Signalized Urban Intersections
Time headways between vehicles being discharged from a queue at a signalized urban intersection is a measure of the intersection's capacity. An event recorder actuated by tape switches on the road surface is used to measure headways at various ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Oct 2019
532 pages
ISBN:978-3-030-54993-0
DOI:10.1007/978-3-030-54994-7
© Springer Nature Switzerland AG 2020.
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 07 October 2019
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 01 Jan 2025
Other Metrics
Citations
Cited By
View all- Schwammberger MHamarneh Q(2024)It’s Safe to Play While Driving: From a Spatial Traffic Logic Towards Traffic GamesBridging the Gap Between AI and Reality10.1007/978-3-031-75434-0_19(277-290)Online publication date: 30-Oct-2024