@inproceedings(AN15,
 author       = {Yehia Abd Alrahman and De Nicola, Rocco and Michele Loreti and Francesco Tiezzi and Roberto Vigo},
 year         = {2015},
 title        = {A Calculus for Attribute-based Communication},
 booktitle    = {Proc. 30th Annual ACM Symp. on Applied Computing (SAC)},
 publisher    = {ACM},
 pages        = {1840--1845},
 doi          = {10.1145/2695664.2695668},
)
@article(AM16,
 author       = {Matthias Althoff and Silvia Magdici},
 year         = {2016},
 title        = {Set-Based Prediction of Traffic Participants on Arbitrary Road Networks},
 journal      = {{IEEE} Trans. Intelligent Vehicles},
 volume       = {1},
 number       = {2},
 pages        = {187--202},
 doi          = {10.1109/TIV.2016.2622920},
)
@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},
)
@article(An12,
 author       = {Mikael Asplund and Nadjm-Tehrani, Simin},
 year         = {2012},
 title        = {Worst-case Latency of Broadcast in Intermittently Connected Networks},
 journal      = {Int. J. Ad Hoc Ubiquitous Comput.},
 volume       = {11},
 number       = {2/3},
 pages        = {125--138},
 doi          = {10.1504/IJAHUC.2012.050281},
)
@inbook(BDL04,
 author       = {Gerd Behrmann and Alexandre David and Kim G. Larsen},
 year         = {2004},
 title        = {A Tutorial on Uppaal},
 pages        = {200--236},
 publisher    = {Springer Berlin Heidelberg},
 doi          = {10.1007/978-3-540-30080-9_7},
)
@article(BHLO17,
 author       = {Gregor v. Bochmann and Martin Hilscher and Sven Linker and Ernst-R{\"u}diger Olderog},
 year         = {2017},
 title        = {Synthesizing and verifying controllers for multi-lane traffic maneuvers},
 journal      = {Formal Aspects of Computing},
 volume       = {29},
 number       = {4},
 pages        = {583--600},
 doi          = {10.1007/s00165-017-0424-4},
)
@inbook(C05,
 author       = {Franck Cassez and Alexandre David and Emmanuel Fleury and Kim G. Larsen and Didier Lime},
 year         = {2005},
 title        = {Efficient On-the-Fly Algorithms for the Analysis of Timed Games},
 pages        = {66--80},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 doi          = {10.1007/11539452_9},
)
@article(DHO06,
 author       = {Werner Damm and Hardi Hungar and Ernst-R\IeC{\"u}diger Olderog},
 year         = {2006},
 title        = {Verification of Cooperating Traffic Agents},
 journal      = {International Journal of Control},
 volume       = {79},
 number       = {5},
 pages        = {395--421},
 doi          = {10.1080/00207170600587531},
)
@inproceedings(DMR14,
 author       = {Werner Damm and Eike M\"{o}hlmann and Astrid Rakow},
 year         = {2014},
 title        = {Component Based Design of Hybrid Systems: A Case Study on Concurrency and Coupling},
 booktitle    = {Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control},
 series       = {HSCC '14},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {145--150},
 doi          = {10.1145/2562059.2562120},
)
@inproceedings(FHO15,
 author       = {Martin Fr{\"a}nzle and Michael R. Hansen and Heinrich Ody},
 year         = {2015},
 title        = {No Need Knowing Numerous Neighbours},
 editor       = {Roland Meyer and Andr{\'e} Platzer and Heike Wehrheim},
 booktitle    = {Correct System Design},
 series       = {LNCS},
 volume       = {9360},
 publisher    = {Springer},
 pages        = {152--171},
 doi          = {10.1007/978-3-319-23506-6_11},
)
@inbook(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},
 pages        = {404--419},
 publisher    = {Springer Berlin Heidelberg},
 doi          = {10.1007/978-3-642-24559-6_28},
)
@incollection(HLO13,
 author       = {Martin Hilscher and Sven Linker and Ernst-R\IeC{\"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},
 series       = {LNCS},
 volume       = {8051},
 publisher    = {Springer},
 doi          = {10.1007/978-3-642-39698-4_12},
)
@inproceedings(HS16,
 author       = {Martin Hilscher and Maike Schwammberger},
 year         = {2016},
 title        = {An Abstract Model for Proving Safety of Autonomous Urban Traffic},
 editor       = {Augusto Sampaio and Farn Wang},
 booktitle    = {Theoretical Aspects of Computing (ICTAC)},
 series       = {LNCS},
 volume       = {9965},
 publisher    = {Springer},
 pages        = {274--292},
 doi          = {10.1007/978-3-319-46750-4_16},
)
@article(K11,
 author       = {J. B. Kenney},
 year         = {2011},
 title        = {Dedicated Short-Range Communications (DSRC) Standards in the United States},
 journal      = {Proceedings of the IEEE},
 volume       = {99},
 number       = {7},
 pages        = {1162--1182},
 doi          = {10.1109/JPROC.2011.2132790},
)
@article(K90,
 author       = {Ron Koymans},
 year         = {1990},
 title        = {Specifying real-time properties with metric temporal logic},
 journal      = {Real-Time Systems},
 volume       = {2},
 number       = {4},
 pages        = {255--299},
 doi          = {10.1007/BF01995674},
)
@phdthesis(L15,
 author       = {Sven Linker},
 year         = {2015},
 title        = {Proofs for Traffic Safety -- Combining Diagrams and Logic},
 school       = {University of Oldenburg},
)
@inproceedings(LP11,
 author       = {Sarah M. Loos and Andr{\'e} Platzer},
 year         = {2011},
 title        = {Safe Intersections: At the Crossing of Hybrid Systems and Verification},
 editor       = {Kyongsu Yi},
 booktitle    = {Intelligent Transportation Systems (ITSC)},
 pages        = {1181--1186},
 doi          = {10.1109/ITSC.2011.6083138},
)
@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(O15,
 author       = {Heinrich Ody},
 year         = {2015},
 title        = {Undecidability Results for Multi-Lane Spatial Logic},
 editor       = {Martin Leucker and Camilo Rueda and Frank D. Valencia},
 booktitle    = {Theoretical Aspects of Computing - {ICTAC}},
 series       = {LNCS},
 volume       = {9399},
 publisher    = {Springer},
 pages        = {404--421},
 doi          = {10.1007/978-3-319-25150-9_24},
)
@misc(O17,
 author       = {Heinrich Ody},
 year         = {2017},
 title        = {Monitoring of Traffic Manoeuvres with Imprecise Information},
 howpublished = {FVAV17},
)
@incollection(ORWprocos17,
 author       = {Ernst R{\"{u}}diger Olderog and Anders P. Ravn and Rafael Wisniewski},
 year         = {2017},
 title        = {Linking spatial and dynamic models, applied to traffic maneuvers},
 editor       = {M. Hinchey and J. P. Bowen and E.-R. Olderog},
 booktitle    = {Provably Correct Systems},
 series       = {NASA Monographs in SSE},
 publisher    = {Springer},
 pages        = {95--120},
 doi          = {10.1007/978-3-319-48628-4_5},
)
@misc(OS17,
 author       = {Ernst R{\"{u}}diger Olderog and Maike Schwammberger},
 year         = {Springer 2017, to appear},
 title        = {Formalising a Hazard Warning Communication Protocol with Timed Automata},
)
@inproceedings(RIA16,
 author       = {Albert Rizaldi and Fabian Immler and Matthias Althoff},
 year         = {2016},
 title        = {A Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles},
 booktitle    = {{NASA} Formal Methods -- 8th International Symposiuim},
 pages        = {175--190},
 doi          = {10.1007/978-3-319-40648-0_14},
)
@book(WD96,
 author       = {J. Woodcock and J. Davies},
 year         = {1996},
 title        = {Using Z -- Specification, Refinement, and Proof},
 publisher    = {Prentice Hall},
)
@inproceedings(XL16,
 author       = {Bingqing Xu and Qin Li},
 year         = {2016},
 title        = {A Spatial Logic for Modeling and Verification of Collision-Free Control of Vehicles},
 booktitle    = {21st ICECCS},
 pages        = {33--42},
 doi          = {10.1109/ICECCS.2016.014},
)