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

Abstrakt

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.

Klíčová slova

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