Antoine DurandGasselin
Since September 2015, I am a postdoc at École Centrale Marseille
(where I teach) and Université AixMarseille (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 nonelementary 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 twoway 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.
Publications
Conference Proceedings

[DGH16]

Antoine DurandGasselin and Peter Habermehl.
Regular transformations of data words through origin information.
In FoSSaCS, volume 9634 of Lecture Notes in Computer Science, pages 285300. Springer, 2016.
[ bib 
.pdf ]

[DEGM15]

Antoine DurandGasselin, Javier Esparza, Pierre Ganty and Rupak Majumdar.
Model Checking Parameterized Asynchronous SharedMemory Systems.
In CAV, volume 9206 of Lecture Notes in Computer Science, pages 6784. Springer, 2015.
[ bib 
.pdf ]

[ADGT13]

Rajeev Alur, Antoine DurandGasselin, and Ashutosh Trivedi.
From Monadic SecondOrder Definable String Transformations to Transducers.
In LICS, pages 458467. IEEE Computer Society, 2013.
[ bib 
.pdf ]

[DGH12]

Antoine DurandGasselin and Peter Habermehl.
EhrenfeuchtFraïssé goes elementarily automatic for
structures of bounded degree.
In STACS,
volume 14 of LIPIcs, pages 242253. Schloss Dagstuhl  LeibnizZentrum
fuer Informatik, 2012.
[ bib 
.pdf ]

[DGH10]

Antoine DurandGasselin and Peter Habermehl.
On the Use of Nondeterministic Automata for Presburger Arithmetic.
In CONCUR,
volume 6269 of Lecture Notes in Computer Science, pages 373387.
Springer, 2010.
[ bib 
.pdf ]
Thesis

[DG13]

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