Yuxin Deng (ECNU)

On Equivalence Checking of Nondeterministic Finite Automata

Language equivalence for nondeterministic finite automata is
important in many application domains such as compiler
construction and model checking. Algorithms for checking language
equivalence have been proposed in the literature, but a
comprehensive comparison is missing. In this paper we provide a
comparative study of some typical algorithms and various
combinations of optimisation techniques. We find that their
practical efficiencies depend very much on the automata under
consideration. We analyse the reasons behind, which should be very
useful in choosing appropriate algorithms in practical
applications. The analysis is conducted by using our tool EBEC
that is an initial step towards building a common platform for
comparing state-of-the-art algorithms for checking behavioural
equivalences.

(Ongoing joint work with Chen Fu and Lijun Zhang)