We should provide a means to check for (graph) isomorphism.
Current solutions such as automata equivalence require input systems to be deterministic and would deem minimal and non-minimal systems equivalent even though they are not isomorphic. Similarly, while existing bi-simulation implementations focus more on structural properties and support non-deterministic systems, they still do not decide isomorphism.
The implementation may be based on existing algorithms such as VF2 and improvements to it as discussed here and here.
This issue is motivated by #93.