Abstract
The specification of Multi-lane Spatial Logic (MLSL) was introduced in [1, 2] for proving safety (collision freedom) on multi-lane motorways and country roads. We now consider an extension of MLSL to deal with urban traffic scenarios, thereby focusing on crossing manoeuvres at intersections. To this end, we modify the existing abstract model by introducing a generic topology of urban traffic networks. We then show that even at intersections we can use purely spatial reasoning, detached from the underlying car dynamics, to prove safety of controllers modelled as extended timed automata.
This research was partially supported by the German Research Council (DFG) in the Transregional Collaborative Research Center SFB/TR 14 AVACS.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Hilscher, M., Linker, S., Olderog, E.-R., Ravn, A.P.: An abstract model for proving safety of multi-lane traffic manoeuvres. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 404–419. Springer, Heidelberg (2011). doi:10.1007/978-3-642-24559-6_28
Hilscher, M., Linker, S., Olderog, E.-R.: Proving safety of traffic manoeuvres on country roads. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 196–212. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39698-4_12
Moszkowski, B.: A temporal logic for multilevel reasoning about hardware. Computer 18, 10–19 (1985)
Zhou, C., Hoare, C., Ravn, A.: A calculus of durations. Inf. Process. Lett. 40, 269–276 (1991)
Schäfer, A.: A calculus for shapes in time and space. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 463–477. Springer, Heidelberg (2005). doi:10.1007/978-3-540-31862-0_33
Loos, S.M., Platzer, A.: Safe intersections: at the crossing of hybrid systems and verification. In: Yi, K. (ed.) Intelligent Transportation Systems (ITSC), pp. 1181–1186. Springer, Heidelberg (2011)
Werling, M., Gindele, T., Jagszent, D., Gröll, L.: A robust algorithm for handling moving traffic in urban scenarios. In: Proceedings of IEEE Intelligent Vehicles Symposium, Eindhoven, The Netherlands, pp. 168–173 (2008)
Colombo, A., Del Vecchio, D.: Efficient algorithms for collision avoidance at intersections. In: Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2012, pp. 145–154. ACM, New York (2012)
Alur, R., Dill, D.: A theory of timed automata. TCS 126, 183–235 (1994)
Woodcock, J., Davies, J.: Using Z - Specification, Refinement, and Proof. Prentice Hall, Upper Saddle River (1996)
Linker, S., Hilscher, M.: Proof theory of a multi-lane spatial logic. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) ICTAC 2013. LNCS, vol. 8049, pp. 231–248. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39718-9_14
Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004). doi:10.1007/978-3-540-30080-9_7
Damm, W., Hungar, H., Olderog, E.R.: Verification of cooperating traffic agents. Int. J. Control 79, 395–421 (2006)
Damm, W., Möhlmann, E., Rakow, A.: Component based design of hybrid systems: a case study on concurrency and coupling. In: Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, pp. 145–150. ACM (2014)
Olderog, E., Ravn, A.P., Wisniewski, R.: Linking spatial and dynamic models for traffic maneuvers. In: 54th IEEE Conference on Decision and Control, CDC 2015, Osaka, Japan, pp. 6809–6816, 15–18 December 2015
Linker, S.: Proofs for Traffic Safety - Combining Diagrams and Logic. Ph.d thesis, University of Oldenburg (2015)
Fränzle, M., Hansen, M.R., Ody, H.: No need knowing numerous neighbours. In: Meyer, R., Platzer, A., Wehrheim, H. (eds.) Correct System Design. LNCS, vol. 9360, pp. 152–171. Springer, Heidelberg (2015). doi:10.1007/978-3-319-23506-6_11
Alrahman, Y.A., De Nicola, R., Loreti, M., Tiezzi, F., Vigo, R.:A calculus for attribute-based communication. In: Proceedings of the 30th Annual ACM Symposium on Applied Computing, SAC 2015, pp. 1840–1845. ACM, New York (2015)
Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science, SFCS 1977, Washington, DC, USA, pp. 46–57. IEEE Computer Society (1977)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Hilscher, M., Schwammberger, M. (2016). An Abstract Model for Proving Safety of Autonomous Urban Traffic. In: Sampaio, A., Wang, F. (eds) Theoretical Aspects of Computing – ICTAC 2016. ICTAC 2016. Lecture Notes in Computer Science(), vol 9965. Springer, Cham. https://doi.org/10.1007/978-3-319-46750-4_16
Download citation
DOI: https://doi.org/10.1007/978-3-319-46750-4_16
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-46749-8
Online ISBN: 978-3-319-46750-4
eBook Packages: Computer ScienceComputer Science (R0)