Logik in der Informatik Prof. Dr. Martin Grohe

Institut für Informatik

Dieses Seminar wird von Mitgliedern des Lehrstuhls Logik in der Informatik als Forum der Diskussion und des Austauschs genutzt. Studierende und Gäste sind herzlich eingeladen. Das Seminar findet während des Wintersemesters 2004/05 Freitags von 11-13 Uhr im Raum 4.410 des Johann von Neumann Hauses (Rudower Chaussee 25) statt.

Nächster Vortrag: hier.

Folgende Termine und Vorträge sind bisher vorgesehen:

Fr, 29.10.04, 11:15 Uhr, Raum 4.410:

Thema:	The Complexity of Finding Graphs in Graphs with Bounded Independence Number
Referent:	Till Tantau (TU Berlin)
Abstract:	We study the problem of finding a path between two vertices in finite directed graphs whose independence number is bounded by some constant k. The independence number of a graph is the largest number of vertices that can be picked such that there is no edge between any two of them. The complexity of this problem depends on the exact question we ask: Do we only wish to tell whether a path exists? Do we also wish to construct such a path? Are we required to construct the shortest one? Concerning the first question, we show that the reachability problem is first-order definable for all k and that its succinct version is Pi_2^P-complete for all k. In contrast, the reachability problems for many other types of finite graphs, including dags and trees, are not first-order definable and their succinct versions are PSPACE-complete. Concerning the second question, we show that not only can we construct paths in logarithmic space, there even exists a logspace approximation scheme for this problem. The scheme gets a ratio r>1 as additional input and outputs a path that is at most r times as long as the shortest path. Concerning the third question, we show that even telling whether the shortest path has a certain length is NL-complete and thus as difficult as for arbitrary directed graphs.

Fr, 05.11.04, 11:15 Uhr, Raum 4.410:

Thema:	Machines, Model-Checking Problems and Parameterized Complexity (1st talk)
Referent:	Yijia Chen (HU Berlin)
Abstract:	Parameterized complexity is built on a relaxed notion of tractability, i.e., fixed-parameter tractability. Significant progress has been made for designing fixed-parameter tractable algorithms for some classically intractable problems. Also a great number of parameterized intractable classes has been identified to classify problems that seem fixed-parameter intractable, which resembles the classical NP-completeness theory. However almost all those classes are originally defined as closures of kernel problems under some type of reductions, which makes them hard to understand and apply. So we try to lay a machine-based foundation for parameterized intractability. The starting point is the class W[P], which we characterize as the languages that are decidable by nondeterministic fixed-parameter tractable algorithms of random access machines whose use of nondeterminism is bounded in terms of the parameters. By further tuning the nondeterminism that machines can use, say, allowing alternating, or restricting the access to the guessed numbers, we obtain characterizations of most parameterized intractable classes.Our main technical tools are model-checking problems. It is well known that various model-checking problems of natural fragments of first-order logic are complete for some of the most important parameterized classes. And they turn out to be much more manageable than those hard combinatorics required to deal with those classes when using the original definitions. We investigate model-checking problems on structures with functions, while most previous works study relational structures. Based on that we introduce a new hierarchy of classes, prove some basic complete results and give their machine characterizations. Finally we also study the halting problems of Turing machines in the context of parameterized complexity. It is previously known that some natural halting problems are complete for some parameterized classes. We give complete halting problems for other important classes. This is a joint work with Jörg Flum and Martin Grohe. The first talk will focus on the machine characterizations, the second one is about model-checking problems and halting problems.

Fr, 12.11.04, 11:15 Uhr, Raum 4.410:

Thema:	Machines, Model-Checking Problems and Parameterized Complexity (2nd talk)
Referent:	Yijia Chen (HU Berlin)
Abstract:	Siehe oben.

Fr, 26.11.04, 11:15 Uhr, Raum 4.410:

Thema:	Model-Checking Spiele
Referent:	Stephan Kreutzer (HU Berlin)
Abstract:	Ein zentrales Ziel der Verifikation besteht darin, weitgehend automatisierte Methoden zu entwickeln, um Eigenschaften gegebener Prozesse überprüfen zu können. Besonders im Bereich der Hardware-Verifikation hat sich dabei das sogenannte "Model-Checking" als erfolgreich erwiesen. Dabei wird der Prozess durch ein Transitionssystem modelliert und die zu verifizierende Eigenschaft durch eine Formel einer temporalen Logik formalisiert. Die Frage, ob der Prozess die Eigenschaft erfüllt, reduziert sich somit auf die Frage, ob die Formel in dem Transitionssystem gilt. Um den Model-Checking Ansatz nutzbar zu machen, benötigt man also effiziente Verfahren, um Formeln temporaler Logiken in Transitionssystemen auszuwerten. Eine hierzu sehr erfolgversprechende Methode reduziert das Auswerten von Formeln in Transitionssystemen auf automaten- oder spieltheoretische Probleme, insbesondere auf das Finden von Gewinnstrategien in bestimmten Formen graphbasierter Zwei-Personen Spiele. Im Vortrag soll dieser Ansatz zur Verifikation und die dabei verwendeten Spiele eingeführt und einige der wichtigen Resultate aus diesem Bereich vorgestellt werden. Anschliessend werden einige neuere Resultate besprochen und ein Ausblick auf aktuelle Forschung im Bereich der Model-Checking-Spiele gegeben.

Fr, 03.12.04, 11:15 Uhr, Raum 4.112:

Thema:	Aspekte der Anfragebearbeitung für große, semistrukturierte Datenmengen und XML-Datenströme
Referentin:	Nicole Schweikardt (HU Berlin)
Abstract:	In dem Vortrag geht es um ein Szenario, in dem Anfragen an Daten bearbeitet werden sollen, die nicht in der strukturierten Form einer relationalen Datenbank vorliegen, sondern als einfache Sammlung von Files, etwa im XML Format. Wir nehmen an, dass die Datenmengen zu groß sind, um als ganzes im Hauptspeicher bearbeitet werden zu können. Diese Situation ist nicht untypisch, etwa liegen große Sammlungen medizinischer Daten in solcher Form vor. Als wichtigen Spezialfall betrachten wir auch die Situation, in der die Daten nur als Datenstrom verfügbar sind. Als entscheidende Maße für die Komplexität solcher Anfragen betrachten wir die Größe des Hauptspeichers und die Zahl der direkten Speicherzugriffe ("Random Access") auf den Sekundärspeicher. Unser Modell berücksichtigt, dass das sequentielle Strömen der Daten durch den Hauptspeicher deutlich geringere Kosten verursacht als direkte Zugriffe. Der Vortrag soll einen Überblick über Fragestellungen und Ergebnisse hinsichtlich der Grundlagen der Verarbeitung solch großer semistrukturierter Datenmengen geben. Besonders werden dabei die Themen "Anfrageoptimierung", "Eigenschaften von Anfragesprachen" und "komplexitätstheoretische Untersuchung der Verarbeitung großer Datenmengen" berücksichtigt.

Fr, 10.12.04, 11:15 Uhr, Raum 4.410:

Thema:	Parameterized complexity of constraint satisfaction problems
Referent:	Daniel Marx (Budapest University of Technology and Economics)

Fr, 14.01.05, 11:15 Uhr, Raum 4.410:

Thema:	#SAT-Solver
Referent:	Marc Thurley (HU Berlin)
Abstract:	Das #SAT-Problem ist eng verwandt mit dem aussagenlogischen Erfüllbarkeitsproblem (SAT). Deshalb hat die Entwicklung von SAT-Solvern viele Ideen geliefert, mit welchen Verfahren man das #SAT-Problem effizient lösen könnte. In dem Vortrag soll es einerseits darum gehen, zu erläutern, wie SAT-Solver für #SAT verwendet werden können. Außerdem werde ich Konzepte vorstellen, die #SAT-Solver von SAT-Solvern unterscheiden, wobei zuletzt verglichen werden soll, wie sich die #SAT-Solver unter Anwendung dieser Konzepte in der Praxis verhalten.

Fr, 28.01.05, 11:15 Uhr, Raum 4.410:

Thema:	TIM: Theoretische Informatik mit Mathematica - Eine Demonstration ausgewählter Anwendungen zur Unterstützung der Studentenausbildung im Fach Theoretische Informatik
Referent:	Klaus-Peter Neuendorf (HU Berlin)
Abstract:	Im Vortrag wird insbesondere die didaktische Bedeutung der durch Mathematica ermöglichten konkreten Modellierung, Visualisierung und Programmierung, sowie des "Ausprobierens" von Modelldefinitionen und Algorithmen der Theoretischen Informatik aufgezeigt.

Fr, 04.02.05, 11:15 Uhr, Raum 4.410:

Thema:	Charakterisierungen von P mittels Selbstreduktion und Teilinformation
Referent:	Andre Hernich (TU Berlin)
Abstract:	Selbstreduzierbarkeit ist eine Eigenschaft, die sich viele NP-vollständige Sprachen (z.B. SAT) sowie PSPACE-vollständige Sprachen (z.B. QBFSAT) teilen. Teilinformationsklassen enthalten Sprachen, für die in Polynomialzeit Teilinformation bezüglich der Mitgliedschaft von Wörtern in solchen Sprachen berechenbar ist. Beispiele sind die Klassen der p-selektiven, strongly membership comparable und der leicht zählbaren Sprachen, die ausführlich in der Literatur studiert wurden. Es ist bekannt, dass die Sprachen in P genau die selbstreduzierbaren p-selektiven Sprachen sind. In diesem Vortrag soll gezeigt werden, dass ähnliche Ergebnisse auch für andere Teilinformationklassen gelten. Zum Beispiel lassen sich die Sprachen in P ebenso charakterisieren als selbstreduzierbare Sprachen L, die leicht 2-zählbar oder für die L und das Komplement strongly 2-membership comparable sind.