Mitarbeiterseminar Logik in der Informatik

Joint work with Andreas Bjoerklund, Petteri Kaski, Mikko Koivisto
To appear at STACS 2008
http://www.cs.lu.se/home/Thore_Husfeldt/papers/trimmedmoebius.pdf

Abstract:
Hamiltonsche Pfade in automatische Graphen und verwandte Probleme
(gemeinsame Arbeit mit Markus Lohrey)

Automatische Graphen sind gegeben durch zwei endliche Automaten, die
die Menge der Knoten bzw. die Menge der Kanten erkennen (hierfuer wird
ein synchroner Zweiband-Automat verwendet). Daher stellen sie eine
Einschraenkung der rekursiven Graphen dar, bei denen Turingmaschinen
verwendet werden.

Wie in der Theorie der rekursiven Graphen ueblich fragen wir, wie sich
Eigenschaften des automatischen Graphen in den Automaten
wiederspiegeln. Dabei zeigen wir:

- die Existenz eines Hamiltonpfades in einem planaren automatischen
Graphen von beschraenktem Grad ist $Sigma_11$-vollstaendig (fuer
rekursive Graphen wurde dies von Hirst und Harel gezeigt)

- die Existenz eines unendlichen Astes in einem automatischen
Nachfolgerbaum ist $Sigma_11$-vollstaendig (fuer rekursive
Nachfolgerbaeume ist dies ein klassisches Ergebnis von Kleene)

- die Existenz einer unendlichen Clique in einem automatischen
Graphen, eines unendlichen Astes in einem automatischen Ordnungsbaum
bzw. einer ko-unendlichen Ueberdeckung in einem automatischen
bipartiten Graphen sind entscheidbar (diese Fragen sind
$Sigma_11$-vollstaendig fuer rekursive Graphen). Diese
Entscheidbarkeitsergebnisse werden erzielt, indem wir ein geeignetes
Fragment der Logik zweiter Stufe betrachten und dessen
Entscheidbarkeit zeigen.