Proof Theory of a Multi-Lane Spatial Logic
Abstract
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.
Keywords
Cite
@article{arxiv.1504.06986,
title = {Proof Theory of a Multi-Lane Spatial Logic},
author = {Sven Linker and Martin Hilscher},
journal= {arXiv preprint arXiv:1504.06986},
year = {2017}
}
Comments
This paper is the extended and slightly revised version of our publication in the 10th International Colloquium on Theoretical Aspects of Computing (ICTAC) in 2013