|
![](images/spacer.gif) |
Vendredi 12 Février
Heure: |
11:00 - 12:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Hacking Nondeterminism with Induction and Coinduction |
Description: |
Damien Pous Finite automata are used in a wide range of verification problems. 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". |
|
|