Loughborough University
Browse
s00224-023-10154-8.pdf (761.64 kB)

A closer look at the expressive power of logics based on word equations

Download (761.64 kB)
journal contribution
posted on 2023-12-11, 15:57 authored by Joel DayJoel Day, Vijay Ganesh, Nathan Grewal, Matthew Konefal, Florin Manea

Word equations are equations α = β where α and β are words consisting of letters from some alphabet Σ and variables from a set X. Recently, there has been substantial interest in the context of string solving in logics combining word equations with other kinds of constraints on words such as (regular) language membership (regular constraints) and arithmetic over string lengths (length constraints). We consider the expressive power of such logics by looking at the set of all values a single variable might take as part of a satisfying assignment for a given formula. Hence, each formula-variable pair defines a formal language, and each logic defines a class of formal languages. We consider logics arising from combining word equations with either length constraints, regular constraints, or both. We also consider word equations with visibly pushdown language membership constraints as a generalisation of the combination of regular and length constraints. We show that word equations with visibly pushdown membership constraints are sufficient to express all recursively enumerable languages and hence satisfiability is undecidable in this case. We then establish a strict hierarchy involving the other combinations. We also provide a complete characterisation of when a thin regular language is expressible by word equations (alone) and some further partial results for regular languages in the general case.

Funding

German Research Foundation (Deutsche Forschungsgemeinschaft, DFG), by the project with number 466789228

History

School

  • Science

Department

  • Computer Science

Published in

Theory of Computing Systems

Publisher

Springer

Version

  • VoR (Version of Record)

Rights holder

© The Author(s)

Publisher statement

This is an Open Access Article. It is published by Springer under the Creative Commons Attribution 4.0 International Licence (CC BY). Full details of this licence are available at: https://creativecommons.org/licenses/by/4.0/

Acceptance date

2023-11-13

Publication date

2023-12-11

Copyright date

2023

ISSN

1432-4350

eISSN

1433-0490

Language

  • en

Depositor

Dr Joel Day. Deposit date: 29 November 2023

Usage metrics

    Loughborough Publications

    Licence

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC