Short bio
I am a computer scientist working on program synthesis, games, and automata. I am a junior researcher at CNRS in LaBRI, Bordeaux (chargé de recherche). I am also a research fellow of The Alan Turing Institute of data science and artificial intelligence in London. I defended my PhD in October 2015.
Curriculum vitae: short, short in French, long, and full publications list.
Latest
I am looking for a postdoc for two years, starting around October 2022 to work on Games for Synthesis. Please contact me for details!
I am serving as Managing Editor for the new journal TheoretiCS, a diamond openaccess journal dedicated to Theoretical Computer Science. Please submit your best work!
I will be defending my habilitation on 11 Feb 2022.
Selected (recent) works by topic
Program synthesis
The conception of computer programs is a complicated, costly, and errorprone task. Program synthesis is an ideal where the program is automatically generated from its specification. I am particularly interested programming by example where the specification is given by a set of input and output pairs.

[FLOE21] DeepSynth: a general purpose program synthesizer abstract ++ technical report ++ Github repository ++ short presentation video (15mn)
Nathanaël Fijalkow, Guillaume Lagarde, Théo Matricon, Kevin Ellis, Pierre Ohlmann, and Akarsh Potta
AAAI Conference on Artificial Intelligence, AAAI'22
We consider the problem of automatically constructing computer programs from inputoutput examples. We investigate how to augment probabilistic and neural program synthesis methods with new search algorithms, proposing a framework called distributionbased search. Within this framework, we introduce two new search algorithms: Heap Search, an enumerative method, and SQRT Sampling, a probabilistic method. We prove certain optimality guarantees for both methods, show how they integrate with probabilistic and neural techniques, and demonstrate how they can operate at scale across parallel compute environments. Collectively these findings offer theoretical and applied studies of search algorithms for program synthesis that integrate with recent developments in machinelearned program synthesizers. 
[FL21] The complexity of learning linear temporal formulas from examples abstract++ technical report ++ official publication webpage (includes a video presentation)
Nathanaël Fijalkow and Guillaume Lagarde
International Conference on Grammatical Inference, ICGI'21
In this paper we initiate the study of the computational complexity of learning linear temporal logic (LTL) formulas from examples. We construct approximation algorithms for fragments of LTL and prove hardness results; in particular we obtain tight bounds for the fragment containing only the next operator and conjunctions, and prove NPhardness results for many fragments. 
[FL20] Tutorial on Machine Learning Guided Program Synthesis abstract ++ dedicated webpage and slides ++ half hour video presentation (seminar talk at the citAI seminar series)
Nathanaël Fijalkow and Guillaume Lagarde
European Conference on Artificial Intelligence, ECAI'20
Program synthesis is an ideal where the program is automatically generated from its specification. It has recently gained momentum thanks to the use of machine learning techniques. In this tutorial we will survey the recent line of work using machine learning for improving program search algorithms. 
[CMFGP20] Data Generation for Neural Programming by Example abstract ++ open access link ++ Github repository ++ slides
Judith Clymo, Haik Manukian, Nathanaël Fijalkow, Adrià Gascón, and Brooks Paige
International Conference on Artificial Intelligence and Statistics, AI&STAT'20
Programming by example is the problem of synthesizing a program from a small set of input / output pairs. Recent works applying machine learning methods to this task show promise, but are typically reliant on generating synthetic examples for training. A particular challenge lies in generating meaningful sets of inputs and outputs, which wellcharacterize a given program and accurately demonstrate its behavior. Where examples used for testing are generated by the same method as training data then the performance of a model may be partly reliant on this similarity. In this paper we introduce a novel approach using an SMT solver to synthesize inputs which cover a diverse set of behaviors for a given program. We carry out a case study comparing this method to existing synthetic data generation procedures in the literature, and find that data generated using our approach improves both the discriminatory power of example sets and the ability of trained machine learning models to generalize to unfamiliar data.
Controller synthesis
Controller synthesis is the special case of program synthesis where the program takes actions over time in a partially controllable environment. I focus on temporal synthesis, where the specification is given by a logical formula in linear temporal logic (LTL) and its extensions.

[CCF21] Optimal transformations of Muller conditions abstract ++ technical report ++ conference version
Antonio Casares, Thomas Colcombet, and Nathanaël Fijalkow
International Colloquium on Automata, Languages and Programming, ICALP'21
In this paper, we are interested in automata over infinite words and infinite duration games, that we view as general transition systems. We study transformations of systems using a Muller condition into ones using a parity condition, extending Zielonka's construction. We introduce the alternating cycle decomposition transformation, and we prove a strong optimality result: for any given deterministic Muller automaton, the obtained parity automaton is minimal both in size and number of priorities among those automata admitting a morphism into the original Muller automaton. We give two applications. The first is an improvement in the process of determinisation of Büchi automata into parity automata by Piterman and Schewe. The second is to present characterisations on the possibility of relabelling automata with different acceptance conditions. 
[FMV20] AssumeGuarantee Synthesis for Prompt Linear Temporal Logic abstract ++ open access link ++ slides ++ 15mn presentation video
Nathanaël Fijalkow, Bastien Maubert, and Moshe Y. Vardi
International Joint Conference on Artificial Intelligence, IJCAI'20
PromptLTL extends Linear Temporal Logic with a bounded version of the eventually operator to express temporal requirements such as bounding waiting times. We study assumeguarantee synthesis for promptLTL: the goal is to construct a system such that for all environments satisfying a first promptLTL formula (the assumption) the system composed with this environment satisfies a second promptLTL formula (the guarantee). This problem has been open for a decade. We construct an algorithm for solving it and show that, like classical LTL synthesis, it is 2EXPTIMEcomplete. 
[FMMR18] Quantifying Bounds in Strategy Logic abstract ++ open access link
Nathanaël Fijalkow, Bastien Maubert, and Sasha Rubin
Computer Science Logic, CSL'18
Program synthesis constructs programs from specifications in an automated way. Strategy Logic (SL) is a powerful and versatile specification language whose goal is to give theoretical foundations for program synthesis in a multiagent setting. One limitation of Strategy Logic is that it is purely qualitative. For instance it cannot specify quantitative properties of executions such as "every request is quickly granted", or quantitative properties of trees such as "most executions of the system terminate". In this work, we extend Strategy Logic to include quantitative aspects in a way that can express bounds on "how quickly" and "how many". We define Prompt Strategy Logic, which encompasses Prompt LTL (itself an extension of LTL with a prompt eventuality temporal operator), and we define BoundedOutcome Strategy Logic which has a bounded quantifier on paths. We supply a general technique, based on the study of automata with counters, that solves the modelchecking problems for both these logics.
Games on graphs
Games on graphs is at the intersection of several fields: verification (modelchecking games such as parity games), logic and model theory (Ehrenfeucht–Fraïssé games), automata theory (emptiness and acceptance games), reinforcement learning (Markov decision processes), and optimisation (mean payoff and discounted games).

[CFGO21] The Theory of Universal Graphs for Infinite Duration Games abstract ++ technical report
Thomas Colcombet, Nathanaël Fijalkow, Paweł Gawrychowski, and Pierre Ohlmann
Submitted journal paper, subsumes the two technical reports (the first on universal trees and the second on universal graphs), the FoSSaCS'19 invited talk paper, and the MFCS'20 paper on mean payoff games.
We introduce the notion of universal graphs as a tool for constructing algorithms solving games of infinite duration such as parity games and mean payoff games. In the first part we develop the theory of universal graphs, with two goals: showing an equivalence and normalisation result between different recently introduced related models, and constructing generic value iteration algorithms for any positionally determined objective. In the second part we give four applications: to parity games, to mean payoff games, and to combinations of them (in the form of disjunctions of objectives). For each of these four cases we construct algorithms achieving or improving over the best known time and space complexity. 
[AFGLO21] The Theory of Universal Graphs for Infinite Duration Games abstract ++ technical report
Ashwani Anand, Nathanaël Fijalkow, Aliénor GoubaultLarrecq, Jérôme Leroux, and Pierre Ohlmann
International Symposium on Games, Automata, Logics, and Formal Verification, GanDALF'21
The notion of separating automata was introduced by Bojanczyk and Czerwinski for understanding the first quasipolynomial time algorithm for parity games. In this paper we show that separating automata is a powerful tool for constructing algorithms solving games with combinations of objectives. We construct two new algorithms: the first for disjunctions of parity and mean payoff objectives, matching the best known complexity, and the second for disjunctions of mean payoff objectives, improving on the state of the art. In both cases the algorithms are obtained through the construction of small separating automata, using as black boxes the existing constructions for parity objectives and for mean payoff objectives. 
[Fij19] Parity games: the quasipolynomial era slides ++ blog post
Nathanaël Fijalkow
Invited talk for the International Symposium on Games, Automata, Logics, and Formal Verification, GanDALF'19

[CDFJLP19] Universal trees grow inside separating automata: Quasipolynomial lower bounds for parity games abstract ++ technical report
Wojciech Czerwiński, Laure Daviaud, Nathanaël Fijalkow, Marcin Jurdziński, Ranko Lazić, and Paweł Parys
Symposium On Discrete Algorithms, SODA'19
Several distinct techniques have been proposed to design quasipolynomial algorithms for solving parity games since the breakthrough result of Calude, Jain, Khoussainov, Li, and Stephan (2017): play summaries, progress measures and register games. We argue that all those techniques can be viewed as instances of the separation approach to solving parity games, a key technical component of which is constructing (explicitly or implicitly) an automaton that separates languages of words encoding plays that are (decisively) won by either of the two players. Our main technical result is a quasipolynomial lower bound on the size of such separating automata that nearly matches the current best upper bounds. This forms a barrier that all existing approaches must overcome in the ongoing quest for a polynomialtime algorithm for solving parity games. The key and fundamental concept that we introduce and study is a universal ordered tree. The technical highlights are a quasipolynomial lower bound on the size of universal ordered trees and a proof that every separating safety automaton has a universal tree hidden in its state space.
Learning and control of probabilistic automata
The study of probabilistic automata, in particular algorithms for learning and controlling them, has many applications, including program verification, natural language processing, modelling of biological systems, and machine learning.

[CF20] Consistent unsupervised estimators for anchored PCFGs abstract ++ open access link ++ extended abstract in the Proceedings of the Society for Computation in Linguistics ++ Github repository
Alexander Clark and Nathanaël Fijalkow
Transactions of the Association for Computational Linguistics, TaCL, invited for presentation at the Conference on Empirical Methods in Natural Language Processing, EMNLP'20, and for the Society for Computation in Linguistics, SCiL'21
Learning probabilistic contextfree grammars from strings is a classic problem in computational linguistics since Horning (1969). Here we present an algorithm based on distributional learning that is a consistent estimator for a large class of PCFGs that satisfy certain natural conditions including being anchored (Stratos et al., 2016). We proceed via a reparameterisation of (topdown) PCFGs which we call a bottomup weighted contextfree grammar. We show that if the grammar is anchored and satisfies additional restrictions on its ambiguity, then the parameters can be directly related to distributional properties of the anchoring strings; we show the asymptotic correctness of a naive estimator and present some simulations using synthetic data that show that algorithms based on this approach have good finite sample behaviour. 
[BFF+21] Alternating Tree Automata with Qualitative Semantics abstract ++ technical report
Raphaël Berthon, Nathanaël Fijalkow, Emmanuel Filiot, Shibashis Guha, Bastien Maubert, Aniello Murano, Laureline Pinault, Sophie Pinchinat, Sasha Rubin, and Olivier Serre
ACM Transactions on Computational Logics (ToCL)
We study alternating automata with qualitative semantics over infinite binary trees: alternation means that two opposing players construct a decoration of the input tree called a run, and the qualitative semantics says that a run of the automaton is accepting if almost all branches of the run are accepting. In this paper we prove a positive and a negative result for the emptiness problem of alternating automata with qualitative semantics. The positive result is the decidability of the emptiness problem for the case of Büchi acceptance condition. An interesting aspect of our approach is that we do not extend the classical solution for solving the emptiness problem of alternating automata, which first constructs an equivalent nondeterministic automaton. Instead, we directly construct an emptiness game making use of imperfect information. The negative result is the undecidability of the emptiness problem for the case of coBüchi acceptance condition. This result has two direct consequences: the undecidability of monadic secondorder logic extended with the qualitative pathmeasure quantifier, and the undecidability of the emptiness problem for alternating tree automata with nonzero semantics, a recently introduced probabilistic model of alternating tree automata. 
[FRW20] Probabilistic Automata of Bounded Ambiguity abstract ++ technical report ++ slides
Nathanaël Fijalkow, Cristian Riveros and James Worrell
Information and Computation, special issue on "Weighted Automata", also presented in the conference International Conference on Concurrency Theory, CONCUR'17
Probabilistic automata are an extension of nondeterministic finite automata in which transitions are annotated with probabilities. Despite its simplicity, this model is very expressive and many of the associated algorithmic questions are undecidable. In this work we focus on the emptiness problem (and its variant the value problem), which asks whether a given probabilistic automaton accepts some word with probability greater than a given threshold. We consider a natural and wellstudied structural restriction on automata, namely the degree of ambiguity, which is defined as the maximum number of accepting runs over all words. The known undecidability proofs exploits infinite ambiguity and so we focus on the case of finitely ambiguous probabilistic automata.
Our main contributions are to construct efficient algorithms for analysing finitely ambiguous probabilistic automata through a reduction to a multiobjective optimisation problem called the stochastic path problem. We obtain a polynomial time algorithm for approximating the value of probabilistic automata of fixed ambiguity and a quasipolynomial time algorithm for the emptiness problem for 2ambiguous probabilistic automata.
We complement these positive results by an inapproximability result stating that the value of finitely ambiguous probabilistic automata cannot be approximated unless P = NP. 
[Fij17] Undecidable problems for probabilistic automata abstract ++ SIGLOG bulletin
Nathanaël Fijalkow
Automata column in SIGLOG news
The model of probabilistic automata was introduced by Rabin in 1963. Ever since, undecidability results were obtained for this model, showing that although simple, it is very expressive. This paper provides streamlined constructions implying the most important negative results, including the celebrated inapproximability result of Condon and Lipton.
Algorithms for Markovian models
Markovian models are stochastic models with a memoryless dynamics. The distinction with probabilistic automata is that Markovian models such as Markov decision processes are fully observable.

[CF020] Controlling a random population abstract ++ journal version ++ conference version (open access link) ++ blog post
Thomas Colcombet, Nathanaël Fijalkow, and Pierre Ohlmann
Logical Methods in Computer Science (LMCS), special issue by invitation, also presented at the International Conference on Foundations of Software Science and Computation Structures, FoSSaCS'20
Bertrand et al. introduced a model of parameterised systems, where each agent is represented by a finite state system, and studied the following control problem: for any number of agents, does there exist a controller able to bring all agents to a target state? They showed that the problem is decidable and EXPTIMEcomplete in the adversarial setting, and posed as an open problem the stochastic setting, where the agent is represented by a Markov decision process. In this paper, we show that the stochastic control problem is decidable. Our solution makes significant uses of well quasi orders, of the maxflow mincut theorem, and of the theory of regular cost functions. 
[FKS20] Trace Refinement in Labelled Markov Decision Processes abstract ++ open access link
Nathanaël Fijalkow, Stefan Kiefer, and Mahsa Shirmohammadi
Logical Methods in Computer Science (LMCS), also presented in the conference Foundations of Software Science and Computation Structures, FoSSaCS'16
Given two labelled Markov decision processes (MDPs), the tracerefinement problem asks whether for all strategies of the first MDP there exists a strategy of the second MDP such that the induced labelled Markov chains are traceequivalent. We show that this problem is decidable in polynomial time if the second MDP is a Markov chain. The algorithm is based on new results on a particular notion of bisimulation between distributions over the states. However, we show that the general tracerefinement problem is undecidable, even if the first MDP is a Markov chain. Decidability of those problems was stated as open in 2008. We further study the decidability and complexity of the tracerefinement problem provided that the strategies are restricted to be memoryless. 
[CFKP19] Expressiveness of probabilistic modal logics: A gradual approach abstract ++ official journal link
Florence Clerc, Nathanaël Fijalkow, Bartek Klin, and Prakash Panangaden
Information and Computation, also presented in the conference International Colloquium on Automata, Languages and Programming, ICALP'17
Logical characterizations of probabilistic bisimulation and simulation for Labelled Markov Processes were given by Desharnais et al. These results hold for systems defined on analytic state spaces and assume countably many labels in the case of bisimulation and finitely many labels in the case of simulation.
We revisit these results by giving simpler and more streamlined proofs. In particular, our proof for simulation has the same structure as the one for bisimulation, relying on a new result of a topological nature. We also propose a new notion of event simulation.
Our proofs assume countably many labels, and we show that the logical characterization of bisimulation may fail when there are uncountably many labels. However, with a stronger assumption on the transition functions (continuity instead of just measurability), we regain the logical characterization result for arbitrarily many labels. These results arose from a gametheoretic understanding of probabilistic simulation and bisimulation.
Invariants for linear dynamical systems
A dynamical system follows the evolution of a point through repeated applications of a function; the special case of linear dynamical systems is concerned with linear functions, i.e. multiplication by a matrix. Their algorithmic study is deeply intertwined with deep insights from algebraic number theory and geometry, and many very natural problems remain unsolved. I am particularly interested in invariants for linear dynamical systems, and in related control problems.

[FLOOPW19] On the Monniaux Problem in Abstract Interpretation abstract ++ technical report
Nathanaël Fijalkow, Engel Lefaucheux, Pierre Ohlmann, Joël Ouaknine, Amaury Pouly, and James Worrell
International Static Analysis Symposium, SAS'19
The Monniaux Problem in abstract interpretation asks, roughly speaking, whether the following question is decidable: given a program P, a safety (e.g., nonreachability) specification phi, and an abstract domain of invariants D, does there exist an inductive invariant I in D guaranteeing that program P meets its specification phi. The Monniaux Problem is of course parameterised by the classes of programs and invariant domains that one considers. In this paper, we show that the Monniaux Problem is undecidable for unguarded affine programs and semilinear invariants (unions of polyhedra). Moreover, we show that decidability is recovered in the important special case of simple linear loops. 
[FOPSW19] On the Decidability of Reachability in Linear TimeInvariant Systems abstract ++ technical report
Nathanaël Fijalkow, Joël Ouaknine, Amaury Pouly, João SousaPinto, and James Worrell
International Conference on Hybrid Systems: Computation and Control, HSCC'19
We consider the decidability of statetostate reachability in linear timeinvariant control systems, with control sets defined by boolean combinations of linear inequalities. Decidability of the subproblem in which control sets are linear subspaces is a fundamental result in control theory. We first show that reachability is undecidable if the set of controls is a finite union of affine subspaces. We then consider two simple subclasses of control setsunions of two affine subspaces and bounded convex polytopes respectivelyand show that in these two cases the reachability problem for LTI systems is as hard as certain longstanding open decision problems concerning linear recurrence sequences. Finally we present some spectral assumptions on the transition matrix of an LTI system under which reachability becomes decidable with bounded convex polytopes as control sets. 
[FOOPW19] Complete Semialgebraic Invariant Synthesis for the KannanLipton Orbit Problem abstract ++ technical report
Nathanaël Fijalkow, Pierre Ohlmann, Joël Ouaknine, Amaury Pouly and James Worrell
Theory of Computing Systems (ToCS), special issue by invitation, also published in the Symposium on Theoretical Aspects of Computer Science, STACS'17
The Orbit Problem consists of determining, given a linear transformation A on Q^d, together with vectors x and y, whether the orbit of x under repeated applications of A can ever reach y. This problem was famously shown to be decidable by Kannan and Lipton in the 1980s.
In this paper, we are concerned with the problem of synthesising suitable invariants P included in R^d, i.e., sets that are stable under A and contain x and not y, thereby providing compact and versatile certificates of nonreachability. We show that whether a given instance of the Orbit Problem admits a semialgebraic invariant is decidable, and moreover in positive instances we provide an algorithm to synthesise suitable invariants of polynomial size.
Our results imply that the class of closed semialgebraic invariants is closurecomplete: there exists a closed semialgebraic invariant if and only if y is not in the topological closure of the orbit of x under A.
Supervision
Current
 Théo Matricon (PhD, jointly supervised with Laurent Simon)
 Rémi Morvan (PhD, jointly supervised with Diego Figuera and Marcin Jurdzinski)
 Antonio Casares (PhD, jointly supervised with Thomas Colcombet and Igor Walukiewicz)
 Ritam Raha (PhD jointly supervised with Guillermo Pérez, Jérôme Leroux, and Floris Geerts)
Former
 Pierre Ohlmann (PhD jointly supervised with Olivier Serre, now postdoc in University of Warsaw)
 Guillaume Lagarde (postdoc 2019  2021, now research engineer at Criteo AI Lab)