I am a computer scientist working on games, machine learning, automata, and dynamical systems. 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.
I am the principal investigator of the DeepSynth project (Momentum 2019 -- 2021) whose goal is to combine formal methods and machine learning for program synthesis.
Check out my research blog Games automata play!
Selected (recent) works by topic
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.
Short presentation video (15mn) of the DeepSynth Momentum project: machine learning guided program synthesis.
Nathanaël Fijalkow and Guillaume Lagarde
European Conference on Artificial Intelligence, ECAI'20Program 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.
Judith Clymo, Haik Manukian, Nathanaël Fijalkow, Adrià Gascón, and Brooks Paige
International Conference on Artificial Intelligence and Statistics, AI&STAT'20Programming 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 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.
Antonio Casares, Thomas Colcombet, and Nathanaël Fijalkow
International Colloquium on Automata, Languages and Programming, ICALP'21In 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.
Nathanaël Fijalkow, Bastien Maubert, and Moshe Y. Vardi
International Joint Conference on Artificial Intelligence, IJCAI'20Prompt-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.
Nathanaël Fijalkow, Bastien Maubert, and Sasha Rubin
Computer Science Logic, CSL'18Program 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).
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.
Invited talk for the International Symposium on Games, Automata, Logics, and Formal Verification, GanDALF'19
Wojciech Czerwiński, Laure Daviaud, Nathanaël Fijalkow, Marcin Jurdziński, Ranko Lazić, and Paweł Parys
Symposium On Discrete Algorithms, SODA'19Several 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'21Learning 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.
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 LogicsWe 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.
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'17Probabilistic 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.
Automata column in SIGLOG newsThe 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.
Thomas Colcombet, Nathanaël Fijalkow, and Pierre Ohlmann
Submitted to 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'20Bertrand 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.
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'16Given 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.
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'17Logical 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.
Mathias Ruggaard Pedersen, Nathanaël Fijalkow, Giorgio Bacci, Kim Guldstrand Larsen, and Radu Mardare
Language and Automata Theory and Applications, LATA'18Semi-Markov processes are Markovian processes in which the firing time of transitions is modelled by probabilistic distributions over positive reals interpreted as the probability of firing a transition at a certain moment in time. In this paper we consider the trace-based semantics of semi-Markov processes, and investigate the question of how to compare two semi-Markov processes with respect to their time-dependent behaviour. To this end, we introduce the relation of being “faster than” between processes and study its algorithmic complexity. Through a connection to probabilistic automata we obtain hardness results showing in particular that this relation is undecidable. However, we present an additive approximation algorithm for a time-bounded variant of the faster-than problem over semi-Markov processes with slow residence-time functions, and a coNP algorithm for the exact faster-than problem over unambiguous semi-Markov processes.
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.
Nathanaël Fijalkow, Engel Lefaucheux, Pierre Ohlmann, Joël Ouaknine, Amaury Pouly, and James Worrell
International Static Analysis Symposium, SAS'19The 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.
Nathanaël Fijalkow, Joël Ouaknine, Amaury Pouly, João Sousa-Pinto, and James Worrell
International Conference on Hybrid Systems: Computation and Control, HSCC'19We 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.
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'17The 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.