Home > Research > Publications & Outputs > Proof Theory of a Multi-Lane Spatial Logic

Links

Text available via DOI:

View graph of relations

Proof Theory of a Multi-Lane Spatial Logic

Research output: Contribution to Journal/MagazineJournal articlepeer-review

Published
Article number4
<mark>Journal publication date</mark>18/08/2015
<mark>Journal</mark>Logical Methods in Computer Science
Issue number3
Volume11
Number of pages27
Publication StatusPublished
<mark>Original language</mark>English

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.