Project

General

Profile

OGM » batman-v5-beweis.tex

Linus Lüssing, 05/15/2011 07:42 AM

 
1
\documentclass[a4paper,10pt]{scrartcl}[2003/01/01] %europäische article-version
2
\usepackage{fullpage}   % weniger Ränder (1cm?)
3
\usepackage[ngerman]{babel}
4
\usepackage{amssymb}    % mathematische Symbole
5
\usepackage{tabularx}   % für Tabellen mit \begin{tabular}
6
\usepackage{amsmath}    % mathematische Formeln
7
\usepackage{textcomp}   % für das copyleft-Zeichen
8
%\usepackage[all]{xy}    % z.B.  für das Zeichnen von Graphen
9
\usepackage{stmaryrd}   % für das Blitz-Symbol (stmaryrd in texlive-math-extra)
10
%\usepackage{listings}  % Anzeige von formatiertem Programmiercode
11
%\lstset{language=bash}
12
%\usepackage{uniinput}
13
\usepackage[T1]{fontenc}
14
\usepackage[utf8]{inputenc}
15
\title{BATMAN V - Beweis zur Kreisfreiheit}
16
\author{Linus Lüssing}
17
\date{\textcopyleft\today}
18
\begin{document}
19
\maketitle
20

    
21
\emph{WIP - WIP - WIP - WIP} \\
22
Bin noch kein Experte in Graphentheorie und das Dokument hier hat sicherlich noch
23
ein paar kleinere Lücken. Ist also sicherlich sowohl inhaltlich als auch stilistisch
24
noch weit von einer Perfektion entfernt :) (hab' aber zumindest versucht mich nach dem
25
Notationsstil von ''Graphentheorie, R. Diestel'' zu richten. Hoffe aber, dass die Hauptargumentationsgründe
26
drin enthalten sind, warum BATMAN V kreisfreie Routingentscheidungen trifft und das
27
diese Gründe nützlich sein können zur Prüfung und Validierung jeder Änderung am
28
Routingprotokoll. Wenn eine Änderung des Routingprotokolls die OGM-Forwarding-Regeln (i), (ii) nicht verletzt,
29
und sichergestellt ist, das weiterhin nur in den Fällen (a) oder (b) die Route geändert wird,
30
dann sollte (TM) BATMAN weiterhin Kreisfreiheit garantieren können.
31

    
32
\newpage
33

    
34
Wir wollen zeigen, dass für eine beliebige Topologie und zu einer beliebigen Zeit
35
BATMAN V kreisfrei ist. \\
36

    
37
\section*{Definitionen}
38

    
39
Sei G = (V,A) der gerichtete, gewichtete Graph der die Topologie zu einem
40
bestimmten Zeitpunkt darstellt. \\
41

    
42
Sei ferner $T = (V,E) \subseteq G$ ein von BATMAN V ermittelter Graph für einen Knoten
43
r (alias 'Originator'). \\
44

    
45
T ist schlicht, da keine Mehrfachkanten (verschiedene Kanten alias 'Links'
46
werden zwischen NDP und OGM Protokoll vorher abstrahiert) sowie Schlingen
47
(ein Knoten wählt sich nie selbst als nächsten Router, er erkennt
48
und verwirft seine selbst gerebroadcasteten OGMs). \\
49

    
50
$v_c \in V(G)$ ist ein Knoten der zu einem bestimmten Zeitpunkt eine OGM erhält
51
und nun entscheiden muss, ob er seine Route zum entsprechenden Originator-Knoten r
52
ändern müsse. \\
53

    
54
Eine OGM ist ein Tupel der Form OGM = (seqno, TQ, r, n) wobei n der Nachbar ist,
55
von dem die OGM empfangen wurde ($nv_c \in E(G)$). \\
56
Da ein Knoten eine OGM nur von einem Nachbarn, den es selbst als Router zum Knoten
57
r ausgewhält hat, rebroadcasted, gilt außerdem $n \in T$. \\
58

    
59
Wir können die Routen-Änderung durch BATMAN V darstellen als eine Abbildung der Form: \\
60
$f: \{T\} \times \{OGM\} \rightarrow \{T\}$ für die gilt: \\
61

    
62
$f(T, OGM) = \left\{ \begin{array}{rcl} T - v_{c-1}v_c + nv_c & \mbox{für} & ((a) \vee (b)) \wedge (x) \\
63
					T & \mbox{sonst} & \end{array} \right.$ \\
64

    
65
Mit: \\
66
$(a) \Leftrightarrow seqno(OGM) > seqno(v_c)$ ($seqno(v_c)$ ist die Sequenznummer des aktuell gewählten Routers) \\
67
$(b) \Leftrightarrow seqno(OGM) = seqno(v_c) \wedge TQ(OGM) > TQ(v_c)$ ($TQ(v_c)$ ist die Path-TQ des aktuell gewählten Routers) \\
68
$(x)$: Ein beliebiges Kriterium, dass einen Routenwechsel verhindern können wolle. \\
69

    
70
Außerdem gewährleistet BATMAN V die folgenden zwei Kriterien: \\
71
(i): Sequenznummern-Konsistenz: Sequenznummern einer OGM werden nicht erhöht (und auch garnicht verändert) zwischen
72
dem Originator und einem beliebigen anderen Knoten. \\
73
(ii): Path-TQ Monotonie: Die path TQ einer OGM sinkt mit jedem rebroadcast. Anders gesagt, die Kosten
74
einer OGM und des zugehörigen Pfades sind strikt monoton steigend. \\
75

    
76
TQ ist definiert als: $TQ = 1 / \text{cost(P)}$ für einen gerichteten Weg P (oder auch für eine gerichtete Kante). \\
77

    
78
Wir wollen zunächst zeigen, dass zu einer beliebigen Topologie und Zeit gilt: \\
79

    
80
T ist ein Baum. \\
81

    
82
\newpage
83

    
84
\section*{Beweis durch vollständige Induktion}
85

    
86
\paragraph{Induktionsvorraussetzung}
87

    
88
Für ein beliebiges $T \subseteq G$ gilt: T ist ein Baum.
89

    
90
\paragraph{Induktionanfang}
91

    
92
$T = ({r}, \emptyset)$ (z.B. zu dem Zeitpunkt, zu dem noch keine OGMs versendet wurden)
93
$\Rightarrow$ T ist offensichtlich ein Baum.
94

    
95
\paragraph{Induktionsschritt}
96

    
97
Zu zeigen: T ist ein Baum $\Rightarrow f(T, OGM)$ ist ein Baum. \\
98

    
99
\emph{Fall 1:} $(\urcorner(a) \wedge \urcorner(b)) \vee \urcorner(x)$ \\
100
$\Rightarrow f(T, OGM) = T \Rightarrow$ f(T, OGM) ist kreisfrei. \\
101

    
102
\emph{Fall 2:} $(a) \vee (b)$ \\
103

    
104
T ist ein Baum $\Leftrightarrow$ T ist minimal zusammenhängend $\Rightarrow T - e$ \\
105
ist nicht zusammenhängend mit $e \in E(T)$ beliebig. \\
106

    
107
Seien $T_r$ und $T_{v_c}$ die beiden durch T - e entstandenen, nicht zusammenhängenden
108
Teilgraphen (sogar Untergraphen) mit $v_c \in T_{v_c}$ und $r \in T_r$ \\
109
Dann gilt:
110
\begin{itemize}
111
\item $T_r, T_{v_c}$ sind disjunkt. (*)
112
\item $T_r, T_{v_c}$ sind Bäume. (**)
113
\end{itemize}
114

    
115
\subparagraph{Korollar:} T ist ein Baum $\wedge ((a) \vee (b)) \Rightarrow n \in V(T_r)$ \\
116

    
117
\emph{Fall 2.1 (a):} \\
118
(OGM-seqno größer als seqno des gewählten Routers) \\
119
\emph{Beweis durch Widerspruch} \\
120
Angenommen: T ist ein Baum $\wedge (a) \Rightarrow n \notin V(T_r)$
121

    
122
T ist ein Baum $\Rightarrow^\text{(i)} \forall v \in V(T) : seqno(v_i - 1) >= seqno(v_{i}) \Rightarrow seqno(v_i \in T_r) >= seqno (v_j \in T_{v_c})$ \\
123
$\Rightarrow^{(a)} n \in V(T_r) \Rightarrow \lightning$ \\
124

    
125
\emph{Fall 2.2 (b):} \\
126
(OGM-seqno gleich des gewählten Routers, aber TQ besser - analog, aber mit (ii)) \\\\
127

    
128

    
129
$\Rightarrow$ T ist ein Baum $\Rightarrow^{(a) \vee (b)} n \notin V(T_{v_c}) \Leftrightarrow^{n \in T} n \in V(T_r) \square$
130

    
131
$n \in T_r \wedge v_c \in T_{v_c} \wedge (*) \wedge (**) \Rightarrow (T_r \cup T_{v_c}) + nv_c = T - v_{c-1}v_c + nv_c$ ist ein Baum. \\\\
132

    
133

    
134

    
135
Da T zu einer beliebigen Topologie und Zeit ein Baum ist, gilt: \\
136
T ist maximal kreisfrei zu einer beliebigen Topologie und Zeit. $\square$
137

    
138
\end{document}
    (1-1/1)