 Mi,12.5.1999
|
Christine Röckl
Mechanisierung von Bisimulationsbeweisen für Kommunikationsprotokolle
|
Die Beobachtungsäquivalenz (schwache Bisimilarität) hat einige
interessante Eigenschaften für die Verifikation verteilter Systeme:
- Sie ist kompositional, d.h. Äquivalenzbeweise für große Systeme
lassen sich oft gut in Beweise für kleinere Teilsysteme zerlegen.
- Sind zwei Systeme beobachtungsäquivalent, so kann man von der
Verklemmungsfreiheit eines Systems automatisch auf die des anderen
schließen. Das ist etwa bei der Traceäquivalenz nicht der Fall.
- Die Beobachtungsäquivalenz verfügt über eine weit entwickelte
Theorie auf semantischer (explizites Angeben von Bisimulationsrelationen) und syntaktischer (algebraische Beweise) Ebene, als
auch für Mischformen (Bisimulationen "bis auf").
In einer Fallstudie haben wir untersucht, inwieweit sich die reine
semantische Vorgehensweise (d.h. Angabe einer Relation und Nachweis,
daß es sich dabei um eine Bisimulation handelt) für die Behandlung von
Systemen mit unendlichem Zustandsraum und für parametrisierte Systeme
eignet. Die Beweise umfassen i.d.R. sehr viele Fälle, so daß eine
Beweiserunterstützung praktisch unerläßlich ist. Wir haben für die
Fallstudie Isabelle/HOL verwendet.
Die Fallstudie umfaßt drei Beispiele, u.a. das Alternating Bit Protokoll
und eine Spezifikation von Sliding Window Protokollen durch Alternating
Bit Protokolle.
Das Ergebnis der Fallstudie ist recht vielversprechend: Es konnte sehr
stark von der Kompositionalität der Beobachtungsäquivalenz Gebrauch
gemacht werden. Dadurch daß die zu betrachtenden Fälle oft sehr ähnlich
waren, reichte die einmalige Angabe eines Verfahren aus, und der Beweiser
konnte die restlichen Fälle analog, und damit weitgehend autonom, lösen.
Viel Aufwand kam allerdings durch die Verwendung von Listen für die
Modellierung von Kanälen und parametrisierten Systemen zustande.
|
|
|
Mi,19.5.1999
|
Peter Rossmanith
Learning From Random Text
|
Lernen im Limes untersucht hauptsächlich, was gelernt werden kann und was nicht, aber nicht wie schnell. Das ist auch im
normalen Modell nicht möglich. Daher gibt es entsprechende
Untersuchungen immer nur für bestimmte Spezialfälle.
In diesem Vortrag soll eine Methode gezeigt werden, wie allgemeine
Aussagen zur Lerngeschwindigkeit bewiesen werden können.
|
|
|
Mi,26.5.1999
|
Rom Langerak (University of Twente)
Experiences with model checking in industry
|
|
The talk consists of an intuitive
(non-technical) introduction to model
checking,
together with a brief description of some
industrial projects done at our group using
the model-checking tools SPIN and UPPAAL.
|
|
Fr,28.5.1999
Raum 1400
10:15 - 11:45
|
|
|
Mi,2.6.1999
|
Thomas Erlebach
Algorithmen für bestimmte Maximum-Weight-Independent-Set-Probleme
Das Maximum-Weight-Independent-Set-Problem besteht darin, in einem
gegebenen Graphen mit Knotengewichten eine unabhängige Menge (d.h. eine
Teilmenge der Knoten, so daß keine zwei Knoten in dieser Teilmenge
durch eine Kante verbunden sind) maximalen Gewichts auszuwählen.
Im Vortrag werden zwei Spezialfälle dieses Problems diskutiert:
ein Intervall-Scheduling-Problem, das sich bei der Bestückung von
Produktionsstraßen ergibt, und ein Kantendisjunkte-Pfade-Problem,
das in Kommunikationsnetzwerken mit Circuit-Switching auftritt. Für
beide Spezialfälle werden Approximationsalgorithmen mit konstanter
Approximationsguete vorgestellt. Es wird gezeigt, daß die Analyse
der Approximationsguete scharf ist und daß kein Algorithmus, der die
Eingabe in derselben Reihenfolge wie die vorgestellten Algorithmen
bearbeitet, eine substantiell bessere Approximationsguete erzielen
kann.
Ein Teil des Vortrags beschreibt eine gemeinsame Arbeit mit F. Spieksma
von der Universiteit Maastricht.
|
|
|
Mi,9.6.1999
|
Robert Elsässer (Universität Paderborn)
Loadbalancing Schemes using Network Properties
|
We discuss iterative nearest neighbor load balancing schemes on
processor networks which are represented by a cartesian product
of graphs like e.g. tori or hypercubes.
By the use of the Alternating-Direction Loadbalancing scheme, the number
of load balance iterations decreases by a factor of 2 for this type of
graphs.
The resulting flow is analyzed theoretically and it can be very high
for certain cases.
Therefore, we furthermore present the Mixed-Direction scheme which needs
the same number of iterations but results in a much smaller flow.
Apart from that, we present a simple optimal diffusion scheme for
general graphs which calculates a minimal balancing flow in the
l_2 norm.
The scheme is based on the spectrum of the graph representing the
network and needs only m-1 iterations in order to balance the
load with m being the number of distinct eigenvalues.
|
|
Mi,16.6.1999
13:45
|
Giorgio Delzanno (Max-Plack-Institut für Informatik, Saarbrücken)
Constraint-based Analysis of Broadcast Protocols
|
|
Broadcast protocols (Emerson-Namjoshi 98) are systems composed of
a finite but arbitrarily large number of processes that communicate
by rendezvous (two processes exchange a message) or by broadcast
(a process sends a message to all other processes).
We will show that constraints-based techniques can be used to
efficiently
analyze the flow of processes in these systems.
|
|
|
Mi,23.6.1999
|
Farid Ablayev (Dept. of
Theoretical Cybernetics, Kazan State
University.)
The Complexity of Restricted Branching
Programs: A Communication Complexity Approach (results and open problems)
|
In theory branching programs (BP-s ) are
useful for investigation the amount of space
necessary to compute various functions.
Developments in the field of digital design
and verification have led to the restricted
forms of branching programs. A most common
model used for verifying circuits is a
polynomial size ordered read-once branching
program also called an ordered
binary decision diagram (for short
OBDD). The importance of OBDD for practice
based on the following fact: Boolean
manipulations with OBDD (equivalence checking,
...) can be performed deterministically in
polynomial time. But many important functions
(such as multiplication) can not be presented
by polynomial size OBDD-s. So, important
problem is to investigate the power of
``slightly'' more general models than
OBDD-s.
In the talk we review results on randomized
OBDD-s (ROBDD). It was proved in 1995 that
ROBDD-s are more powerful than their
deterministic counterparts.
Next. We present a generalization of
read-once branching program, which we call
regular (1,+k)-branching program. We
present proof methods and new lower bound
results for regular (1,+k)-branching
program models based on communication
complexity techniques.
We present proof methods and lower bound
results for restricted branching programs,
namely OBDD-s, k-OBDD and their
generalizations.
We formulate research problems of further
developing of communication lower bounds proof
technique for BP-s.
|
|
|
Mi,30.6.99
|
Hanno Lefmann (TU Chemnitz)
Approximation großer unabhängiger Mengen und Anwendungen
auf Optimierungsprobleme
|
Verschiedene
Optimierungsprobleme lassen sich auf die Bestimmung großer
unabhängiger Mengen in geeigneten Graphen oder Hypergraphen
reduzieren.
Unabhängige Mengen in Graphen G = (V, E) sind Teilmengen I
\subseteq V der Punktmenge, die keine Kanten enthalten.
Das Problem, die maximale Kardinalität einer unabhängigen Menge
in einem Graphen zu bestimmen, ist jedoch
NP-hart. Håstad gelang es kürzlich zu zeigen, daß man für Graphen
auf n
Punkten in Polynomialzeit nicht einmal eine Approximationsgüte von O(n^{1/2 -
\epsilon})$
erreichen kann (P \neq NP). Andererseits haben
Boppana und Halldorsson gezeigt, daß man immer in Polynomialzeit eine
Approximationsgüte von O(n/(log n)^2) erreichen kann.
Es zeigt sich, daß in Hypergraphen
die maximale Kardinalität einer unabhängigen Menge ebenfalls
schwer zu approximieren ist.
Für Graphen und Hypergraphen kann man jedoch,
in Abhängigkeit von polynomiell
meßbaren Parametern, in Polynomialzeit eine Mindestgüte für die
Approximation
von unabhängigen Mengen in Graphen und Hypergraphen garantieren, die für
quasizufällige Instanzen fast optimal ist. Die
entsprechenden deterministischen Verfahren, die im
wesentlichen auf probabilistischen Argumenten basieren, werden in diesem
Vortrag vorgestellt. Darüberhinaus werden Anwendungen auf geeigneten Instanzen
diskutiert, wobei nahezu optimale
Lösungen gefunden werden.
|
|
|
Mi,28.7.1999
|
|
|
