@article(ackerman2013,
 author       = {E. Ackerman},
 year         = {2013},
 title        = {{NASA} Lets Curiosity Rover Loose on {M}ars in Autonomous Driving Mode},
 journal      = {{IEEE} Spectrum},
 note         = {Retrieved from \url{https://spectrum.ieee.org/nasa-mars-curiosity-rover-autonomous-driving-mode}},
)
@article(ackerman2021,
 author       = {E. Ackerman},
 year         = {2021},
 title        = {Everything You Need to Know About {NASA}'s Perseverance Rover Landing on {M}ars},
 journal      = {{IEEE} Spectrum},
 note         = {Retrieved from \url{https://spectrum.ieee.org/nasa-mars-rover-perseverance-landing}},
)
@article(alnuwiquaive2021,
 author       = {{Al-Nuaimi}, M. and S. Wibowo and H. Qu and J. Aitken and S. Veres},
 year         = {2021},
 title        = {Hybrid Verification Technique for Decision-Making of Self-Driving Vehicles},
 journal      = {Journal of Sensor and Actuator Networks},
 volume       = {10},
 number       = {42},
 doi          = {10.3390/jsan10030042},
)
@inproceedings(aldsugyon2016,
 author       = {M. {Aldibaja} and N. {Suganuma} and K. {Yoneda}},
 year         = {2016},
 title        = {Improving localization accuracy for autonomous driving in snow-rain environments},
 booktitle    = {2016 {IEEE/SICE} International Symposium on System Integration ({SII})},
 pages        = {212--217},
 doi          = {10.1109/SII.2016.7844000},
)
@article(Althoff2014,
 author       = {M. Althoff and J. M. Dolan},
 year         = {2014},
 title        = {Online verification of automated road vehicles using reachability analysis},
 journal      = {{IEEE} Transactions on Robotics},
 volume       = {30},
 number       = {4},
 pages        = {903--918},
 doi          = {10.1109/TRO.2014.2312453},
)
@article(Althoff2011,
 author       = {M. Althoff and A. Mergel},
 year         = {2011},
 title        = {{Comparison of Markov chain abstraction and Monte Carlo simulation for the safety assessment of autonomous cars}},
 journal      = {{IEEE} Transactions on Intelligent Transportation Systems},
 volume       = {12},
 number       = {4},
 pages        = {1237--1247},
 doi          = {10.1109/TITS.2011.2157342},
)
@article(Althoff2009,
 author       = {M. Althoff and O. Stursberg and M. Buss},
 year         = {2009},
 title        = {Model-based probabilistic collision detection in autonomous driving},
 journal      = {{IEEE} Transactions on Intelligent Transportation Systems},
 volume       = {10},
 number       = {2},
 pages        = {299--310},
 doi          = {10.1109/TITS.2009.2018966},
)
@book(baier,
 author       = {C. Baier and {J.-P.} Katoen},
 year         = {2008},
 title        = {Principles of Model Checking},
 publisher    = {The {MIT} Press},
)
@inproceedings(Clarke2001,
 author       = {E. M. Clarke and O. Grumberg and S. Jha and Y. Lu and H. Veith},
 year         = {2001},
 title        = {Progress on the State Explosion Problem in Model Checking},
 booktitle    = {Informatics - 10 Years Back. 10 Years Ahead.},
 series       = {Lecture Notes in Computer Science},
 volume       = {2000},
 publisher    = {Springer-Verlag},
 address      = {Berlin, Heidelberg},
 pages        = {176\IeC{\textendash}194},
 doi          = {10.1006/inco.1997.2696},
)
@book(clagrpe99,
 author       = {{E. M. Jnr} Clarke and O. Grumberg and {D. A.} Peled},
 year         = {1999},
 title        = {Model Checking},
 publisher    = {{MIT} Press},
)
@article(conger2020,
 author       = {K. Conger},
 year         = {2020},
 title        = {Driver Charged in Uber\IeC{\textquoteright}s Fatal 2018 Autonomous Car Crash},
 journal      = {The New York Times},
)
@inproceedings(damopera2018,
 author       = {W. Damm and M{\" o}hlmann, E. and T. Peikenkamp},
 year         = {2018},
 title        = {A Formal Semantics for Traffic Sequence Charts},
 booktitle    = {Principles of Modeling},
 series       = {Lecture Notes in Computing Science},
 publisher    = {Springer},
 pages        = {188--205},
 doi          = {10.1002/spe.1038},
)
@article(defiwebor2012,
 author       = {L. Dennis and M. Fisher and M. Webster and R. Bordini},
 year         = {2012},
 title        = {Model Checking Agent Programming Languages},
 journal      = {Automated Software Engineering},
 volume       = {19},
 number       = {1},
 pages        = {5--63},
 doi          = {10.1007/s10515-011-0088-x},
)
@article(deo2018,
 author       = {N. Deo and {M. M.} Trivedi},
 year         = {2018},
 title        = {Convolutional Social Pooling for Vehicle Trajectory Prediction},
 journal      = {CoRR},
 volume       = {abs/1805.06771},
)
@book(dijkstra76,
 author       = {E. W. Dijkstra},
 year         = {1976},
 title        = {A Discipline of Programming},
 publisher    = {Prentice-Hall},
)
@article(fecualfi2017,
 author       = {L. E. R. Fernandes and V. Custodio and G. V. Alves and M. Fisher},
 year         = {2017},
 title        = {A Rational Agent Controlling an Autonomous Vehicle: Implementation and Formal Verification},
 journal      = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {257},
 pages        = {35\IeC{\textendash}42},
 doi          = {10.1007/978-94-015-9204-8},
)
@article(frgihoirmino2020,
 author       = {D. Fraser and R. Giaquinta and Hoffmann and M. Ireland and A. Miller and G. Norman},
 year         = {2020},
 title        = {Collaborative models for autonomous systems controller synthesis},
 journal      = {Form Aspects of Computing},
 volume       = {32},
 pages        = {157\IeC{\textendash}--186},
 doi          = {10.1109/TCST.2006.872519},
)
@article(harris2018,
 author       = {M. Harris},
 year         = {2018},
 title        = {Waymo Filings Give New Details on Its Driverless Taxis},
 journal      = {{IEEE} Spectrum},
 note         = {Retrieved from \url{https://spectrum.ieee.org/waymo-filings-give-new-details-on-its-driverless-taxis}},
)
@article(Havelund2001-3,
 author       = {K. Havelund and M. Lowry and J. Penix},
 year         = {2001},
 title        = {Formal Analysis of a Space-Craft Controller Using SPIN.},
 journal      = {Software Engineering, IEEE Transactions on},
 volume       = {27},
 pages        = {749--765},
 doi          = {10.1109/32.940728},
)
@inproceedings(hiliol2013,
 author       = {M. Hilsher and S. Linker and {E-R} Olderog},
 year         = {2013},
 title        = {Proving Safety of Traffic Manoeuvres on Country Roads},
 booktitle    = {Theories of Programming and Formal Methods},
 series       = {Lecture Notes in Computing Science},
 publisher    = {Springer},
 pages        = {196--212},
 doi          = {10.1007/978-3-642-39698-4_12},
)
@book(holz2011,
 author       = {G. Holzmann},
 year         = {2011},
 title        = {The {SPIN} Model Checker: Primer and Reference Manual},
 edition      = {1st},
 publisher    = {Addison-Wesley Professional},
)
@article(hsu2019,
 author       = {J. Hsu},
 year         = {2016},
 title        = {{U.S.} Navy's Drone Boat Swarm Practices Harbor Defense},
 journal      = {{IEEE} Spectrum},
 note         = {Retrieved from \url{https://spectrum.ieee.org/navy-drone-boat-swarm-practices-harbor-defense}},
)
@article(Ji2017,
 author       = {J. Ji and A. Khajepour and W. M. Melek and Y. Huang},
 year         = {2017},
 title        = {{Path planning and tracking for vehicle collision avoidance based on model predictive control with multiconstraints}},
 journal      = {{IEEE} Transactions on Vehicular Technology},
 volume       = {66},
 number       = {2},
 pages        = {952--964},
 doi          = {10.1109/TVT.2016.2555853},
)
@article(Josef2020,
 author       = {S. Josef and A. Degani},
 year         = {2020},
 title        = {Deep Reinforcement Learning for Safe Local Planning of a Ground Vehicle in Unknown Rough Terrain},
 journal      = {IEEE Robotics and Automation Letters},
 volume       = {5},
 number       = {4},
 pages        = {6748--6755},
 doi          = {10.1109/LRA.2020.3011912},
)
@article(kademcfive2017,
 author       = {M. Kamali and L. Dennis and O. {McAcree} and M. Fisher and S. Veres},
 year         = {2017},
 title        = {Formal Verification of autonomous vehicle platooning},
 journal      = {Science of Computer Programming},
 volume       = {148},
 pages        = {88--106},
 doi          = {10.1016/j.scico.2017.05.006},
)
@article(Kavanagh2019,
 author       = {W. J. Kavanagh and A. Miller and G. Norman and O. Andrei},
 year         = {2021},
 title        = {Balancing Turn-Based Games with Chained Strategy Generation},
 journal      = {IEEE Transactions on Games},
 volume       = {13},
 number       = {2},
 pages        = {113--122},
 doi          = {10.1109/TG.2019.2943227},
)
@article(Kinder2010,
 author       = {J. Kinder and S. Katzenbeisser and C. Schallhart and H. Veith},
 year         = {2010},
 title        = {Proactive detection of computer worms using model checking},
 journal      = {IEEE Transactions on Dependable and Secure Computing},
 volume       = {7},
 number       = {4},
 pages        = {424--438},
 doi          = {10.1109/TDSC.2008.74},
)
@article(Kroll2017,
 author       = {Joshua Kroll and Joanna Huey and Solon Barocas and Edward Felten and Joel Reidenberg and David Robinson and Harlan Yu},
 year         = {2017},
 title        = {Accountable algorithms},
 journal      = {University of Pennsylvania Law Review},
 volume       = {165},
 pages        = {633--705},
)
@inproceedings(kwiatkowska,
 author       = {M. Kwiatkowska and G. Norman and D. Parker},
 year         = {2011},
 title        = {{PRISM} 4.0: Verification of Probabilistic Real-Time Systems},
 booktitle    = {Computer Aided Verification ({CAV}'2011)},
 series       = {Lecture Notes in Computer Science},
 volume       = {6806},
 publisher    = {Springer},
 pages        = {585--591},
 doi          = {10.1007/3-540-45657-0_17},
)
@article(lapeyi97,
 author       = {K. Larsen and P. Pettersson and W. Yi},
 year         = {1997},
 title        = {\sc{uppaal} in a nutshell},
 journal      = {Software Tools for Technology Transfer},
 pages        = {134--152},
 doi          = {10.1007/s100090050010},
)
@article(li2016,
 author       = {X. Li and Z. Sun and D. Cao and Z. He and Q. Zhu},
 year         = {2016},
 title        = {Real-time trajectory planning for autonomous urban driving: Framework, algorithms, and verifications},
 journal      = {{IEEE/ASME} Transactions on Mechatronics},
 volume       = {21},
 number       = {2},
 pages        = {740--753},
 doi          = {10.1109/TMECH.2015.2493980},
)
@article(Lillicrap2016,
 author       = {T. Lillicrap and J. Hunt and A. Pritzel and N. Heess and T. Erez and Y. Tassa and D. Silver and D. Wierstra},
 year         = {2016},
 title        = {Continuous control with deep reinforcement learning},
 journal      = {CoRR},
 volume       = {abs/1509.02971},
)
@inproceedings(loqura2009,
 author       = {A. Lomuscio and H. Qu and F. Raimondi},
 year         = {2009},
 title        = {a model checker for the verification of multi-agent systems},
 booktitle    = {Proceedings of the International Conference on Computer Aided Verification},
 publisher    = {Springer},
 pages        = {682--688},
 doi          = {10.1109/ICMAS.2000.858426},
)
@inproceedings(lu2015,
 author       = {Y. Lu and A. Miller and C. Johnson and Z. Peng and T. Zhao},
 year         = {2014},
 title        = {Availability analysis of satellite positioning systems for avaiation using the {P}rism model checker},
 booktitle    = {Proceedings of the 17th International Conference on Computational Science and Engineering ({CSE} 2014)},
 pages        = {704--713},
 doi          = {10.1109/CSE.2014.148},
)
@article(Marcus2020,
 author       = {G. Marcus and E. Davis},
 year         = {2020},
 title        = {{GPT}-3 bloviator: {OpenAI}\IeC{\textquoteright}s language generator has no idea what it\IeC{\textquoteright}s talking about},
 journal      = {MIT Technology Review},
 url          = {https://www.technologyreview.com/2020/08/22/1007539},
)
@article(Mnih2015,
 author       = {V. Mnih and K. Kavukcuoglu and D. Silver and A. A. Rusu and J. Veness and M. G. Bellemare and A. Graves and M. Riedmiller and A. K. Fidjeland and G. Ostrovski and S. Petersen and C. Beattie and A. Sadik and I. Antonoglou and H. King and D. Kumaran and D. Wierstra and S. Legg and D. Hassabis},
 year         = {2015},
 title        = {Human-level control through deep reinforcement learning},
 journal      = {Nature},
 volume       = {518},
 number       = {7540},
 pages        = {529--533},
 doi          = {10.1016/S0004-3702(98)00023-X},
)
@misc(Pagojus2021,
 author       = {D. Pagojus and A. Miller and B. Porr and I. Valkov},
 year         = {2021},
 title        = {Simulation and Model checking for close to real-time overtaking planning},
 howpublished = {github},
 doi          = {10.5281/zenodo.5543845},
 note         = {GitHub repository},
)
@article(pnueli81,
 author       = {A. Pnueli},
 year         = {1981},
 title        = {The temporal semantics of concurrent programs},
 journal      = {Theoretical Computer Science},
 volume       = {13},
 number       = {1},
 pages        = {45--60},
 doi          = {10.1016/0304-3975(81)90110-9},
)
@article(Prokop2001,
 author       = {G. Prokop},
 year         = {2001},
 title        = {Modeling human vehicle driving by model predictive online optimization},
 journal      = {Vehicle System Dynamics},
 volume       = {35},
 number       = {1},
 pages        = {19--53},
 doi          = {10.1076/vesd.35.1.19.5614},
)
@article(Rasekhipour2017,
 author       = {Y. Rasekhipour and A. Khajepour and S. K. Chen and B. Litkouhi},
 year         = {2017},
 title        = {{A Potential Field-Based Model Predictive Path-Planning Controller for Autonomous Road Vehicles}},
 journal      = {{IEEE} Transactions on Intelligent Transportation Systems},
 volume       = {18},
 number       = {5},
 pages        = {1255--1267},
 doi          = {10.1109/TITS.2016.2604240},
)
@book(Sutton98,
 author       = {R. S. Sutton and A. G. Barto},
 year         = {1998},
 title        = {Reinforcement Learning: {An Introduction}},
 edition      = {2002},
 publisher    = {Bradford Books, MIT Press},
 address      = {Cambridge, MA},
)
@article(visser2003,
 author       = {W. Visser and K. Havelund and G. Brat and S Park and F. Lerda},
 year         = {2003},
 title        = {Model checking programs},
 journal      = {Automated Software Engineering},
 volume       = {10},
 pages        = {203--232},
 doi          = {10.1023/A:1022920129859},
)
@article(Wang2018,
 author       = {L. Wang and F. Cai},
 year         = {2017},
 title        = {{Reliability analysis for flight control systems using probabilistic model checking}},
 journal      = {Proceedings of the {IEEE} International Conference on Software Engineering and Service Sciences, {ICSESS}},
 volume       = {2017-Novem},
 pages        = {161--164},
 doi          = {10.1109/RAM.2017.7889773},
)
@article(Wang2019,
 author       = {Q. Wang and B. Ayalew and T. Weiskircher},
 year         = {2019},
 title        = {{Predictive Maneuver Planning for an Autonomous Vehicle in Public Highway Traffic}},
 journal      = {{IEEE} Transactions on Intelligent Transportation Systems},
 volume       = {20},
 number       = {4},
 pages        = {1303--1315},
 doi          = {10.1109/TITS.2018.2848472},
)
@article(yadron2016,
 author       = {D. Yadron and D. Tynan},
 year         = {2016},
 title        = {Tesla driver dies in first fatal crash while using autopilot mode},
 journal      = {The Guardian},
 note         = {Retrieved from \url{https://www.theguardian.com/technology/2016/jun/30/tesla-autopilot-death-self-driving-car-elon-musk}},
)
@inproceedings(Yu2020,
 author       = {T. Yu and G. Thomas and L. Yu and S. Ermon and J. Y. Zou and S. Levine and C. Finn and T. Ma},
 year         = {2020},
 title        = {{MOPO}: Model-based Offline Policy Optimization},
 booktitle    = {Advances in Neural Information Processing Systems},
 volume       = {33},
 publisher    = {Curran Associates, Inc.},
 pages        = {14129--14142},
)