Damien Pous' Home Page.

Proposals for M2 internships

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.

1. Coinductive and symbolic algorithms for challenging automata models

We recently proposed algorithms for checking language equivalence of non-deterministic finite automata (NFA), by relying: 1/ on techniques from concurrency and process algebra theory: ``bisimulations up to'' [1], and 2/ on a symbolic representation of automata, using BDD [2] .
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.
  1. F. Bonchi and D. Pous, Checking NFA equivalence with bisimulations up to congruence, in Proc. POPL 2013. Associated webpage.
  2. D. Pous, Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests, in Proc. POPL 2015. Associated webpage.
  3. 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.
  4. J. E. Hopcroft and R. M. Karp. A linear algorithm for testing equivalence of finite automata. TR 114, Cornell Univ., December 1971.

2. Relation algebra without complement

We consider the equational theory generated by binary relations together with standard operations (e.g., union, intersection, composition, converse, reflexive transitive closure). If we also take the operation of complement, this equational theory is highly undecidable, and any axiomatisation must be incomplete, by Gödel theorem.
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!
  1. D. Pous, Notes for a course on this topic (gentle introduction, in french but under translation)
  2. P. Brunet and D. Pous, Petri automata for Kleene allegories, in Proc. LICS 2015.
  3. D. Kozen, A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events, Information and Computation, 452:366-390, 1994.
  4. P. Freyd and A. Scedrov, Categories, Allegories, North Holland, 1990.
  5. S Givant and A. Tarski, A Formalization of Set Theory without Variables, AMS Colloquium Publications, 1987

The Coq proof assistant

In both cases, there is the possibility of doing some Coq formalisation, if you feel the envy for it.
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
Last modified: Feb 3, 2016