The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
We introduce "bisimulation up to congruence" as a technique for proving language equivalence of non-deterministic finite automata. Exploiting this technique, we devise an optimisation of the classical algorithm by Hopcroft and Karp which, as we show, is exploiting a weaker "bisimulation up to equivalence" technique. The resulting algorithm can be exponentially faster than the recently introduced antichain algorithms. We actually show that antichain-based algorithms correspond to using an up-to context technique, so that our algorithm can be seen as the result of merging both antichains and Hopcroft and Karp's ideas.