Lynch-Morawska Systems on Strings

TL;DR

This paper studies specific string rewriting systems called $LM$-Systems, proving their subterm-collapse problem is decidable and applying this to solve the cryptographic cap problem in this context.

Contribution

It adapts the $LM$-System criteria to string rewriting, proves the subterm-collapse problem is decidable, and shows the cap problem is decidable for string systems.

Findings

Subterm-collapse problem is effectively solvable for $LM$-Systems.

Decidability of the cap problem is established for string rewriting $LM$-Systems.

Provides decision procedures for properties of convergent and forward-closed string rewriting systems.

Abstract

We investigate properties of convergent and forward-closed string rewriting systems in the context of the syntactic criteria introduced in \cite{LynchMorawska} by Christopher Lynch and Barbara Morawska (we call these $LM$-Systems). Since a string rewriting system can be viewed as a term-rewriting system over a signature of purely monadic function symbols, we adapt their definition to the string rewriting case. We prove that the subterm-collapse problem for convergent and forward-closed string rewriting systems is effectively solvable. Therefore, there exists a decision procedure that verifies if such a system is an $LM$-System. We use the same construction to prove that the \emph{cap problem} from the field of cryptographic protocol analysis, which is undecidable for general $LM$-systems, is decidable when restricted to the string rewriting case.