Post correspondence problem for finite monoids The Post correspondence problem has the following version for finite monoids:

Input: a finite monoid $M$ and a finite list $(m_1,m_1'),\ldots, (m_n,m_n')$ of pairs of elements of $M$

Question: is there a natural number $k\geq 1$ and indices $i_1,\ldots, i_k\in \{ 1,\ldots, n\}$ such that $m_{i_1}\cdot\cdots \cdot m_{i_k} = m_{i_1}'\cdot\cdots \cdot m_{i_k}'$?

Is it known whether this problem is decidable?
Yes, it is decidable.  Build a graph where each vertex is a pair $(r,s)$ of elements from $M$.  Add all edges of the form $(r,s) \to (r m_i, s m'_i)$ for all $r,s,i$.  Then, your question asks whether there exists a path in this graph from the vertex $(1,1)$ to any vertex of the form $(t,t)$.  This can be answered using standard reachability algorithms (e.g., DFS).  The running time is linear in the size of the graph (i.e., $O(|M|^2 n)$), so the problem is decidable.