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

lmcs:1580 - Logical Methods in Computer Science, August 18, 2015, Volume 11, Issue 3
Proof Theory of a Multi-Lane Spatial Logic

Authors: Linker, Sven and Hilscher, Martin

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.


Source : oai:arXiv.org:1504.06986
DOI : 10.2168/LMCS-11(3:4)2015
Volume: Volume 11, Issue 3
Published on: August 18, 2015
Submitted on: February 14, 2014
Keywords: Computer Science - Logic in Computer Science


Share

Consultation statistics

This page has been seen 112 times.
This article's PDF has been downloaded 46 times.