 Mi,13.5.1998
|
Richard Mayr
Deciding Weak Bisimilarity of Infinite-State Systems and Finite-State Systems by Model Checking
Weak bisimulation is a semantic equivalence that is often used
in process algebra. We present a general method for deciding
weak bisimilarity of infinite-state systems and finite-state
systems. We show that the equivalence problem can be reduced
to the model checking problem for the branching-time temporal
logic EF. Thus it is decidable for all classes of processes
for which model checking with EF is decidable, e.g. BPA,
BPP, PA and PAD.
|
|
Mi,20.5.1998
|
Mark Scharbrodt (Lehrstuhl für Brauereianlagen und Lebensmittel-Verpackungstechnik)
Approximierbarkeit des Scheduling Problemes mit fixierten Jobs
Im Standardproblem des Maschinen-Scheduling sind n Jobs mit ganzzahligen
Prozesszeiten gegeben, die derart auf m Maschinen zu verteilen sind, dass der
Endzeitpunkt (Makespan) des zuletzt fertiggestellten Jobs minimiert wird. Wir
erweitern das Modell indem wir erlauben, dass
k der n Jobs bereits a priori auf bestimmten Maschinen und zu bestimmten Zeiten eingeplant sind. Die Aufgabe
ist, die verbleibenden n - k Jobs auf den Maschinen einzuplanen, so daß der
Makespan minimiert wird.
Ein solches Modell erlaubt ein realistischeres Abbilden von Anwendungen in der
Produktionsplanung, denn nur in seltenen Fällen kann von der freien
Verfügbarkeit aller Maschinen ausgegangen werden. Vielmehr müssen
Unterbrechungen, bedingt etwa durch Wartung und Reperatur, Reinigungszeiten
oder durch Schichtmodelle berücksichtigt werden. Da derartige
"black out"-Zeiten in der Regel im voraus bekannt sind, können sie auf einfache
Weise durch fixierte Jobs abgebildet werden.
Für dieses Scheduling Problem mit fixierten Jobs werden wir die folgenden
Ergebnisse vorstellen:
Wir präsentieren ein Polynomielles Approximations Schema (PAS) für den
eingeschränkten Fall, dass die Zahl der Maschinen konstant ist. Ist die
Maschinenzahl hingegen Teil der Eingabe, so ergibt unser Ansatz ein
Asymptotisch Polynomielles Approximationsschema (APAS). Als zweites zeigen wir,
dass kein PAS existiert, wenn die Zahl der Maschinen Teil der Eingabeinstanz ist
und dass in beiden Fällen kein Voll Polynomielles Approximationsschema (FPAS)
existieren kann (wenn nicht P = NP gilt). In diesem Sinne ist unser Resultat
das best mögliche für das Scheduling Problem mit fixierten Jobs.
|
|
Mi,27.5.1998
|
Frank Wallner
Model Checking of Logics for Communicating Sequential Agents
Distributed systems are often modelled as a fixed collection of
autonomous, sequential components (agents) which can operate
independently as well as cooperate by exchanging information.
There is an increasing interest in investigating
"local temporal logics" that allow to specify requirements of the
individual components of a distributed system.
While there are several sound model checking procedures for
such logics for the linear-time case, only recently the model
checking problem for similar branching-time logics has been considered.
One such local branching-time logic was introduced by
Lodaya, Ramanujam and Thiagarajan, intended to specify the
behaviour of "Communicating Sequential Agents", a certain
class of prime event structures supporting the notion of locality.
The logic is interpreted at the local states of the contributing
components and allows an agent i to refer to another agent j
according to the "latest gossip", i.e., the most recent information
i has about j via the messages wandering through the system.
We show how McMillan's net unfolding can be used to
solve the model checking problem for this logic.
This is joint work with
Michaela Huhn (Uni Karlsruhe) and Peter Niebert (Uni Hildesheim).
|
|
Mi,3.6.1998
|
Prof. Dr. Javier Esparza
Broadcast Protocols
|
|
Mi,10.6.1998
|
Jens Ernst
Ein System zur Visualisierung und Animation paralleler Graph-Algorithmen
Der Vortrag behandelt eine Diplomarbeit mit dem Titel
"Ein System zur Visualisierung und Animation paralleler Graph-Algorithmen".
Die Aufgabe war dabei der Entwurf und die Implementierung eines für den Lehr- und
Praktikumsbetrieb geeigneten Visualisierungssystems für parallele und insbesondere
verteilte Graph-Algorithmen. Das System bietet sowohl eine Programmierschnittstelle
als auch eine Benutzerschnittstelle mit zahlreichen Möglichkeiten zur Editierung
von Graphen und zur Steuerung der Animation.
Im Diplomarbeitsvortrag wird zunächst die Grobstruktur des Animationssystems und
dann die für parallele Programmierung geeignete Sprache SR vorgestellt.
Abschliessend wird das Visualisierungssystem aus der Benutzerperspektive betrachtet.
|
|
Mi,17.6.1998
|
Martin Raab
Balls into Bins - A Simple and Tight Analysis
Bei der Entwicklung von Verfahren zur Lastverwaltung und bei der
Analyse von Hash-Verfahren wird immer wieder das
``Balls into Bins''-Modell verwendet, bei dem
m Bälle zufällig in n Urnen
geworfen werden.
Ein wichtiger Parameter zur Untersuchung dieser Probleme ist die
maximale Anzahl Bälle, die sich nach dem
Experiment in einer Urne befindet.
In der Literatur findet man an vielen Stellen die Aussage, daß
diese Zahl für den Fall m = n mit hoher Wahrscheinlichkeit in Theta(log n/(log log n)) ist. Dies wird von Gonnet in [1] mit relativ aufwendiger Technik bewiesen.
Im Vortrag werden wir zeigen, wie mit der Methode des ersten und zweiten Moments leicht scharfe Schranken nachgewiesen werden k"onnen, wobei die Anzahl der geworfenen Bälle eine beliebige Funktion der Anzahl Urnen ist.
Wir werden dabei hauptsächlich auf die Methode des ersten und
zweiten Moments eingehen, die in der Analyse von
randomisierten Algorithmen häufig angewandt
werden kann.
[1] Gaston H. Gonnet. Expected length of the longest probe sequence in hash code searching. Journal of the ACM, 28(2):289--304, April 1981
|
|
Mi,24.6.1998
|
Thomas Decker (Universität-GH Paderborn)
Parallel Real Root Isolation
Given a univariate polynomial we compute isolating intervals for
its real roots.
These are disjoint intervals that each contain exactly one real
root and together contain all the real roots.
The intervals are obtained by a bisection method that uses
Descartes' rule of signs and follows a binary search tree.
A first attempt to parallelize the Descartes method was made by
Collins, Johnson, and Küchlin (1992). Their idea was to search left
and right subtrees in parallel. This method is successful provided the
search tree is wide; however, random polynomials have narrow search trees.
Since not much parallelism is available at the tree level,
we parallelize the most time-consuming subalgorithm,
namely the transformation T that transforms a polynomial P(x) into the
polynomial Q(x) = P(x+1).
Since T needs to be performed for each node of the tree, our algorithm
scales well even when the tree is narrow.
We present an BSP*-algorithm for the translation by one which is
2-optimal, which means that the speedup tends to p/2 with growing
input-size. This optimality is achieved for exact arithmetic as
well as for floating point interval arithmetic.
Our experiments with interval arithmetic show that (a) the computation time
can be significantly reduced and (b) that the required precision for
random polynomials is surprisingly low. About 85% of the random
polynomials of degree 1000 can be processed using just 29 bits
of precision. We isolated the real roots of 100 random polynomials of degree
4000 and found that 58 bits of precision sufficed in every case.
Going from 29 to 58 bits of precision increases the computing time by
a factor of about 1.5. The reason why we use software supplied floating point
arithmetic is not the need for precision but the need for large exponents.
|
|
Mi,1.7.1998
|
Peter Rossmanith
Neue obere Schranken für MaxSat
Das Maximum Satisfiability Problem ist folgendermaßen
definiert. Gegeben eine Formel in konjunktiver Normalform. Wie viele
Klauseln lassen sich maximal durch eine Belegung der Variablen
gleichzeitig erfüllen?
Es gibt viele Ergebnisse über exakte Lösungsalgorithmen, welche
Heuristiken verwenden und über polynomielle Approximationsalgorithmen.
Allerdings ist die Lücke zwischen einer beweisbaren oberen Schranke
für die Worst-Case Komplexität des Problems und den experimentellen
Ergebnissen sehr groß. In diesem Vortrag wird diese Lücke
durch bessere obere Schranken in der Anzahl der Klauseln und der Länge
der Formel verkleinert.
|
|
Mi,8.7.1998
|
Thomas Schickinger
Effiziente Optimierung jenseits scharfer
Approximationsschranken
Bei der Lösung NP-harter Optimierungsprobleme besteht ein gebräuchlicher
Ansatz darin, auf Approximationsalgorithmen auszuweichen. Die Qualität
solcher Algorithmen hängt davon ab, wie stark sich die gefundenen
Näherungslösungen vom globalen Optimum unterscheiden. Wenn ein Verfahren zur
Lösung eines Maximierungsproblems für alle Eingaben einen Wert erreicht, der
mindestens halb so groß ist, wie das globale Optimum, so nennt man dies einen
Approximationsalgorithmus der Güte zwei. Je näher die Güte bei Eins liegt,
umso dichter liegen die gefundenen Lösungen beim globalen
Optimum.
Während manche Probleme mit beliebiger Güte 1 + ε approximiert werden
können, existieren für andere Approximationsschranken g > 1 mit der
Eigenschaft, daß es keinen Approximationsalgorithmus mit Güte < g geben kann
(außer es gilt P = NP oder ähnliches).
Für die Probleme MaxkSat und MaxLinEqk-2 (eine Verallgemeinerung von MaxCut)
wurden 1997 von Johan Håstad scharfe Approximationsschranken gezeigt. Die
bestmöglichen Approximationsgüten werden bei diesen Problemen von recht
einfachen polynomiellen Algorithmen erreicht.
Wir beschäftigen uns mit der Frage, wie bei solchen Problemen mit scharfen
Approximationsschranken bessere Lösungen als die polynomiell erreichbaren
Approximationen gefunden werden können. Unser Ziel besteht also darin, exakte
Algorithmen oder Approximationsalgorithmen jenseits der polynomiell
erreichbaren Güten anzugeben, die (u. U. für eingeschränkte Problemklassen)
die Laufzeit O(2n) für vollständige Suche über n Variablen unterbieten.
|
|
Mi,15.7.1998
|
Matthias Westermann (Universität-GH Paderborn)
Data Management in Systems of Limited Bandwidth
This talk deals with data management in computer systems
in which the computing nodes are connected by a relatively sparse network.
We consider the problem of placing and accessing a set of shared objects
that are read and written from the nodes in the network.
These objects are, e.g., global variables in a parallel program,
pages or cache lines in a virtual shared memory system,
shared files in a distributed file system, or pages in the World Wide Web.
A data management strategy consists of a placement strategy
that maps the objects (possibly dynamically and with redundancy) to the nodes,
and an access strategy that describes how reads and writes
are handled by the system (including the routing).
We investigate static and dynamic data management strategies.
In the static model, we assume that we are given an application for which
the rates of read and write accesses for all node-object pairs are known.
The goal is to calculate a static placement of the objects
to the nodes in the network and to specify the routing
such that the network congestion is minimized.
We introduce efficient algorithms that calculate optimal or
close-to-optimal solutions for tree-connected networks,
meshes of arbitrary dimension, and internet-like clustered networks.
These algorithms take time only linear in the input size.
In the dynamic model, we assume no knowledge about the access pattern.
An adversary specifies accesses at runtime.
Here we develop dynamic caching strategies that also aim to minimize
the congestion on trees, meshes, and clustered networks.
These strategies are investigated in a competitive model.
For example, we achieve optimal competitive ratio 3 for tree-connected
networks and competitive ratio O(d log n) for d-dimensional
meshes of size n which is optimal for meshes of constant dimension.
This is a joint work with Bruce Maggs, Friedhelm Meyer auf der Heide,
and Berthold Vöcking.
|
|
Mi,22.7.1998
|
Anna Bernasconi, Michal Mnuk
Algorithmen und Komplexität von Radikalen
Radikale von Idealen sind Objekte, die den
algebraischen Mengen, d.h. den Nullstellen einer
endlichen Anzahl von Polynomen, entsprechen und
diese beschreiben. Wir präsentieren einige
Algorithmen zur Berechnung von Radikalen und
analysieren die Komplexität der Entscheidung, ob ein
Polynom im Radikal eines gegebenen Ideals liegt.
|
|
