Automatische Strukturen

• Antragsteller: Professor Dr. Erich Grädel
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2013 bis 2018
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 230228719

Die allgemeine Motivation dieses Projektes kommt aus der Algorithmischen Modelltheorie. Es geht darum, die Zusammenhänge zwischen logischen und algorithmischen Eigenschaften endlich präsentierbarer Strukturen besser zu verstehen, im Hinblick auf Anwendungen in verschiedenen Bereichen der Informatik neue Methoden zur logischen und algorithmischen Behandlung unendlicher Strukturen bereitzustellen, und wesentliche theoretische Fragen in diesem Gebiet zu klären.Konkret soll es in diesem Vorhaben um die automatischen Strukturen gehen. Eine Struktur ist dann automatisch, wenn man ihre Elemente so durch Wörter einer regulären Sprache repräsentieren kann, dass alle Funktionen und Relationen der Struktur durch synchron operierende endliche Automaten erkennbar sind. Da automatische Strukturen die effektive (in diesem Fall sogar automatische) Auswertung von beliebigen Formeln der Prädikatenlogik (und gewisser Erweiterungen) erlauben und abgeschlossen sind unter wichtigen Operationen, sind sie ein geeigneter Rahmen für das Forschungsprogramm der Algorithmischen Modelltheorie.Primär wollen wir uns der aktuellen Herausforderung stellen, über den bereits relativ gut verstandenen Fall der wortautomatischen Strukturen hinaus insbesondere die Theorie und die algorithmischen Methoden für omega-automatische und omega-baumautomatische Strukturen weiterzubringen. Darüber hinaus streben wir an, einen hinreichend allgemeinen und umfassenden Rahmen für automatische Strukturen zu finden, in dem, so hoffen wir, grundlegende Fragen unabhängig von spezifischen Präsentationsvarianten geklärt werden können. Zwar haben wir im Bereich der omega-automatischen Strukturen und zu Fragen injektiver oder nicht-injektiver Präsentationen kürzlich wesentliche Fortschritte erzielt, aber die Methoden müssen verfeinert und bereichert werden, um im Gebiet der omega-baumautomatischen Strukturen signifikante Fortschritte zu erzielen. Neben der Arbeit an den bereits etablierten Klassen automatischer Präsentationen, wollen wir zudem den Ansatz, unendliche Strukturen mittels endlicher Präsentationen algorithmisch zu behandeln, systematisch verallgemeinern. Als Motivation dient die zunächst informell gestellte Frage, ob für jede (natürliche) algebraische Struktur mit entscheidbarer Theorie diese auch mit Hilfe einer endlichen (oder sogar in irgendeinem Sinn automatischen) Präsentation der Struktur entschieden werden kann. Diese Frage wurde in gewissem Sinn bereits 1969 von Rabin in seiner klassischen Arbeit über die monadische Theorie des unendlichen Baumes gestellt.Langfristig versprechen wir uns von diesem Unterfangen auch ein besseres Verständnis der algorithmischen Komplexität entscheidbarer Theorien.

• DFG-Verfahren: Sachbeihilfen