Open Access

Lucas Böltz

• The goal of this thesis is to use methods from automated reasoning to analyze graphs occurring in the context of wireless networks. For this a suitable representation of the considered graphs, the transformations and algorithms executed on the graphs and also the underlying geometric conditions are required. The considered graphs resp. classes of graphs in this thesis refer to a) graphs only defined by geometric conditions, b) graphs defined by more general axioms after applying transformations, c) graphs resulting from a graph transformation algorithm. For studying graphs in the context of wireless networks, an important task is the construction of graphs without intersecting edges. Such graphs are called plane graphs and have a wide range of applications, for example in routing procedures. For the construction of connected plane graphsThe goal of this thesis is to use methods from automated reasoning to analyze graphs occurring in the context of wireless networks. For this a suitable representation of the considered graphs, the transformations and algorithms executed on the graphs and also the underlying geometric conditions are required. The considered graphs resp. classes of graphs in this thesis refer to a) graphs only defined by geometric conditions, b) graphs defined by more general axioms after applying transformations, c) graphs resulting from a graph transformation algorithm. For studying graphs in the context of wireless networks, an important task is the construction of graphs without intersecting edges. Such graphs are called plane graphs and have a wide range of applications, for example in routing procedures. For the construction of connected plane graphs on a given set of vertices, the concepts of Gabriel graphs and relative neighborhood graphs exist. These concepts were originally developed for the Euclidean plane with Euclidean distance. In this thesis it is investigated, for which more general distance functions, Gabriel graphs, and relative neighborhood graphs are plane graphs, whenever possible by using the hierarchical prover HPiLoT. In addition to graph constructions, this thesis also examines graph transformations. A transformation is simple if the existence of an edge uv in the transformed graph depends only on the existence of the edges uv and vu in the underlying original graph. In the original graph, predicates determine which edges must exist, which edges must not exist, and which edges exist depending on the existence of other edges. It is investigated under which conditions for the predicates and for which transformations expressions can be found to automatically examine the containedness relation between two graph classes, whereby only graphs up to a certain number of vertices need to be considered. For the expressions found in this way, the containedness relations are evaluated for all possible graph classes using Mathematica. Graphs can also be transformed using algorithms instead of simple transformations. This thesis examines a planarization algorithm that generates a plane graph from an original graph by selecting a subset of edges. To maintain, in addition also the graph’s connectivity, the original graph must satisfy certain structural properties. Such properties are the redundancy and coexistence property. It is shown that for RCGs, i.e. graphs that satisfy these two properties, a connected plane subgraph always exists. To obtain this connected plane graph, the correctness of a local planarization algorithm for RCGs is proven by verifying the individual proof steps of a manual proof using the theorem prover Z3. To perform this verification, a suitable axiom system is defined that describes, the properties of the graphs, the properties required for the proof, as well as the underlying geometry.…
• Im Rahmen dieser Dissertation wird die Möglichkeit untersucht, Methoden des automatischen Beweisens für Graphen im Kontext von drahtlosen Netzwerken zu verwenden. Dafür müssen die Graphen, die betrachteten Transformationen bzw. Algorithmen, sowie geometrischen Eigenschaften, in einer geeigneten Weise beschrieben werden. Im Rahmen dieser Dissertation wurden a) rein geometrisch definierte Graphen, b) durch allgemeinere Axiome definierten Graphen nach dem anwenden einer simplen Transformation, sowie c) durch Graphtransformationsalgorithmen erzeugte Graphen untersucht. Eine wichtiges Ziel bei der Betrachtung von Graphen im Kontext von drahtlosen Netzwerken ist, die Konstruktion von Graphen ohne schneidene Kanten. Solche Graphen werden als ebene Graphen bezeichnet und haben vielfältige Anwendungsgebiete, zum Beispiel für Routingverfahren. FürIm Rahmen dieser Dissertation wird die Möglichkeit untersucht, Methoden des automatischen Beweisens für Graphen im Kontext von drahtlosen Netzwerken zu verwenden. Dafür müssen die Graphen, die betrachteten Transformationen bzw. Algorithmen, sowie geometrischen Eigenschaften, in einer geeigneten Weise beschrieben werden. Im Rahmen dieser Dissertation wurden a) rein geometrisch definierte Graphen, b) durch allgemeinere Axiome definierten Graphen nach dem anwenden einer simplen Transformation, sowie c) durch Graphtransformationsalgorithmen erzeugte Graphen untersucht. Eine wichtiges Ziel bei der Betrachtung von Graphen im Kontext von drahtlosen Netzwerken ist, die Konstruktion von Graphen ohne schneidene Kanten. Solche Graphen werden als ebene Graphen bezeichnet und haben vielfältige Anwendungsgebiete, zum Beispiel für Routingverfahren. Für die Konstruktion von zusammenhängenden ebenen Graphen auf einer gegebenen Knotenmengen existieren die Konzepte Gabriel-Graph und relativer Nachbarschaftsgraph. Diese ursprünglich für die euklidische Distanz konzipierten Graphen werden im Rahmen der Dissertation für allgemeineren Distanzfunktionen analysiert und dabei wird, sofern möglich, der hierarschische Beweiser HPiLoT verwendet. Neben Graphkonstruktionen werden in der Dissertation auch Transformationen auf Graphen betrachtet. Eine Transformation ist simpel, wenn die Existenz einer Kante uv im transformierten Graphen, nur von der Existenz der Kanten uv und vu im zugrundeliegenden ursprünglichen Graphen abhängt. Bedingungen für die Existenz von Kanten im zugrundeliegenden Graphen, werden mithilfe von Prädikaten axiomatisch beschrieben. Es wird untersucht, unter welchen Bedingungen für die Prädikate und für welche Transformationen Ausdrücke gefunden werden können, mit denen die Teilklassenbeziehung zwischen zwei Graphklassen automatisch untersucht werden kann, wobei nur Graphen bis zu einer gewissen Anzahl an Knoten betrachtet werden müssen. Für die so gefundenen Ausdrücke wird die Teilklassenbeziehung für alle möglichen Graphklassen mittels Mathematica ausgewertet. Eine weitere Möglichkeit Graphen in andere Graphen zu transformieren sind Algorithmen. Im Rahmen der Dissertation wird ein Planarisierungsalgorithmus, der aus einem Ursprungsgraphen einen ebenen Graphen durch Auswahl einer Teilmenge von Kanten erzeugt, betrachtet. Um gleichzeitig den Zusammenhang des Graphen beizubehalten, muss der Ursprungsgraph, gewisse strukturelle Eigenschaften erfüllen, z. B. die Redundanz- und Koexistenzeigenschaft. Es wird gezeigt, dass für Graphen, welche die Redundanz- und Koexistenzeigenschaft erfüllen, immer ein zusammenhängender ebener Teilgraph existiert. Um diesen zusammenhängenden ebenen Graphen zu erhalten, wird die Korrektheit eines lokalen Planarisierungsalgorithmus durch die Verifizierung der einzelnen Beweisschritte eines manuellen Beweises mit dem Theorembeweiser Z3 gezeigt. Um diese Verifizierung durchzuführen, wird zunächst ein geeignetes Axiomensystem definiert, das sowohl die zugrundeliegende Geometrie als auch die Eigenschaften der Graphen und für den Beweis benötigte Eigenschaften beschreibt.…