Here are two subjects I propose for Master internships, possibly to
be continued as a PhD. (Funding opportunities through
the ERC project CoVeCe.)

These subjects are quite open; please do not hesitate to contact
me directly to discuss about these subjects: I'd be really happy to
take your scientific wishes into account (je parle français, au
besoin).

The internship would take place at ENS Lyon, within the wonderful Plume team.

Thanks to these techniques, our algorithms seem to be more efficient than all algorithms known up to now (Hopcroft&Karp, partition refinment, antichains). We propose to study the possibility of extending these algorithms to other kinds of automata, that are widely used in practice: Büchi automata, alternating automata, tree automata, etc...

Applicants should preferably have a good knowledge of one of those automata models.

- F. Bonchi and D. Pous,
Checking NFA equivalence with bisimulations up to congruence,
*in Proc. POPL 2013.*Associated webpage. - D. Pous,
Symbolic Algorithms for Language Equivalence and Kleene Algebra with
Tests,
*in Proc. POPL 2015.*Associated webpage. - M. D. Wulf, L. Doyen, T. A. Henzinger, and J.-F. Raskin. Antichains:
A new algorithm for checking universality of finite automata.
*In Proc. CAV 2006.* - J. E. Hopcroft and R. M. Karp. A linear algorithm for testing equivalence of finite automata.
*TR 114, Cornell Univ., December 1971.*

So we focus on fragments without complement, and we ask several questions: how to caracterise the corresponding equational theory? Can we decide it? What is its complexity? (This kind of questions were already asked by Tarski in the 40's and many are still unanswered today.)

This is a fairly open-ended topic, requiring a strong interest in logic, universal algebra, and automata theory. I'd be happy to discuss it in more details with anyone interested to join the challenge!

- D. Pous, Notes for a course on this topic (gentle introduction, in french but under translation)
- P. Brunet and D. Pous,
Petri automata for Kleene allegories,
*in Proc. LICS 2015.* - D. Kozen,
A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events,
*Information and Computation, 452:366-390, 1994.* - P. Freyd and A. Scedrov,
Categories, Allegories,
*North Holland, 1990.* - S Givant and A. Tarski,
A Formalization of Set Theory without Variables,
*AMS Colloquium Publications, 1987*

Cf. the Relation Algebra library, which contains tactics for Kleene algebra and Kleene algebra with tests (with underlying automata algorithms).

The idea is to integrate the above research results to

- obtain powerful automation tactics for the algebra of relations;
- extract certified implementations of various automata algorithms, to be used in critical verification applications.

Last modified: Feb 3, 2016