Together with Filippo Bonchi, we have recently found a new
algorithm for language equivalence of finite automata on
strings [1]. This algorithm
exploits bisimulations up to congruence, and improves
existing algorithms by an order of magnitude.
- Can we extend this idea to more challenging automata
models? (alternating, tree, push-down, Büchi...)
- Can we mix this idea with symbolic approaches for
handling huge state-spaces?
|
Here we study the theory of binary relations and their
standard operations (union, composition, transitive closure,
converse...).
- Can we decide the equational theory?
- Can we axiomatise it?
- Can we design proof systems for it? (e.g., using
non-commutative linear logic)
We obtained encouraging preliminary results with Paul
Brunet [2], where we use Petri
automata to recognise regular sets of directed
graphs. Many directions remain to be explored.
|
Proof assistants should help the user to write its proof.
To this end, one needs to provide powerful automation tools.
By certifying our results about automata and the calculus of
relations, we aim at
- bringing standard verification techniques into the
realm of proof assistants;
- providing a comprehensive library for binary relations
(i.e., further extending [3]).
As an additional outcome, we expect to distribute certified
implementations of automata algorithms and verification tools.
|
