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.


I am looking for a post-doc 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 open-access 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 error-prone 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 input-output examples. We investigate how to augment probabilistic and neural program synthesis methods with new search algorithms, proposing a framework called distribution-based 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 machine-learned 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 NP-hardness 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 well-characterize 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] Assume-Guarantee 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

    Prompt-LTL extends Linear Temporal Logic with a bounded version of the eventually operator to express temporal requirements such as bounding waiting times. We study assume-guarantee synthesis for prompt-LTL: the goal is to construct a system such that for all environments satisfying a first prompt-LTL formula (the assumption) the system composed with this environment satisfies a second prompt-LTL 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 2-EXPTIME-complete.

  • [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 multi-agent 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 Bounded-Outcome 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 model-checking problems for both these logics.

Games on graphs

Games on graphs is at the intersection of several fields: verification (model-checking 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 Goubault-Larrecq, 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: Quasi-polynomial 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 quasi-polynomial 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 quasi-polynomial 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 polynomial-time 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 quasi-polynomial 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 context-free 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 (top-down) PCFGs which we call a bottom-up weighted context-free 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 non-deterministic 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 co-Büchi acceptance condition. This result has two direct consequences: the undecidability of monadic second-order logic extended with the qualitative path-measure quantifier, and the undecidability of the emptiness problem for alternating tree automata with non-zero 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 well-studied 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 multi-objective 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 quasi-polynomial time algorithm for the emptiness problem for 2-ambiguous 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 EXPTIME-complete 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 max-flow min-cut 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 trace-refinement 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 trace-equivalent. 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 trace-refinement 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 trace-refinement 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 game-theoretic 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., non-reachability) 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 Time-Invariant Systems abstract ++ technical report

    Nathanaël Fijalkow, Joël Ouaknine, Amaury Pouly, João Sousa-Pinto, and James Worrell

    International Conference on Hybrid Systems: Computation and Control, HSCC'19

    We consider the decidability of state-to-state reachability in linear time-invariant control systems, with control sets defined by boolean combinations of linear inequalities. Decidability of the sub-problem 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 sets---unions of two affine subspaces and bounded convex polytopes respectively---and 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 Kannan-Lipton 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 non-reachability. 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 closure-complete: there exists a closed semialgebraic invariant if and only if y is not in the topological closure of the orbit of x under A.



  • 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)