Anthony W. Lin ; Rupak Majumdar - Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility

lmcs:6693 - Logical Methods in Computer Science, October 29, 2021, Volume 17, Issue 4 - https://doi.org/10.46298/lmcs-17(4:4)2021
Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with DivisibilityArticle

Authors: Anthony W. Lin ; Rupak Majumdar

    Word equations are a crucial element in the theoretical foundation of constraint solving over strings. A word equation relates two words over string variables and constants. Its solution amounts to a function mapping variables to constant strings that equate the left and right hand sides of the equation. While the problem of solving word equations is decidable, the decidability of the problem of solving a word equation with a length constraint (i.e., a constraint relating the lengths of words in the word equation) has remained a long-standing open problem. We focus on the subclass of quadratic word equations, i.e., in which each variable occurs at most twice. We first show that the length abstractions of solutions to quadratic word equations are in general not Presburger-definable. We then describe a class of counter systems with Presburger transition relations which capture the length abstraction of a quadratic word equation with regular constraints. We provide an encoding of the effect of a simple loop of the counter systems in the existential theory of Presburger Arithmetic with divisibility (PAD). Since PAD is decidable (NP-hard and is in NEXP), we obtain a decision procedure for quadratic words equations with length constraints for which the associated counter system is flat (i.e., all nodes belong to at most one cycle). In particular, we show a decidability result (in fact, also an NP algorithm with a PAD oracle) for a recently proposed NP-complete fragment of word equations called regular-oriented word equations, when augmented with length constraints. We extend this decidability result (in fact, with a complexity upper bound of PSPACE with a PAD oracle) in the presence of regular constraints.


    Volume: Volume 17, Issue 4
    Published on: October 29, 2021
    Accepted on: September 28, 2021
    Submitted on: August 5, 2020
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Formal Languages and Automata Theory
    Funding:
      Source : OpenAIRE Graph
    • imPACT – Privacy, Accountability, Compliance, and Trust in Tomorrow’s Internet; Funder: European Commission; Code: 610150
    • Algorithmic Verification of String Manipulating Programs; Funder: European Commission; Code: 759969

    1 Document citing this article

    Consultation statistics

    This page has been seen 1707 times.
    This article's PDF has been downloaded 531 times.