String Constraint Solving: Kombinatorische, algorithmische und sprachtheoretische Ansätze

• Antragsteller: Professor Dr. Florin Manea
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung seit 2025
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 562495345

Strings (Wörter oder Zeichenketten) sind ein grundlegender Datentyp, der in den meisten Bereichen der Informatik vorkommt, beispielsweise als primäre Art, Nutzereingaben zu erhalten und Informationen an den Benutzer zurückzugeben. Daher sind das Verständnis der grundlegenden mathematischen Eigenschaften von Strings und die Entwicklung effizienter Verarbeitungsmethoden für Zeichenketten zentrale Aufgaben in der theoretischen Informatik, die tiefgreifende und wichtige praktische Anwendungen haben. In diesem Projekt befassen wir uns mit einer Reihe grundlegender Probleme aus dem Bereich der Kombinatorik und Algorithmik auf Strings (kurz: Stringologie) sowie mit deren potenziellen Anwendungen in anderen Bereichen der Informatik, wie der formalen Verifikation. String-Constraint-Solving (kurz: String-Solving) ist ein in diesem Zusammenhang aufkommendes Thema, das in letzter Zeit im Bereich der formalen Methoden in den Vordergrund gerückt ist und tiefe Wurzeln in der Theorie der Wortgleichungen und damit in der Algebra und der Theorie der formalen Sprachen hat. Dieses Forschungsgebiet ist reich an schwierigen, seit langem offenen Problemen (beispielsweise die Entscheidbarkeit von Wortgleichungen mit linearen Längenbeschränkungen, ein Problem, welches eng mit Hilberts Zehntem Problem zusammenhängt), deren Lösung wichtige praktische Anwendungen haben würde. Unser Ziel ist es vor allem, bedeutende Fortschritte bei der Lösung der zentralen offenen Probleme im Bereich des String-Solving zu erzielen. Darüber hinaus werden wir einige interessante verwandte Probleme betrachten, die sich bei der Untersuchung einiger spezieller, durch praktische Szenarien motivierter, Klassen von String-Constraints ergeben. Während unser Ansatz auf kombinatorischen und formalen sprach- oder automatentheoretischen Werkzeugen basiert, besitzt er auch eine wichtige algorithmische Komponente, und ein erwünschtes Nebenerzeugnis unserer Arbeit besteht in der Entwicklung leistungsfähiger praktischer String-Constraint-Solver. Insgesamt erwarten wir, dass dieses Projekt sowohl in der theoretischen Informatik (insbesondere in Bereichen wie den formalen Sprachen und der Stringologie) als auch in den damit verbundenen praktischen Bereichen zu bedeutenden und wirkungsvollen Fortschritten führen wird.

• DFG-Verfahren: Sachbeihilfen