Antoine Durand-Gasselin

Since September 2015, I am a post-doc at École Centrale Marseille (where I teach) and Université Aix-Marseille (as a member of Modélisation and Verification team of Laboratoire d'Informatique Fondamentale).

Research Interests

My research is in the field of theoretical computer science. I study logic and my primary topic of interest is Automata Theory, since automata (and their extansions) can be seen as a bridge between computational models and formal logic. As I give as much focus on complexity analysis as on expressivity, my work can be classified in the domain of formal verification. Program verification consists in achieving greater confidence in the correct behaviour of a given program. The most commonly used approach is an empiric one, which can be summarized as testing the actual programs. Formal verification deals with formal computational models, which allows to use logical formalism to express and prove formally some properties of our computational models. What is gained by being able to use mathematical proofs is probably lost in practicality, yet it gives some valuable insight for developping new techniques of software verification (model checking, symbolic analysis, etc.)

Automatic Structures

The core idea of Automatic Structures is that some infinite structures can be presented in a finite manner with automata. This is a very strong restriction, which gives decidability of the underlying first order theory. That decidability is shown with a very generic algorithm: an inductive translation of first order formulas to automata.
We exhibited that, surprisingly, this generic construction which can be non-elementary in general, when restricted to Presburger Arithmetic, closely matches the complexity of the quantifier elimination procedure. We gave a criterion to exhibit such finer upper bounds of complexity for any automatic structure. On the automatic structures we studied, that upper bound closely matches the complexity of the underlying first order theory.
These results yield an interesting question: for any given automatic structure, does this generic decision procedure always have a "good" complexity ? A positive answer would then imply that the choice of the automatic presentation cannot impact the complexity of the construction.

Regular Strings Transformations

I also work on Streaming String Transducers (and currently on extensions for data words) which generalize (classical) deterministic finite state automata (language acceptors) to a model of string transformation. These transformations are referred to as the regular string transformations.
An admirable property of this class of transformations is that it (also) admits a triple characterisation: a logical characterization relying on the (generic) MSO graph transduction, a characterization through the two way model of two-way deterministic transducers (essentially memoryless Turing machines) and finally the characterization through the sequential model of Streaming String transducers.
This triple characterization makes this class of regular transformations very robust and allows to exploit the best of these three worlds. Furthermore this class naturally lifts regular languages to regular transformations: some key ideas and proof techniques that were developed for regular languages can be reused in this new setting. For this reason, this extension of regular languages gives some new hindsight and a more comprehensive understanding of the fundamental aspects of formal languages.
A very appealing research direction is to lift results originating from automata theory and formal languages (typically extensions of the model of automata: data words, trees, nested words, timed languages, etc.) to that new setting of transformations, without the limitation of regular languages.


Conference Proceedings

Antoine Durand-Gasselin and Peter Habermehl. Regular transformations of data words through origin information. In FoSSaCS, volume 9634 of Lecture Notes in Computer Science, pages 285-300. Springer, 2016. [ bib |  .pdf ]
Antoine Durand-Gasselin, Javier Esparza, Pierre Ganty and Rupak Majumdar. Model Checking Parameterized Asynchronous Shared-Memory Systems. In CAV, volume 9206 of Lecture Notes in Computer Science, pages 67-84. Springer, 2015. [ bib |  .pdf ]
Rajeev Alur, Antoine Durand-Gasselin, and Ashutosh Trivedi. From Monadic Second-Order Definable String Transformations to Transducers. In LICS, pages 458-467. IEEE Computer Society, 2013. [ bib | .pdf ]
Antoine Durand-Gasselin and Peter Habermehl. Ehrenfeucht-Fraïssé goes elementarily automatic for structures of bounded degree. In STACS, volume 14 of LIPIcs, pages 242-253. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2012. [ bib | .pdf ]
Antoine Durand-Gasselin and Peter Habermehl. On the Use of Non-deterministic Automata for Presburger Arithmetic. In CONCUR, volume 6269 of Lecture Notes in Computer Science, pages 373-387. Springer, 2010. [ bib | .pdf ]


Antoine Durand-Gasselin. Automata based logics for program verification. Defended on 03/12/2013. LIAFA, Université Paris Diderot & CNRS. Peter Habermehl and Ahmed Bouajjani, advisors. [.pdf ]

A picture of me

A picture of me

Contact Information

antoine.durand-gasselin `at`

Office location
609 (building TPR1, 6th floor, entrance G)

Laboratoire d’Informatique Fondamentale,
Parc Scientifique de Luminy,
163 avenue de Luminy - Case 901,
F-13288 Marseille Cedex 9, France