LEA
Fakultät für Informatik der Technischen Universität München
Lehrstuhl für Effiziente Algorithmen
Postadresse: 80290 München; Hausadresse: Arcisstr.21, 80333 München

Oberseminar Theoretische Informatik SS 99

Brauer, Esparza, Mayr, Steger

Mittwochs um 14:00 Uhr s.t., Raum S2229

[Zusammenfassung des nächsten Vortrags (Mittwoch, 28. Juli 1999)]

*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:
  1. Sie ist kompositional, d.h. Äquivalenzbeweise für große Systeme lassen sich oft gut in Beweise für kleinere Teilsysteme zerlegen.
  2. 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.
  3. 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
Marie-Françoise Roy (Université de Rennes 1)
Finding a point in every conected component of the real points defined by a single equation
*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
Javier Esparza
Grammars as Processes


Martin Raab Last modified: Tue Jul 27 13:09:30 METDST 1999
Thomas Erlebach, 1998-04-29