Binary Generalized PCP for Two Periodic Morphisms is Decidable in Polynomial Time

Abstract

We show that the binary generalized Post's Correspondence Problem is decidable inpolynomial time for the case where both morphisms are periodic.

Our result is based oncombinatorial properties and we have formalized the proofs and verified correctness ofour algorithm using the Isabelle/HOL formal proof system.

Keywords

• Binary Post’s Correspondence Problem
• periodic morphism
• Isabelle/HOL.