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.
de
String equations arise in many areas of software engineering and formal methods. They play a central role in tasks such as security analysis, automated reasoning, and software verification, where the satisfiability of a constraint like xy = abc determines whether a program behavior is possible. A solution to such a constraint is an assignment of concrete strings to variables that satisfies the equation. This thesis takes a closer look at Nielsen transformation, a common approach to solving string equations. Nielsen transformation applies systematic rewriting rules to reduce equations until they become trivially satisfiable or unsatisfiable. The rules may lead to variable substitutions, which can be organized and explored using a substitution graph. Another prominent approach is recompression, where equations are simplified by iteratively replacing repeated patterns with fresh symbols, reducing problem size while preserving satisfiability. A third approach, often used by solvers, is called stabilization. Variable domains are represented as regular languages and automata are used to iteratively refine these domains. We extend the standard Nielsen transformation rule set with a parameterized substitution rule that compactly represents infinite families of solutions arising from cycles in the substitution graph. This allows cycles to be replaced by a single edge annotated with a power expression and enabling termination in cases where the unmodified procedure would diverge. We define a signature for an equation, representing a common structural prefix of different equations. Equations sharing the same signature evolve through the same repeating sequence of rewriting steps, even if their trailing terms differ. By grouping such equations, we avoid redundant graph expansion in certain cases and reduce the size of the search space. By using the signature the problem is divided into subproblems that lead to partial solutions. To represent these partial solutions compactly, we use EDT0L languages, which provide a formal language-theoretic framework to capture potentially infinite sets of solutions in a structured way.
en
Additional information:
Arbeit an der Bibliothek noch nicht eingelangt - Daten nicht geprüft Abweichender Titel nach Übersetzung der Verfasserin/des Verfassers
