Sven Linker ; Martin Hilscher - Proof Theory of a Multi-Lane Spatial Logic

lmcs:1580 - Logical Methods in Computer Science, August 18, 2015, Volume 11, Issue 3 - https://doi.org/10.2168/LMCS-11(3:4)2015
Proof Theory of a Multi-Lane Spatial LogicArticle

Authors: Sven Linker ORCID; Martin Hilscher

    We extend the Multi-lane Spatial Logic MLSL, introduced in previous work for proving the safety (collision freedom) of traffic maneuvers on a multi-lane highway, by length measurement and dynamic modalities. We investigate the proof theory of this extension, called EMLSL. To this end, we prove the undecidability of EMLSL but nevertheless present a sound proof system which allows for reasoning about the safety of traffic situations. We illustrate the latter by giving a formal proof for the reservation lemma we could only prove informally before. Furthermore we prove a basic theorem showing that the length measurement is independent from the number of lanes on the highway.


    Volume: Volume 11, Issue 3
    Published on: August 18, 2015
    Submitted on: February 14, 2014
    Keywords: Computer Science - Logic in Computer Science

    14 Documents citing this article

    Consultation statistics

    This page has been seen 1112 times.
    This article's PDF has been downloaded 479 times.