Spatial Reasoning About Motorway Traffic Safety with Isabelle/HOL

  • Sven LinkerEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10510)


Formal verification of autonomous vehicles on motorways is a challenging problem, due to the complex interactions between dynamical behaviours and controller choices of the vehicles. In previous work, we showed how an abstraction of motorway traffic, with an emphasis on spatial properties, can be beneficial. In this paper, we present a semantic embedding of a spatio-temporal multi-modal logic, specifically defined to reason about motorway traffic, into Isabelle/HOL. The semantic model is an abstraction of a motorway, emphasising local spatial properties, and parameterised by the types of sensors deployed in the vehicles. We use the logic to define controller constraints to ensure safety, i.e., the absence of collisions on the motorway. After proving safety with a restrictive definition of sensors, we relax these assumptions and show how to amend the controller constraints to still guarantee safety.


Spatial logic Isabelle Interactive theorem proving Motorway traffic Verification Safety 


  1. 1.
    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 CrossRefGoogle Scholar
  2. 2.
    Linker, S., Hilscher, M.: proof theory of a multi-lane spatial logic. LMCS 11 (2015)Google Scholar
  3. 3.
    Linker, S.: Proofs for traffic safety: combining diagrams and logic. Ph.D. thesis, University of Oldenburg (2015).
  4. 4.
    Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL–A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)zbMATHGoogle Scholar
  5. 5.
    Platzer, A., Quesel, J.-D.: KeYmaera: a hybrid theorem prover for hybrid systems (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 171–178. Springer, Heidelberg (2008). doi: 10.1007/978-3-540-71070-7_15 CrossRefGoogle Scholar
  6. 6.
    Loos, S.M., Platzer, A., Nistor, L.: Adaptive cruise control: hybrid, distributed, and now formally verified. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 42–56. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-21437-0_6 CrossRefGoogle Scholar
  7. 7.
    Platzer, A.: The complete proof theory of hybrid systems. In: LICS, pp. 541–550. IEEE (2012)Google Scholar
  8. 8.
    Rizaldi, A., Althoff, M.: Formalising traffic rules for accountability of autonomous vehicles. In: ITSC, pp. 1658–1665. IEEE (2015)Google Scholar
  9. 9.
    Kamali, M., Dennis, L.A., McAree, O., Fisher, M., Veres, S.M.: Formal verification of autonomous vehicle platooning. arXiv preprint arXiv:1602.01718 (2016)
  10. 10.
    Alur, R., Dill, D.L.: A theory of timed automata. TCS 126, 183–235 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Dennis, L.A., Fisher, M., Webster, M.P., Bordini, R.H.: Model checking agent programming languages. ASE 19, 5–63 (2012)Google Scholar
  12. 12.
    Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. STTT 1, 134–152 (1997)CrossRefzbMATHGoogle Scholar
  13. 13.
    Campbell, J., Tuncali, C.E., Liu, P., Pavlic, T.P., Ozguner, U., Fainekos, G.: Modeling concurrency and reconfiguration in vehicular systems: a \(\pi \)-calculus approach. In: CASE, pp. 523–530 IEEE (2016)Google Scholar
  14. 14.
    Alur, R.: Principles of Cyber-Physical Systems. MIT Press, Cambridge (2015)Google Scholar
  15. 15.
    Braüner, T.: Hybrid Logic and Its Proof-Theory. Springer, Netherlands (2010)zbMATHGoogle Scholar
  16. 16.
    Moszkowski, B.C.: A temporal logic for multilevel reasoning about hardware. Computer 18, 10–19 (1985)CrossRefGoogle Scholar
  17. 17.
    Benzmüller, C., Paulson, L.: Quantified multimodal logics in simple type theory. Log. Univers. 7, 7–20 (2013)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Bochmann, G.V., Hilscher, M., Linker, S., Olderog, E.R.: Synthesizing and verifying controllers for multi-lane traffic maneuvers. FAC 29, 583–600 (2017)MathSciNetGoogle Scholar
  19. 19.
    Olderog, E.-R., Ravn, A.P., Wisniewski, R.: Linking discrete and continuous models, applied to traffic manoeuvrers. In: Hinchey, M.G., Bowen, J.P., Olderog, E.-R. (eds.) Provably Correct Systems. NMSSE, pp. 95–120. Springer, Cham (2017). doi: 10.1007/978-3-319-48628-4_5 CrossRefGoogle Scholar
  20. 20.
    Hölzl, J.: Markov processes in Isabelle/HOL. In: CPP 2017, pp. 100–111. ACM (2017)Google Scholar
  21. 21.
    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 CrossRefGoogle Scholar
  22. 22.
    Hilscher, M., Schwammberger, M.: An abstract model for proving safety of autonomous urban traffic. In: Sampaio, A., Wang, F. (eds.) ICTAC 2016. LNCS, vol. 9965, pp. 274–292. Springer, Cham (2016). doi: 10.1007/978-3-319-46750-4_16 CrossRefGoogle Scholar
  23. 23.
    Xu, B., Li, Q.: A spatial logic for modeling and verification of collision-free control of vehicles. In: ICECCS, pp. 33–42. IEEE (2016)Google Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.Department of Computer ScienceUniversity of LiverpoolLiverpoolUK

Personalised recommendations