@article(AD94, author = {Rajeev Alur and David L. Dill}, year = {1994}, title = {A Theory of Timed Automata}, journal = {Theoretical Computer Science}, volume = {126}, number = {2}, pages = {183--235}, doi = {10.1016/0304-3975(94)90010-8}, ) @incollection(alves_reliable_2020, author = {Gleifer Vaz Alves and Louise Dennis and Lucas Fernandes and Michael Fisher}, year = {2020}, title = {Reliable {Decision}-{Making} in {Autonomous} {Vehicles}}, editor = {Andrea Leitner and Daniel Watzenig and Ibanez-Guzman, Javier}, booktitle = {Validation and {Verification} of {Automated} {Systems}: {Results} of the {ENABLE}-{S3} {Project}}, publisher = {Springer International Publishing}, address = {Cham}, pages = {105--117}, doi = {10.1007/978-3-030-14628-3\_10}, ) @inproceedings(alves_formalisation_2020, author = {Gleifer Vaz Alves and Louise Dennis and Michael Fisher}, year = {2020}, title = {Formalisation and {Implementation} of {Road} {Junction} {Rules} on an {Autonomous} {Vehicle} {Modelled} as an {Agent}}, editor = {Emil Sekerinski and Nelma Moreira and Jos\IeC{\'e} N. Oliveira and Daniel Ratiu and Riccardo Guidotti and Marie Farrell and Matt Luckcuck and Diego Marmsoler and Jos\IeC{\'e} Campos and Troy Astarte and Laure Gonnord and Antonio Cerone and Luis Couto and Brijesh Dongol and Martin Kutrib and Pedro Monteiro and David Delmas}, booktitle = {Formal {Methods}. {FM} 2019 {International} {Workshops}}, series = {Lecture {Notes} in {Computer} {Science}}, publisher = {Springer International Publishing}, address = {Cham}, pages = {217--232}, doi = {10.1007/978-3-030-54994-7\_16}, ) @article(jsan10030041, author = {Gleifer Vaz Alves and Louise Dennis and Michael Fisher}, year = {2021}, title = {A Double-Level Model Checking Approach for an Agent-Based Autonomous Vehicle and Road Junction Regulations}, journal = {Journal of Sensor and Actuator Networks}, volume = {10}, number = {3}, doi = {10.3390/jsan10030041}, url = {https://www.mdpi.com/2224-2708/10/3/41}, ) @misc(avary_safe_2020, author = {Michelle Avary and Tim Dawkins}, year = {2020}, title = {Safe {Drive} {Initiative}: {Creating} safe autonomous vehicle policy ({World} {Economic} {Forum})}, url = {https://www.weforum.org/reports/safe-drive-initiative-creating-safe-autonomous-vehicle-policy/}, ) @inproceedings(BDL04, author = {Gerd Behrmann and Alexandre David and Kim G. Larsen}, year = {2004}, title = {A Tutorial on Uppaal}, editor = {Marco Bernardo and Flavio Corradini}, booktitle = {Formal Methods for the Design of Real-Time Systems}, publisher = {Springer}, pages = {200--236}, doi = {10.1007/978-3-540-30080-9\_7}, ) @inproceedings(bhuiyan_traffic_2020, author = {Hanif Bhuiyan and Guido Governatori and Andy Bond and S{\'{e}}bastien Demmel and Mohammad Badiul Islam and Andry Rakotonirainy}, year = {2020}, title = {Traffic Rules Encoding Using Defeasible Deontic Logic}, editor = {Villata Serena and Jakub Harasta and Petr Kremen}, booktitle = {Legal Knowledge and Information Systems - {JURIX} 2020: The Thirty-third Annual Conference, Brno, Czech Republic, December 9-11, 2020}, series = {Frontiers in Artificial Intelligence and Applications}, volume = {334}, publisher = {{IOS} Press}, pages = {3--12}, doi = {10.3233/FAIA200844}, ) @inproceedings(BS19, author = {Christopher Bischopink and Maike Schwammberger}, year = {2019}, title = {Verification of Fair Controllers for Urban Traffic Manoeuvres at Intersections}, editor = {Emil Sekerinski and Nelma Moreira and Jos{\'{e}} N. Oliveira and Daniel Ratiu and Riccardo Guidotti and Marie Farrell and Matt Luckcuck and Diego Marmsoler and Jos{\'{e}} Campos and Troy Astarte and Laure Gonnord and Antonio Cerone and Luis Couto and Brijesh Dongol and Martin Kutrib and Pedro Monteiro and David Delmas}, booktitle = {Formal Methods. {FM} 2019 International Workshops - Porto, Portugal, October 7-11, 2019, Revised Selected Papers, Part {I}}, series = {Lecture Notes in Computer Science}, volume = {12232}, publisher = {Springer}, pages = {249--264}, doi = {10.1007/978-3-030-54994-7\_18}, ) @mastersthesis(Bi18, author = {Cristopher Bischopink}, year = {2018}, title = {Moving Hazards - Reasoning about humand drivers in autonomous traffic}, school = {University of Oldenburg}, ) @inproceedings(DMPR18, author = {Werner Damm and Eike M{\"{o}}hlmann and Thomas Peikenkamp and Astrid Rakow}, year = {2018}, title = {A Formal Semantics for Traffic Sequence Charts}, editor = {Marten Lohstroh and Patricia Derler and Marjan Sirjani}, booktitle = {Principles of Modeling - Essays Dedicated to Edward A. Lee on the Occasion of His 60th Birthday}, publisher = {Springer}, pages = {182--205}, doi = {10.1007/978-3-319-95246-8\_11}, ) @misc(department_for_transport_using_2017, author = {{Department for Transport}}, year = {2017}, title = {Using the road (159 to 203) - {The} {Highway} {Code} - {Guidance} - {GOV}.{UK}}, url = {https://www.gov.uk/guidance/the-highway-code/using-the-road-159-to-203}, ) @inproceedings(CARLA, author = {Alexey Dosovitskiy and Germ{\'{a}}n Ros and Felipe Codevilla and Antonio M. L{\'{o}}pez and Vladlen Koltun}, year = {2017}, title = {{CARLA:} An Open Urban Driving Simulator}, booktitle = {1st Annual Conference on Robot Learning, CoRL 2017, Mountain View, California, USA, November 13-15, 2017, Proceedings}, series = {Proceedings of Machine Learning Research}, volume = {78}, publisher = {{PMLR}}, pages = {1--16}, url = {http://proceedings.mlr.press/v78/dosovitskiy17a.html}, ) @inproceedings(EGK20, author = {Klemens Esterle and Luis Gressenbuch and Alois C. Knoll}, year = {2020}, title = {Formalizing Traffic Rules for Machine Interpretability}, booktitle = {3rd {IEEE} Connected and Automated Vehicles Symposium, {CAVS} 2020, Victoria, BC, Canada, November 18 - December 16, 2020}, publisher = {{IEEE}}, pages = {1--7}, doi = {10.1109/CAVS51000.2020.9334599}, ) @inproceedings(Getal14, author = {Shalini Ghosh and Daniel Elenius and Wenchao Li and Patrick Lincoln and Natarajan Shankar and Wilfried Steiner}, year = {2016}, title = {ARSENAL: Automatic Requirements Specification Extraction from Natural Language}, editor = {Sanjai Rayadurgam and Oksana Tkachuk}, booktitle = {NASA Formal Methods}, publisher = {Springer International Publishing}, address = {Cham}, pages = {41--46}, doi = {10.1007/978-3-319-40648-0\_4}, ) @misc(hawkins_tesla_2021, author = {Andrew J. Hawkins and Richard Lawler}, year = {2021}, title = {Tesla finally begins shipping \IeC{\textquoteleft}{Full} {Self}-{Driving}\IeC{\textquoteright} beta version 9 after a long delay}, url = {https://www.theverge.com/2021/7/10/22570081/tesla-fsd-v9-beta-autopilot-update}, ) @inproceedings(HLO13, author = {Martin Hilscher and Sven Linker and Ernst{-}R{\"{u}}diger Olderog}, year = {2013}, title = {Proving Safety of Traffic Manoeuvres on Country Roads}, editor = {Zhiming Liu and Jim Woodcock and Huibiao Zhu}, booktitle = {Theories of Programming and Formal Methods - Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday}, series = {Lecture Notes in Computer Science}, volume = {8051}, publisher = {Springer}, pages = {196--212}, doi = {10.1007/978-3-642-39698-4\_12}, ) @inproceedings(HLOR11, author = {Martin Hilscher and Sven Linker and Ernst-R{\"u}diger Olderog and Anders P. Ravn}, year = {2011}, title = {An Abstract Model for Proving Safety of Multi-lane Traffic Manoeuvres}, editor = {Shengchao Qin and Zongyan Qiu}, booktitle = {13th Int. Conference on Formal Engineering Methods, {ICFEM}, Proc.}, publisher = {Springer}, pages = {404--419}, doi = {10.1007/978-3-642-24559-6\_28}, ) @misc(sae2018, author = {SAE International}, year = {2018}, title = {J 3016: Surface vehicle recommended practice -- (R) Taxonomy and Definitions for Terms Related to Driving Automation Systems for On-Road Motor Vehicles}, ) @article(jin_tesla_2021, author = {Hyunjoo Jin}, year = {2021}, title = {Tesla tells regulator that full self-driving cars may not be achieved by year-end}, journal = {Reuters}, url = {https://www.reuters.com/business/autos-transportation/tesla-tells-regulator-that-full-self-driving-cars-may-not-be-achieved-by-year-//2021-05-07/}, ) @inproceedings(KD20, author = {Abolfazl Karimi and Parasara Sridhar Duggirala}, year = {2020}, title = {Formalizing traffic rules for uncontrolled intersections}, booktitle = {11th {ACM/IEEE} International Conference on Cyber-Physical Systems, {ICCPS} 2020, Sydney, Australia, April 21-25, 2020}, publisher = {{IEEE}}, pages = {41--50}, doi = {10.1109/ICCPS48487.2020.00012}, ) @misc(law_commission_automated_2020, author = {Law Commission, UK}, year = {2020}, title = {Automated {Vehicles}: {Summary} of the {Analysis} of {Responses} to {Consultation} {Paper} 2 on {Passenger} {Services} and {Public} {Transport}}, url = {https://www.lawcom.gov.uk/project/automated-vehicles/}, ) @article(Mos85, author = {Ben Moszkowski}, year = {1985}, title = {A Temporal Logic for Multilevel Reasoning About Hardware}, journal = {Computer}, volume = {18}, number = {2}, pages = {10--19}, doi = {10.1109/MC.1985.1662795}, ) @inproceedings(OS17, author = {Ernst{-}R{\"{u}}diger Olderog and Maike Schwammberger}, year = {2017}, title = {Formalising a Hazard Warning Communication Protocol with Timed Automata}, editor = {Luca Aceto and Giorgio Bacci and Giovanni Bacci and Anna Ing{\'{o}}lfsd{\'{o}}ttir and Axel Legay and Radu Mardare}, booktitle = {Models, Algorithms, Logics and Tools - Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday}, series = {Lecture Notes in Computer Science}, volume = {10460}, publisher = {Springer}, pages = {640--660}, doi = {10.1007/978-3-319-63121-9\_32}, ) @inproceedings(pek_verifying_2017, author = {C. Pek and P. Zahn and M. Althoff}, year = {2017}, title = {Verifying the safety of lane change maneuvers of self-driving vehicles based on formalized traffic rules}, booktitle = {2017 {IEEE} {Intelligent} {Vehicles} {Symposium} ({IV})}, pages = {1477--1483}, doi = {10.1109/IVS.2017.7995918}, ) @misc(philipp_safety_2019, author = {Robbel Philipp and David Wittmann and Christian Knobel and Jack Weast and Neil Garbacik and Philipp Schnetter}, year = {2019}, title = {Safety {First} for {Automated} {Driving}}, url = {https://newsroom.intel.com/news/intel-auto-industry-leaders-publish-new-automated-driving-safety-framework/}, ) @article(prakken_problem_2017, author = {Henry Prakken}, year = {2017}, title = {On the problem of making autonomous vehicles conform to traffic law}, journal = {Artificial Intelligence and Law}, volume = {25}, number = {3}, pages = {341--363}, doi = {10.1007/s10506-017-9210-0}, url = {https://link.springer.com/article/10.1007/s10506-017-9210-0}, ) @inproceedings(R11, author = {Aarne Ranta}, year = {2011}, title = {Translating between Language and Logic: What Is Easy and What Is Difficult}, editor = {Bj{\o}rner, Nikolaj and Sofronie{-}Stokkermans, Viorica}, booktitle = {Automated Deduction - {CADE-23} - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6803}, publisher = {Springer}, pages = {5--25}, doi = {10.1007/978-3-642-22438-6\_3}, ) @inproceedings(Retal17, author = {Albert Rizaldi and Jonas Keinholz and Monika Huber and Jochen Feldle and Fabian Immler and Matthias Althoff and Eric Hilgendorf and Tobias Nipkow}, year = {2017}, title = {Formalising and Monitoring Traffic Rules for Autonomous Vehicles in Isabelle/HOL}, editor = {Nadia Polikarpova and Steve A. Schneider}, booktitle = {Integrated Formal Methods - 13th International Conference, {IFM} 2017, Turin, Italy, September 20-22, 2017, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {10510}, publisher = {Springer}, pages = {50--66}, doi = {10.1007/978-3-319-66845-1\_4}, ) @article(Sch18-TCS, author = {Maike Schwammberger}, year = {2018}, title = {An abstract model for proving safety of autonomous urban traffic}, journal = {Theoretical Computer Science}, volume = {744}, pages = {143--169}, doi = {10.1016/j.tcs.2018.05.028}, ) @article(Sch18, author = {Maike Schwammberger}, year = {2018}, title = {Introducing Liveness into Multi-lane Spatial Logic lane change controllers using {UPPAAL}}, journal = {Electronic Proceedings in Theoretical Computer Science}, volume = {269}, pages = {17--31}, doi = {10.4204/EPTCS.269.3}, ) @phdthesis(Sch20-thesis, author = {Maike Schwammberger}, year = {2020}, title = {Distributed Controllers for Provably Safe, Live and Fair Autonomous Car Manoeuvres in Urban Traffic}, school = {University of Oldenburg}, url = {https://oops.uni-oldenburg.de/id/eprint/4961}, ) @inproceedings(WW07, author = {Bj{\"{o}}rn Wachter and Bernd Westphal}, year = {2007}, title = {The Spotlight Principle}, editor = {Byron Cook and Andreas Podelski}, booktitle = {Verification, Model Checking, and Abstract Interpretation, 8th International Conference, {VMCAI} 2007, Nice, France, January 14-16, 2007, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {4349}, publisher = {Springer}, pages = {182--198}, doi = {10.1007/978-3-540-69738-1\_13}, ) @book(WD96, author = {Jim Woodcock and Jim Davies}, year = {1996}, title = {Using Z -- Specification, Refinement, and Proof}, publisher = {Prentice Hall}, )