Seminar: Coinduction Up-To for Non Deterministic Automata

Abstract. In this talk, I will introduce the Coinduction proof principle and its enhancements by mean of up-to techniques.
I will introduce bisimulation up to congruence as a technique for
proving language equivalence of non-deterministic finite automata. Such
technique can be effectively implemented in an algorithm that
exponentially improves the state of the art.