Solving String Equations

Stringgleichungen, treten in vielen Bereichen der Softwareentwicklung und formalen Methoden auf. Sie spielen eine zentrale Rolle in Aufgaben wie Sicherheitsanalysen, automatisiertem Schließen und Softwareverifikation, bei denen die Erfüllbarkeit einer Bedingung wie xy = abc darüber entscheidet, ob ein bestimmtes Programmverhalten möglich ist. Eine Lösung für eine solche Bedingung ist eine Belegung der Variablen mit konkreten Zeichenketten, sodass die Gleichung erfüllt ist. Diese Arbeit befasst sich eingehender mit der Nielsen-Transformation, einem verbreiteten Ansatz zum Lösen von Stringgleichungen. Die Nielsen-Transformation wendet systematisch Umformungsregeln an, um Gleichungen zu reduzieren, bis sie trivial erfüllbar oder unerfüllbar sind. Die dabei entstehenden Variablensubstitutionen können mit Hilfe eines Substitutionsgraphen organisiert und untersucht werden. Ein weiterer bedeutender Ansatz ist Recompression, wo Gleichungen durch iteratives Ersetzen von wiederholten Mustern durch neue Symbole vereinfacht werden. Dadurch wird die Problemgröße reduziert, während die Erfüllbarkeit erhalten bleibt. Ein dritter häufig verwendeter Ansatz nennt sich Stabilization. Solver modellieren dabei Variablendomänen als reguläre Sprachen und verwenden Automaten, um diese Domänen schrittweise zu verfeinern. Wir erweitern die Menge der Regeln für die Nielsen-Transformations um eine parametrisierte Substitutionsregel, die unendliche Familien von Lösungen, die durch Zyklen im Substitutionsgraphen entstehen, kompakt darstellt. Dies ermöglicht es, Zyklen durch eine einzige Kante mit einer Potenzannotation zu ersetzen, wodurch Termination in Fällen möglich wird, in denen das ursprüngliche Verfahren divergieren würde. Darüber definieren wir das Konzept der Signatur für eine Gleichung, die ein gemeinsames strukturelles Präfix verschiedener Gleichungen erfasst. Gleichungen mit derselben Signatur durchlaufen oft dieselbe Abfolge von Umformungsschritten, auch wenn sich ihre verbleibenden Teile unterscheiden. Durch das Gruppieren solcher Gleichungen lassen sich redundante Graphenerweiterungen vermeiden und der Suchraum verkleinern. Durch die Signatur wird das Problem in Teilprobleme geteilt und es ergeben sich Teillösungen. Zur kompakten Darstellung dieser Teillösungen verwenden wir EDT0L-Sprachen, die einen formalen, sprachtheoretischen Rahmen bieten, um potenziell unendliche Mengen von Lösungen strukturiert zu erfassen.