### Abstract

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.

### License

BSD License

### Topics

- Logic/General logic/Modal logic

### Session Hybrid_Multi_Lane_Spatial_Logic

- NatInt
- RealInt
- Cars
- Traffic
- Views
- Restriction
- Move
- Sensors
- Length
- HMLSL
- Perfect_Sensors
- HMLSL_Perfect
- Safety_Perfect
- Regular_Sensors
- HMLSL_Regular
- Safety_Regular

## Cite

×

Hybrid_Multi_Lane_Spatial_Logic-AFP

    @article{Hybrid_Multi_Lane_Spatial_Logic-AFP,
      author  = {Sven Linker},
      title   = {Hybrid Multi-Lane Spatial Logic},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/Hybrid_Multi_Lane_Spatial_Logic.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Nov 9, 2017 : Isabelle2017