POSTDOC POSITION In BRUSSELS (Theory of transducers)

ARC PROJECT TRANSFORM: Theoretical Foundations of Transformations


The theories of automata, languages, and their connections with logics have now reached a high maturity level, and have found many applications, for instance in model-checking and synthesis of reactive systems. For such systems, data processing aspects can be usually neglected. However, a finer abstraction than languages is necessary to reason about computer systems that transform data, such as string, list or stream processing programs.

A transformation is a function from (finite or infinite) words to words. Transducers are state-based models of transformations, that extend automata with an output mechanism. Finite state transducers have been studied since the 60s and many important results have been obtained. More recently, there has been a renewed interest in more expressive transducer models for transformations: two-way finite state transducers and transducers with registers, introduced in 2009 by Alur and Cerny. These models have the same expressive power as monadic second-order translations (MSOT), a logic-based formalism to express transformations of logical structures, introduced by Courcelle.

The goal of this project is to advance substantially the theory of MSOT-expressive transformations, by lifting to transformations important and impactful results from formal language theory. An objective is to characterise precisely classes of transformations: computationally,
logically, and algebraically. This project also targets a novel application, the automatic synthesis of word-processing programs, as a generalisation of reactive system synthesis. Finally, extensions to other data structures, such as streams and trees will be envisaged.

This project is a three years project funded by the French-speaking community of Belgium, and headed by Emmanuel Filiot, who is FNRS associate researcher at Université Libre de Bruxelles.


Candidates should hold a PhD thesis, or defend it soon, and have a strong background in theoretical computer science, in particular automata theory. Some knowledge in transducer theory is appreciated.

The hired candidate will work on theoretical research questions, will participate to seminars, and will interact with other members of the research group, including PhD students.


The wage is a bit more than 2,000 euros a month, after all taxes. Enrollment to the Belgian national health insurance scheme is included.


Université Libre de Bruxelles, Brussels, Belgium. Formal methods and verification group (


The starting date of the position is to be decided with the applicant, but preferably before September 2015.
The duration is preferably two years, but also subject to discussion.


The applicants should send in electronic form:
• a Curriculum Vitae
• title and summary of the PhD
• list of publications
• the names and contact details (institution, e-mail address and phone number) of two referees.
• a covering letter explaining how the candidates meets the requirements

The applications should be sent by e-mail to Emmanuel Filiot ( by Feb 15.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s