Tobias Nipkow
2017-11-09 11:02:56 UTC
Hybrid Multi-Lane Spatial Logic
Sven Linker
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.
https://www.isa-afp.org/entries/Hybrid_Multi_Lane_Spatial_Logic.html
Enjoy!
Sven Linker
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.
https://www.isa-afp.org/entries/Hybrid_Multi_Lane_Spatial_Logic.html
Enjoy!