Graph isomorphism checking?

[liamoc]

Hi there,

I have a system where students will submit automata and they are checked against a given automaton using the equivalence checkers that automatalib generously provides.

But now I have a question where I want students to submit automata that are not minimal. These automata will be checked against the automaton in my system, but I don't want the students to submit just any equivalent automaton, but rather the same one that it's checking against, modulo permutation of the internal identity of the states.

In other words, I want graph isomorphism checking, e.g. with vf2 or something. Have I just missed this, or is this not present in AutomataLib? What's the best way to proceed?

[liamoc]

I should add that these are deterministic automata, so perhaps a more efficient algorithm could be devised than just vf2, something like a depth first search might even work.

[mtf90]

For testing equivalence, you could use Automata#testEquivalence (or Automata#findSeparatingWord if you want to provide an explanation as to why two automata may not be equivalent). For additionally ensuring isomorphism, shouldn't it suffice to simply check whether the size of the two automata is equal as well? If you are interested in identifying actual equivalent states, Bisimulation#bisimulationEquivalenceRelation may help you out.

However, note that many equivalence checks internally use a notion of "structural bisimilarity". For acceptor-based systems in particular (e.g., DFAs), an undefined transition and a transition into a rejecting sink are language-equivalent, but AutomataLib would identify them as inequivalent. The easiest way to prevent any unexpected results would be to ensure the completeness of both input automata. As an alternative, you could fine-tune the flags on, e.g., NearLinearEquivalenceTest#findSeparatingWord.

[mtf90]

(sorry, for the previous response, I haven't seen your reply yet)

Aah, the automata in your system may not be minimal as well. I thought this was the case and only your students could potentially submit non-minimal automata. Then the size check is not enough.

Unfortunately, there currently exists no implementation for checking isomorphism. The closest you'll get is the previously mentioned Bisimulation functionality. But this may be an actual use-case to implement something like VF2 then.

[liamoc]

I see. While graph-isomorphism checking may be nice, I am thinking that for my use case (deterministic moore machines) I might be able to get away with the following idea:

Use Floyd-Warshall APSP algorithm from the initial state on both automata (automatalib already has this). Change the property of each state to be the pair of the original property AND the shortest path from the initial state. Then check for equivalence.

I'm pretty sure this would work here.

[mtf90]

Definitely sounds like worth a try. However, make sure that you use the
same order of input sequences (e.g., the same alphabet instance) to
compute the shortest paths, otherwise the access sequences may differ
even for isomorphic states.

[liamoc]

Right. They will have the same alphabet. If there are multiple shortest paths to a given state, how does APSP choose which one to pick? Does it always pick the alphabetically "smallest" one?

[mtf90]

The implementation should deterministically explore states according to the given alphabet. So if a comes before b it should return [a] as SP instead of [b].