Bisimulation, at its core, is a means of studying the alignment between two dynamical systems. It has been used to great effect in the planning community for heuristic computation; simulating the full state space in the space of abstractions (merge-and-shrink heuristics). Here, we consider the direct task of theory alignment– assessing if two planning problems are “equivalent”– through the lens of regular bisimulation. We accomplish the task through a novel encoding that merges the two theories as a new planning problem, where the encoded problem is unsolvable if and only if the two theories are a regular bisimulation. We demonstrate that modern planners are capable of solving many of these encodings, and the solutions (if plans exist) provide a rich explanation as to why two models differ. The work has already had a direct and practical impact, being deployed in a classroom setting to assess the correctness of student-authored planning models as compared against a reference solution. Our solution has a direct impact on being able to verify if a candidate planning model matches a known specification, and opens the door to model verification through planning techniques.