Authors: Filippo Bonchi and Damien Pous.

Checking NFA equivalence with bisimulations up to congruence

Abstract

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. We compare our algorithm to the recently introduced antichain algorithms, by analysing and relating the two underlying coinductive proof methods. We give concrete examples where we exponentially improve over antichains; experimental results moreover show non negligible improvements on random automata.

Coq proof scripts

We used the Coq proof assistant to formalise most results presented in the paper (up to equivalence/congruence/similarity techniques, the rewriting system to compute the congruence closure, the coinductive proof techniques underlying the two antichain algorithms, the facts that HKC/HKC' can mimick AC/AC', and that AC can mimick HKC on disjoint inclusions---only the proofs for the concrete examples are missing.)

Here is an HTML version of the development; here is the raw proof script (to be processed with Coq v8. 4).

Implementation

An implementation of Hopcroft and Karp's algorithm for NFA (HK) and of our optimised version (HKC) can be found here. This is the code we used for the experiments presented in the paper. The model-checking automata we used can be obtained from Lukas Holik's page: we tested the inclusions of the last 16 consecutive pairs of each sequence, in both directions.

Other implementations of language inclusion or equivalence algorithms for finite automata can be found at LanguageInclusion.org. See for instance libvata for tree automata, and RABIT for infinite word automata.

Interactive applet

The various algorithms can be tested online, using the following applet. It suffices to write your favourite NFA in the text field below. (See below for syntax and clickable examples.)

In the HK and HKC columns, the word on the left-hand side is the word corresponding to the current pair; blue pairs are those that are added to the bisimulation up-to candidate; grey pairs are those that are skipped according to the other ones. When checking inclusions, arrows of the form X <-- Y denote pairs of the form X+Y --- Y.

The AC column corresponds to the antichain-based algorithm proposed in this paper for CAV'06. Similarly, blue pairs are those added to the antichain and grey ones are those that are skipped (note that some of the blue pairs are removed in the actual antichain when they are subsumed by a subsequent pair).

Click on the examples below to load them in the above applet.

Syntax