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.
- 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.
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!
- 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
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
- 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