Home > Research > Publications & Outputs > Proofs for Traffic Safety

Research

Associated organisational unit

View graph of relations

Proofs for Traffic Safety: Combining Diagrams and Logic

Research output: Thesis › Doctoral Thesis

Published

Standard

Proofs for Traffic Safety: Combining Diagrams and Logic. / Linker, Sven.
2015.

Research output: Thesis › Doctoral Thesis

Harvard

Linker, S 2015, 'Proofs for Traffic Safety: Combining Diagrams and Logic', PhD, Carl von Ossietzky University of Oldenburg.

APA

Linker, S. (2015). Proofs for Traffic Safety: Combining Diagrams and Logic. [Doctoral Thesis, Carl von Ossietzky University of Oldenburg].

Vancouver

Linker S. Proofs for Traffic Safety: Combining Diagrams and Logic. 2015.

Author

Linker, Sven. / Proofs for Traffic Safety : Combining Diagrams and Logic. 2015.

Bibtex

@phdthesis{40c951921e18491a81e90b23ea5825ac,
title = "Proofs for Traffic Safety: Combining Diagrams and Logic",
abstract = "Due to the increasing interest in autonomously driving cars, safety issues of such systems are of utmost importance. Safety in this sense is primarily the absence of collisions, which is inherently a spatial property. Within computer science, typical models of cars include specifications of their behaviour, where the space a car needs for operating safely is a function of time. This complicates proofs of safety properties tremendously. In this thesis, we present methods to separate reasoning on space from the dynamical behaviour of cars. To that end, we define an abstract model with an emphasis on spatial transformations of the situation on the road. Based on this model, we develop two formalisms: We give the definitions of a modal logic suited to reason about safety properties of arbitrarily many cars. Furthermore, we present a diagrammatic language to ease the specification of such properties. We formally prove that no collisions arise between cars obeying a small set of requirements.",
author = "Sven Linker",
year = "2015",
language = "English",
school = "Carl von Ossietzky University of Oldenburg",

}

RIS

TY - BOOK

T1 - Proofs for Traffic Safety

T2 - Combining Diagrams and Logic

AU - Linker, Sven

PY - 2015

Y1 - 2015

N2 - Due to the increasing interest in autonomously driving cars, safety issues of such systems are of utmost importance. Safety in this sense is primarily the absence of collisions, which is inherently a spatial property. Within computer science, typical models of cars include specifications of their behaviour, where the space a car needs for operating safely is a function of time. This complicates proofs of safety properties tremendously. In this thesis, we present methods to separate reasoning on space from the dynamical behaviour of cars. To that end, we define an abstract model with an emphasis on spatial transformations of the situation on the road. Based on this model, we develop two formalisms: We give the definitions of a modal logic suited to reason about safety properties of arbitrarily many cars. Furthermore, we present a diagrammatic language to ease the specification of such properties. We formally prove that no collisions arise between cars obeying a small set of requirements.

AB - Due to the increasing interest in autonomously driving cars, safety issues of such systems are of utmost importance. Safety in this sense is primarily the absence of collisions, which is inherently a spatial property. Within computer science, typical models of cars include specifications of their behaviour, where the space a car needs for operating safely is a function of time. This complicates proofs of safety properties tremendously. In this thesis, we present methods to separate reasoning on space from the dynamical behaviour of cars. To that end, we define an abstract model with an emphasis on spatial transformations of the situation on the road. Based on this model, we develop two formalisms: We give the definitions of a modal logic suited to reason about safety properties of arbitrarily many cars. Furthermore, we present a diagrammatic language to ease the specification of such properties. We formally prove that no collisions arise between cars obeying a small set of requirements.

UR - http://oops.uni-oldenburg.de/2337/

M3 - Doctoral Thesis

ER -