Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On Solving String Equations via Powers and Parikh Images

Clemens Eisenhofer, Theodor Seiser, Nikolaj S. Bjørner, Laura Kovács

TL;DR

Key to this work are the combination of three techniques: a power operator for strings; generalisations of Parikh images; and equality decomposition, which allows us to solve complex string equations, including less commonly encountered SMT inputs over strings.

Abstract

We present a new approach for solving string equations as extensions of Nielsen transformations. Key to our work are the combination of three techniques: a power operator for strings; generalisations of Parikh images; and equality decomposition. Using these methods allows us to solve complex string equations, including less commonly encountered SMT inputs over strings.

On Solving String Equations via Powers and Parikh Images

TL;DR

Key to this work are the combination of three techniques: a power operator for strings; generalisations of Parikh images; and equality decomposition, which allows us to solve complex string equations, including less commonly encountered SMT inputs over strings.

Abstract

We present a new approach for solving string equations as extensions of Nielsen transformations. Key to our work are the combination of three techniques: a power operator for strings; generalisations of Parikh images; and equality decomposition. Using these methods allows us to solve complex string equations, including less commonly encountered SMT inputs over strings.
Paper Structure (25 sections, 1 theorem, 16 equations, 2 figures, 2 tables)

This paper contains 25 sections, 1 theorem, 16 equations, 2 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Strings.
  4. String equations and substitutions.
  5. Interpretations and models.
  6. String Solving -- Workflow
  7. Expansion of Nielsen Graphs
  8. Nielsen graphs.
  9. String Solving via Expansion of Nielsen Graphs.
  10. Extended Nielsen Transformations Rules
  11. Lemma rules.
  12. Term rewriting rules.
  13. Equation rewriting and generating rules.
  14. Equality Decomposition
  15. Ground Power Introduction
  16. ...and 10 more sections

Key Result

lemma 1

Assume $w$ is an unbordered pattern.

Figures (2)

  • Figure 1: String solving workflow.
  • Figure 2: Fully expanded Nielsen graph for the plain string equation $xx \simeq yb$, representing a variant of a tableau derivation.

Theorems & Definitions (4)

  • definition 1: Token & String Terms
  • remark 1: Termination of expanding Nielsen graphs
  • lemma 1: Correctness of Parikh images for Unbordered Patterns
  • definition 2: $d$-gaps and $w \bowtie u$