Lucie Callens
email: lucie.callens@irisa.fr

Guy Carrault
email: guy.carrault@univ-rennes1.fr

Marie-Odile Cordier
email: marie-odile.cordier@irisa.fr

Elisa Fromont
email: elisa.fromont@cs.kuleuven.be

Franc ¸ois Portet
email: fportet@abdn.ac.uk

René Quiniou
email: rene.quiniou@irisa.fr

Intelligent adaptive monitoring for cardiac surveillance

Monitoring patients in intensive care units is a critical task. Simple condition detection is generally insufficient to diagnose a patient and may generate many false alarms to the clinician operator. Deeper knowledge is needed to discriminate among alarms those that necessitate urgent therapeutic action. We propose an intelligent monitoring system that makes use of many artificial intelligence techniques: artificial neural networks for temporal abstraction, temporal reasoning, model based diagnosis, decision rule based system for adaptivity and machine learning for knowledge acquisition. To tackle the difficulty of taking context change into account, we introduce a pilot aiming at adapting the system behavior by reconfiguring or tuning the parameters of the system modules. A prototype has been implemented and is currently experimented and evaluated. Some results, showing the benefits of the approach, are given.

INTRODUCTION

Monitoring means to process incoming data (signals) recorded by sensors in order to recognize alarming conditions. Such devices may generate alarms in huge volume that can overwhelm an operator who has to validate the alarms and take therapeutic actions. What the operator really needs is a decision support system that could help him decide whether an alarm needs some action or can be skipped safely. In the 1980's the concept of kwnowledge based system emerged with the aim to associate deep knowledge to diagnosis. An intelligent monitoring system integrates such a knowledge-based system into a monitoring system.

The first step of intelligent monitoring is temporal abstraction. This means transforming numerical time series into symbolic event sequences. There is a huge literature in this domain (for surveys see [START_REF] Stacey | Temporal abstraction in intelligent clinical data analysis: A survey[END_REF][START_REF] Lavrac | Intelligent data analysis for medical diagnosis: Using machine learning and temporal abstraction[END_REF]), e.g. in the cardiac domain. The second step is devoted to the reasoning task. Among proposals, model-based diagnosis [START_REF] Reiter | A theory of diagnosis from first principles[END_REF][START_REF] De Kleer | Characterizing diagnoses and systems[END_REF] has the main avantage of using an explicit model that can be used to diagnose the series of events observed during monitoring as well as giving comprehensible explanations to the operator. As diseases have an important temporal dimension, we have proposed to represent them by sets of events linked by temporal constraints on their occurrences. Such sets of events are called chronicles [START_REF] Dousson | Situation recognition: representation and algorithms[END_REF]. They can model (a faulty model, in this case) the evolution of a disease during time or local typical temporal phenomena, e.g. typical wave sequences of an electrocardiogram (ECG) that represent cardiac beats characteristic of some rhythm problem. Their recognition on an input stream is based on efficient processing of temporal constraint networks [START_REF] Dechter | Temporal constraint networks[END_REF]. This makes chronicles good candidates for monitoring.

One of the main challenge of temporal abstraction in intelligent monitoring systems is to closely couple signal processing tasks and higher level tasks involved in diagnosis. One source of difficulty is that, generally, recorded data are highly dynamic and subject to changes. For example, the patient may move letting some sensor transmit very noisy data. Also, the patient state may evolve quickly due to the effect of some drug or disease evolution. We propose to introduce a central module called a pilot that analyzes continuously the monitoring context, i.e. the nature and quality of signals as well as the hypotheses devised by the diagnosis module. The aim of the pilot is to select the best signal processing algorithms and the right abstraction level for data abstraction. The pilot makes use of decision rules in order to bring high flexibility for taking into account new monitoring conditions or new monitoring domains.

The major bottleneck of knowledge based approaches is knowledge acquisition and maintenance. Machine learning has been advocated for this task. Since monitored diseases have a temporal relational dimension, first order models are good candidates for knowledge representation. This is why we have used Inductive Logic Programming [START_REF] Muggleton | Inductive Logic Programming: Theory and methods[END_REF] for learning chronicles. Devising decision rules for the pilot could also be tedious and time consuming [START_REF] Portet | Evaluation of real-time QRS detection algorithms in variable contexts[END_REF]. We have proposed decision tree learning for inducing decision rules from the performance of algorithms in a representative set of contexts.

Stacey and McGregor's survey [START_REF] Stacey | Temporal abstraction in intelligent clinical data analysis: A survey[END_REF] lists many intelligent monitoring systems that share several objectives and features with ours. To cite a few, R ÉSUM É [START_REF] Shahar | Knowledge-based temporal abstraction in clinical domains[END_REF], VIE-VENT [START_REF] Miksch | Utilizing temporal data abstraction for data validation and therapy planning for artificially ventilated newborn infants[END_REF] and its successors like ASGAARD [START_REF] Shahar | The Asgaard project: a taskspecific framework for the application and critiquing of time-oriented clinical guidelines[END_REF] have introduced general knowledge representation paradigms for temporal abstraction with a deep integration of domain knowledge. VIE-VENT could process data streams whereas R ÉSUM É was limited to databases. For efficiency reasons, instead of being general, our work focusses on cardiac knowledge in order to extract rich information from ECG or pressure signals online. From the temporal reasoning and diagnosis point of view, N ÉO-GANESH [START_REF] Dojat | Néoganesh: a working system for the automated control of assisted ventilation in ICUs[END_REF] shares the concept of temporal patterns, called scenarios, with our approach. In addition, we have proposed a supervised method to learn such temporal patterns automatically from annotated temporal data. In [START_REF] Karsai | An approach to self-adaptive software based on supervisory control[END_REF], a self-adaptive software is introduced to modify the processing chain according to some predefined events such as sensor loss. But this approach does not deal with high-level goals as temporal reasoning which is crucial for monitoring evolving systems. In ASGAARD [START_REF] Seyfang | Using time-oriented data abstraction methods to optimize oxygen supply for neonates[END_REF], the data abstraction module focusses on specific input sources according to a contextual plan which can be adapted when the processed inputs contradict expected values. However, data abstraction subtasks are scheduled in rigid sequences and diagnosis information is not used for adapting the current system. This article summarizes the work done during several years as an active collaboration with experts in biological signal processing and the department of cardiology of the local hospital and which led to the implementation of an experimental platform called Calicot. Section 2 describes the medical applicative context. In Section 3, an overall overview of the system architecture is given. In Sections 4 and 5, we present the temporal abstraction and diagnosis methods. In Section 6, a solution to adaptation to context change is detailed. Learning chronicles and decision rules are presented in Section 7. We provide some evaluation results in Section 8 before concluding.

APPLICATION DOMAIN: MONITORING CARDIAC PATIENTS

Several areas in medicine require monitoring and management, e.g. temporary paralysis of the respiratory center in the brain, renal damage, surgical anesthesia or myocardial infarction. In this latter case, our concern, intensive care units were initiated in the 60s, for monitoring the vital functions of a patient after a serious cardiac attack.

The main goal was to prevent, detect and control lethal arrhythmias by therapeutic actions. ECG signals are displayed to an operator and analyzed in real time: the trends of the main parameters, such as the cardiac frequency, are computed and alarms are generated. All this information assists the operator who is in charge of analyzing the situation, validating the alarms and deciding what action to perform.

The main problem is to abstract the signal observation to a pathological state through several steps [START_REF] Mora | Intelligent patient monitoring and management systems : A review[END_REF]: signal processing, alarm handling, therapy advising. To solve this it, intelligent supervision systems appeared in the 90's. Their aim was to integrate several sources of observation (numerical or symbolic) and several types of medical knowledge (surface and deep knowledge). Surface knowledge relies on the use of the so-called experiential knowledge while deep knowledge corresponds to a complete theory about a particular subject, from which all valid statements can be derived.

Recent developments have led to knowledge-based temporal abstraction (KBTA) where machine learning techniques are used to extract the most discriminating patterns which can be identified in normal and several pathological states. There is a wide literature about temporal abstraction in medical domains [START_REF] Lavrac | Intelligent data analysis for medical diagnosis: Using machine learning and temporal abstraction[END_REF][START_REF] Stacey | Temporal abstraction in intelligent clinical data analysis: A survey[END_REF]. The Calicot system [START_REF] Carrault | Temporal abstraction and inductive logic programming for arrhythmia recognition from ECG[END_REF], dedicated to cardiac arrhythmias detection, and the one proposed by Guimaraes [START_REF] Guimarães | A method for automated temporal knowledge acquisition applied to sleep-related breathing disorders[END_REF] which is focused to sleep-related respiratory disorders are two examples. Collaborative knowledge discovery approaches exploiting the properties of multi-agent systems (open character, autonomy of its components) have been proposed recently [START_REF] Guyet | Knowledge construction from time series data using a collaborative exploration system[END_REF] for the exploration of mechanical ventilation asynchronies.

ARCHITECTURE

Calicot has two execution modes: offline and online. The online mode, depicted in Fig. 1, is devoted to monitoring and adopts a pattern-matching approach: multivariate signals are first abstracted in series of symbolic timestamped events and then a matcher attempts to recognize, on the fly, instances of chronicles in the symbolic series. A chronicle associated to some cardiac disease is a temporal signature of this disease. The offline mode is dedicated to learning and updating the decision rule base and the chronicle base.

Contextual information is of great importance for monitoring. On the one hand, by taking the signal quality (noise) into account one can decide more accurately which is the most relevant signal processing algorithm to use in the current situation. On the other hand, by taking the patient state into account one can decide more accurately which are the relevant chronicles. Moreover, these two decisions are not independent: it can be the case that input signals are so noisy that it is useless to try to detect P-waves, for example. Consequently, chronicles that contain P-wave events can't be recognized and should be removed from the candidate set. Also, in the context of a particular disease, some types of event could be absent from the set of candidate chronicles and so it is useless to execute costly signal processing algorithms for detecting their related waves. Thus, low (signal processing) and high (chronicle recognition) level computations should be tightly coupled. This is why we opt for an adaptive architecture.

On the one hand, a signal processing library containing many signal processing algorithms was built. Their performance have been assessed in many contexts to determine when and how to run them. On the other hand, a chronicle abstraction hierarchy was defined: more abstract chronicles contains less event types and/or less event attributes which makes them more relevant to more noisy contexts. More specific chronicles are relevant for situations where the detection of particular events could improve the diagnosis accuracy. The decisions are taken by a central monitor (that we call a pilot) which analyzes continuously the signal and the patient context to determine the best signal processing task and algorithm to execute as well as the related chronicle abstraction level. A centralized control was adopted because it was simpler to specify via decision rules.

DATA ABSTRACTION

The temporal abstraction step transforms the numerical series into symbolic event sequences that are easier to process for high-level diagnosis. In coronary care units, the main problem comes from the presence of different kinds of noise (slow baseline drift, high frequency noise, impulsive noise) and from the great variability of patient dependent patterns and which can change over time. For example, multiform premature ventricular beats can combine with permanent or intermittent left or right bundle branch block. The temporal abstraction level achieves two main tasks: QRS complex (ventricular activity) and P wave (auricular activity) detection and QRS classification. Many methods have been proposed for detecting the ventricular activity, i.e. QRSs. Each one fails in specific situations and each reacts differently to the many different QRS waveforms. Hence we retain several algorithms. The proposed approach is not to merge the decisions of several algorithms but to select, on line, the most promising detector according to its performance in similar contexts. Actually, seven algorithms were selected [START_REF] Portet | Evaluation of real-time QRS detection algorithms in variable contexts[END_REF].

Once a QRS has been detected it is labeled and a symbolic event is generated. The generation of its attribute values is based on the fact a beat can be efficiently represented by a compactly supported wavelet base [START_REF] Senhadji | Comparing wavelet transforms for recognizing cardiac patterns[END_REF]. Each QRS is then represented by a global extrema at each decomposed level. The QRS classification consists in labeling the beats into two mains classes, normal or abnormal. A probabilistic neural network (PNN) based on radial basis function has been used. P wave detection is very hard because it has a weak amplitude and a variable morphology. We retain the QRS-T interval cancellation technique to overcome the limitations window techniques (which assumes that a P wave always occurs before some QRS) and mainly to facilitate the detection of the P wave even for arrhythmias with A-V dissociation. The proposed approach [START_REF] Senhadji | Wavelet extrema representation for QRS-T cancellation and P wave detection[END_REF] mostly relies on: i) QRS-T interval detection and cancellation based on wavelet decomposition, ii) a statistical analysis of the residue for detecting P waves, not associated to a QRS, iii) an artificial neural network classifier to reject false detection which frequently occur in P wave detection.

DIAGNOSIS BY CHRONICLE RECOGNITION

In model-based diagnosis, a model of either normal or faulty behavior is used to detect and identify faults or diseases [START_REF] Reiter | A theory of diagnosis from first principles[END_REF][START_REF] De Kleer | Characterizing diagnoses and systems[END_REF]. If a normal behavioral model is used, the values reflecting the patient's state are fed into the model and the diagnoser generates an alarm if the model outputs are different from the values observed on the patient. With a faulty model, the diagnoser reasons abductively to generate disease hypotheses that could have produced the actual observations. Sometimes, such a model can be compiled into sets of discriminant patterns that can be efficiently searched for on the input stream. This method is very suited to online monitoring: the input stream is analyzed continuously and an alarm is emitted in case a set of events that can be related to a disease have been observed in some time window. In many situations, such as in the case of dynamic systems, time is crucial [START_REF] Cordier | Alarm driven monitoring based on chronicles[END_REF]. The events related to the course of a disease must happen in a specific order and have to respect delay constraints. Moreover, sometimes it is easier to describe a disease by a set of successive or synchronous events respecting temporal constraints than to extract discriminant features from a vector of values recorded by several sensors. This is true in the cardiac domain: the symptom related to some disease, e.g. bigeminy, is described more naturally by the properties of several cardiac beats than by the particular features of a QRS. Such temporal patterns can be easily represented by chronicles. Fig. 2 shows an example of chronicle related to bigeminy and an example of match on two types of signal.

Since the input data streams can be huge, recognizing chronicles on the fly must be very efficient. We have used a system called CRS (Chronicle Recognition System) [START_REF] Dousson | Alarm driven supervision for telecommunication networks. ii-on-line chronicle recognition[END_REF] which manages chronicle models, chronicle instances and temporal constraints between events from these instances. CRS tries to associate each incoming event with some uninstantiated event of a chronicle instance which satisfies the temporal constraints. It generates also new chronicle instances containing an event that can match the observed event. Many chronicle instances can be generated in such a way. One strength of CRS is its ability to prune instances, as early as possible, whenever one temporal constraint could not be satisfied by assessing whether an event occurence time has elapsed. This makes it particularly adapted for applications where the detection of critical situations is essential.

ADAPTATION

The architecture of Calicot shares many features with self adaptive systems [START_REF] Robertson | Model based diagnosis and contexts in self adaptive software[END_REF]. Since it is impossible to anticipate every situation and transition, decisions concerning parameter settings and the choice of tasks and algorithms to execute next are postponed to runtime. The goal of such software, is to monitor and control themselves. In our case, the system can be viewed as a metamonitor: a monitoring system, the pilot, monitors a monitoring system. The goal is to obtain the best performance by reconfiguring the system operations, precisely choosing alternate algorithms and chronicles sets. To each processing module, algorithm or chronicle set, is associated a description which describes the way this module can be used. For example, to a signal processing algorithm is associated the task that it can achieve, the objects (types of events) that it can deliver and features describing the contexts in which it should ensure the best performance.

The pilot receives continuously two kinds of contextual information: signal context, mainly related to the signal quality, and recognition information, related to the diagnosis state. Noise type and level, event detection rate and distribution are used to estimate the signal quality (signal analyzer in Fig. 1). Chronicle recognition rate, types of chronicles recognized so far and their distribution, expected patient state, etc. are used to estimate the diagnosis quality (arrhythmias analyzer in Fig. 1). From this contextual information the pilot has to decide whether the context has changed notably and a reconfiguration is needed. In this case, the pilot must select the best algorithms and tune their parameters as well as choose the right chronicle abstration level and the set of chronicles to be recognized.

To ensure a maximal flexibility and modularity, the pilot uses decision rules to decide when and how to perform reconfigurations. Here follows two examples of decision rules. The first one selects a detection algorithm, the second one selects the abstraction level that must be used for chronicles: if paced ∧ noiseType=muscular ∧ noiseLevel ≤ 0 dB then algo df2 if PWaveDetection is active ∧ QRSClassification is active then ab-stractionLevel=4

MACHINE LEARNING

In our approach machine learning is used at two stages, for learning chronicles and for learning decision rules for the pilot module. To establish accurate diagnoses efficiently the chronicles should be as discriminating as possible, i.e. they should clearly distinguish the diseases. However, the specification of discriminating chronicles is hard to do manually. Moreover, as first order (temporal) relations are concerned, we have chosen to use an ILP method. From examples describing symbolically signals related to disease episodes, ILP induces a set of first-order clauses that can discriminate the classes of the examples [START_REF] Muggleton | Inductive Logic Programming: Theory and methods[END_REF]. Fortunately, such a clause can be translated straightforwardly to a chronicle for CRS. By varying the language bias, i.e. the description language of examples and clauses, and using the related background knowledge, models at different abstraction levels can be learned. In addition, the model space is explored efficiently by searching only the most promising parts. We have also proposed a method for learning efficiently from multisource data [START_REF] Fromont | Learning rules from multisource data for cardiac monitoring[END_REF].

The goal of decision rules is to aid the pilot module select the best algorithm and chronicle set according to the current signal and patient context. We have used two approaches to devise such rules. The first one made use of PCA (Principal Component Analysis) to determine the most informative context attributes [START_REF] Portet | Evaluation of real-time QRS detection algorithms in variable contexts[END_REF] from performance data obtained by executing a set of signal processing algorithms in many situations with different kinds and level of noise and different diseases. Then, decision production rules conditioned by the selected attributes were built manually by experts. The second method used decision tree learning [START_REF] Portet | Learning decision tree for selecting QRS detectors for cardiac monitoring[END_REF]. From a similar set of performance data, decision trees were learnt. The nodes of such a tree represent a partition of the values of some attribute and the leaves represent a class, here an algorithm. Every path from the root node to some leave can be translated into a decision rule having as conditions the tests in the path nodes and as conclusion the algorithm in the leave. It is worthnoting that such learnt rules performed quite as well as expert rules.

EVALUATION

The Calicot prototype has been implemented in Java 7 . Its graphical interface displays monitored signals annotated with complex events related to recognized chronicles (see Fig. 3). Many experiments were conducted in order to assess its monitoring quality and evaluate its performance. Calicot has been evaluated on real clinical data recorded in ICU but, until now, has not been used in clinical routine. This section gives some results concerning the performance of the prototype on QRS detection, with and without piloting. The implemented context analyser is based on a wavelet decomposition-recomposition in three subbands to obtain the triplet ls, ms, hs (low, medium, high subbands). This triplet together with the annotated context attributes r, n, SN R (rhythm, noise type, Signal-to-Noise Ratio) forms the context descriptor used by the pilot to decide which algorithm to use. Piloting rules have been extracted by decision tree learning from the performance results of 7 QRS detectors from the litterature [START_REF] Portet | Learning decision tree for selecting QRS detectors for cardiac monitoring[END_REF]. Three decision trees were induced: D1 (using attributes r × n × SN R × ls × ms × hs), D2 (using r × ls × ms × hs) and D3 (using the subbands only ls × ms × hs).

Ten ECGs, lasting around 30 minutes each (containing about 18.000 QRSs in total) and including ten various ventricular and supra-ventricular arrhythmic contexts, were extracted from the MIT-BIH Arrhythmia database [START_REF] Moody | ECG database applications guide[END_REF]. Real clinical noise, from 5 dB to -15 dB, was introduced randomly in each ECG with probabilities P (no noise) = P (bw) = P (ma) = P (em) = 1/4 and P (5dB) = 1/2, P (-5dB) = 1/3, P (-15dB) = 1/6 to reproduce difficult clinical ECG situations and to assess the system performance in specific contexts as well as when the context changes. The performance was evaluated from the standard T P (True Positive -correct result), F N (False Negative -missed result) and F P (False Positive -false result): the sensitivity Se = To estimate the upper bound performance reachable by Calicot with the pilot, the best detector performance (i.e. achieved by the detector with maximal FM) for each chunck of ECG was also retained. These results were used to define a gold standard (bestChoice).

Table 1 synthesizes the results of arrhythmia recognition without the pilot and every QRS detector algorithms, bestChoice (used as gold standard) and the different piloting rule sets. According to FM pilot D2, outperforms all the other methods. The best non piloted monitoring performance (FM=88.35%) is obtained when using algorithm kadambe for temporal abstraction, followed by af2 (FM=86.67%), and benitez (FM=85.25%). These three algorithms outperform the others with an FM greater by 1.73%. The best piloted monitoring performance is obtained by the pilot D2 rule set followed by pilot D1 and pilot D3. pilot D1 performs better than non piloted af2 but worst than non piloted kadambe. The upper bound that can be obtained is given by bestChoice as FM=91.71%. This shows that the piloting strategy could be notably improved with more accurate rules (at most by 3.36% of FM). kadambe associates wavelet analysis with heuristics for selfadaptating to the signal, thus, it can be considered as being "piloted". To asses the pilot more fairly, new piloting rules, pilot D1 * , pilot D2 * and pilot D3 * , were learned excluding kadambe. The best performance of non piloted algorithms was obtained for af2 followed by benitez. The piloted rule sets exibited the best performance: pilot D3 * with FM = 87.42% outperformed non piloted af2 with FM= 86.67% improving FM by 0.75% which is considered a good score in the QRS detection field. The number of switches, bestChoice, shows that the best possible performance needs 1486 switches. pilot D2 reached good scores with far less switches (294). Without using kadambe, pilot D3 * has switched 1642 times showing that it uses the available algorithms much more.

Compared to kadambe, the advantage of using a pilot is that it uses explicit declarative rules which can be easily updated. This demonstrates the value of using a smart adaptation of QRS detection algorithms according to both signal, patient and diagnosis context.

CONCLUSION

We have presented an approach to intelligent monitoring with selfadaptive capabilities in the cardiac domain. Our proposition associates temporal abstraction, online diagnosis by chronicle recognition, self-adaptation to the monitoring context and automatic knowledge acquisition to learn chronicles and adaptation decision rules. A prototype named Calicot has been implemented.

Efficiency has been a constant concern during the conception implementation of Calicot, as it was intended to run online. Thus, a temporal abstraction method taking advantage of the domain and data specificities has been proposed. Though they representing complex event, chronicles can be efficiently recognized on multiple data streams, one or two orders of magnitude less than real time in our case. To enhance the performance we have also proposed an architecture for self-adaptation, featuring a pilot which can reconfigure the processing chain or tune the module parameters when the monitoring context changes. Finally, symbolic machine learning is used, offline, to get discriminating patterns, on the one hand, and adaptation decision rules, on the other hand. Using a symbolic approach for knowledge and (temporal) reasoning makes it possible to provide understandable explanations to the user. This is very important in medicine for letting clinician operators trust such systems. This research could not have been achieved without an active and fruitful collaboration with the medical staff. Working with clinicians in hospital is not always easy for computer scientists: experts are overbooked, getting data is sometimes difficult as protocols for recording data are very strict, especially they should not introduce any risk for the patient or any violation of data privacy. But confronting ideas and views from different research, knowledge and practice domains is particularly rewarding.

Figure 1 :

 1 Figure 1: The architecture of the online part of the adaptive monitoring system Calicot.

Figure 2 :

 2 Figure 2: ECG (top) and pressure (bottom) signals of a bigeminy episode. The graph in the middle shows a bigeminy chronicle model: P stands for a P wave event occurrence, QRS for a QRS complex, D for a diastole, S for a systole. Quoted QRSs represent abnormal ones. Dotted lines indicate possible event matches that satisfy the temporal constraints.

Figure 3 :

 3 Figure 3: The graphical interface of Calicot showing the recognition of bigeminy and trigeminy episodes.

7

  http://www.irisa.fr/dream/Calicot/

  N , the positive predictivity P P = T P T P +F P and the F-measure F M (β) = (1+β 2 ) * P P * Se β 2 * P P +Se , where β = 1 (same weight for Se and P P ), were computed.

Table 1 :

 1 Recognition results (on 15525 cardiac beats)

	detector	sens(%)	P+(%)	FM(1) (%)	switches
	af2	92.59	81.47	86.67	-
	benitez	95.91	76.72	85.25	-
	df2	80.64	86.61	83.52	-
	gritzali	87.29	75.33	80.87	-
	kadambe *	94.76	82.74	88.35	-
	mobd	95.29	68.36	79.61	-
	pan	79.66	85.70	82.57	-
	bestChoice	92.39	91.04	91.71	1486
	pilot D1	95.09	82.01	88.06	741
	pilot D2	94.74	82.92	88.43	294
	pilot D3	93.30	81.53	87.02	1478
	pilot D1 *	91.32	80.74	85.70	443
	pilot D2 *	92.33	81.38	86.51	343
	pilot D3 *	94.69	81.20	87.42	1642


Since defending my PhD in October 2015, I have been working on a range of topics and questions pertaining to Synthesis. The dictionary entry for synthesis is 'the combination of components or elements to form a connected whole'. In this general definition synthesis covers quite a lot of today's scientific questions; this document will focus on the formalisation of some of them in the field of computer science. This manuscript describes the attempts we have made in the past years to understand, relate, and approach them.

This document is organised in non-technical independent sections each describing a research theme gathering a selection of the most recent scientific works I have contributed to and published between 2017 and today. The sections are named after one or two research colleagues, who have been in different ways influential to the topic at hand. Some of my recent publications are not discussed in this document, a complete list can be found online: http://games-automata-play.com/ Joël Ouaknine and James Worrell I started working with Joël Ouaknine and James Worrell when joining their group as a Research Associate (postdoc) in Oxford in November 2015. They had obtained over the past five to ten years major contributions to a field they almost invented, or re-invented: the algorithmic study of linear dynamical systems (see [START_REF] Ouaknine | On linear recurrence sequences and loop termination[END_REF] for a survey they wrote on the topic).

A dynamical system is given by an operator f : X Ñ X and an initial point x P X, describing an orbit x, f pxq, f 2 pxq, . . . . In the special case of linear dynamical systems, the operators are linear, meaning f : R n Ñ R n is defined using a matrix A P R nˆn through f pxq " A ¨x. Surprisingly, many algorithmic questions remain unanswered for linear dynamical systems: the most innocent looking and fundamental Skolem problem has been open for the better part of a century, it asks whether the first coordinate of f n pxq is zero for some n P N. Joël Ouaknine and James Worrell have shown in [START_REF] Ouaknine | Positivity Problems for Low-Order Linear Recurrence Sequences[END_REF] that solving the related Positivity problem would require major advances in algebraic number theory, putting a lid on efforts to attack this problem directly.

The analysis of linear dynamical systems has many applications: one of them is program analysis. There are two lessons to be had from this setting: the first is that global statements of the form 'in this program this variable is never assigned value 0', akin to the Skolem problem, are very hard to obtain, and the second is that a more practical approach for this is to design (inductive) invariants to reason locally about programs.

This inspired us to study a variant of the Skolem problem: the existence of invariants for linear dynamical systems. More formally, given a linear dynamical system and a target point, does there exist an invariant certifying that the orbit never hits the target? Here an invariant is a set I Ď R n such that x P I, y R I, and f pIq Ď I. Clearly, the existence of an invariant implies that y cannot be in the orbit of x under f . Most importantly, I is a certificate of that fact, which can be easily verified. Without further restriction, the converse also holds: the set I " tx, f pxq, f 2 pxq, . . .u is an invariant if and only if y is not in the orbit. This statement does not bring much clarity to the question: the set I is the orbit itself, and as witnessed by the difficulty of the Skolem problem, can be a very complicated set. Hence our formulation of the invariant synthesis question is parameterised by a class of invariants: natural examples include the class of semialgebraic invariants (defined through polynomial inequalities) and the class of semilinear invariants (defined through linear inequalities). We refer to this problem as the Monniaux problem since it was originally formulated in a more general setting by David Monniaux in [START_REF] Monniaux | On the decidability of the existence of polyhedral invariants in transition systems[END_REF] and also raised by him in a series of personal communications with various members of the theoretical computer science community over the past five years or so.

Asking the invariant synthesis question was the beginning of a daunting quest, giving a new perspective on the analysis of linear dynamical systems. Constructing an invariant circumvents the hardness of the Skolem problem and relates this line of work to decades of research from the field of abstract interpretation where heuristics for constructing invariants have been successfully developed and applied.

The first question we investigated was whether given a linear dynamical system and a target we can determine whether there exists a semialgebraic invariant separating the orbit from the target. Our first paper on this question [START_REF] Fijalkow | Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem[END_REF] (and the journal version [START_REF] Fijalkow | Complete Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem[END_REF]) shows a completeness result: there exists a closed semialgebraic invariant if and only if the target does not belong to the topological closure of the orbit. In some sense, semialgebraic invariants are expressive enough to separate an orbit from a point, although the orbit itself may not be semialgebraic. The proof of our result yields an algorithm for constructing the invariant when it exists, a key ingredient for compositional reasoning about programs.

Semialgebraic invariants are very expressive hence may prove hard to use so in many cases it is desirable to construct simpler invariants: the class of semilinear invariants has been widely used for this purpose. As Monniaux writes in [START_REF] Monniaux | On the decidability of the existence of polyhedral invariants in transition systems[END_REF], 'We started this work hoping to vindicate forty years of research on heuristics by showing that the existence of polyhedral inductive separating invariants in a system with transitions in linear arithmetic (integer or rational) is undecidable.'. Indeed all existing practical implementations rely on heuristics for constructing invariants in this setting, and the existence of an algorithm would potentially have far reaching consequences. Unfortunately, there are no such algorithms: our second paper [START_REF] Fijalkow | On the Monniaux Problem in Abstract Interpretation[END_REF] shows the undecidability of synthesising a semilinear invariant for dynamical systems with two linear operators, fulfiling Monniaux's goal of proving that heuristics are a necessary evil for constructing semilinear invariants. We contrast this negative result with a positive one: in the case of a single linear operator the problem is decidable, albeit very intricate.

The paper [START_REF] Fijalkow | On the decidability of reachability in linear time-invariant systems[END_REF] investigated the related scenario where the linear dynamical system is controlled at each step, and the paper [START_REF] Barloy | A Robust Class of Linear Recurrence Sequences[END_REF] introduced a subclass of linear dynamical systems for which the Skolem problem becomes tractable.

Prakash Panangaden

I met Prakash Panangaden at the Simons Institute for the Theory of Computing in Berkeley in Autumn 2016 during the Logical Structures in Computation semester. He accepted to be my mentor for the semester and introduced me to the beautiful notion of probabilistic bisimulation about which he wrote one of the founding papers [START_REF] Blute | Bisimulation for Labelled Markov Processes[END_REF] and the reference textbook [START_REF] Prakash Panangaden | Labelled Markov Processes[END_REF]. Probabilistic bisimulation is a notion of equivalence for probabilistic systems (labelled Markov processes) whose strength is to be defined locally: two states are equivalent if any action from one state can be simulated by the other, leading to a distribution of equivalent states -note the co-inductive definition.

During the introductory lectures Prakash gave on the topic, he discussed one of the foundational result relating probabilistic bisimulation to logic [START_REF] Desharnais | A Logical Characterization of Bisimulation for Labelled Markov Processes[END_REF]: two states are not probabilistically bisimilar if and only if there exists a formula from probabilistic modal logic separating them. This extends the celebrated Hennessey-Milner theorem from transition systems to the probabilistic world and gives a dual perspective on bisimulation: non-bisimilarity can be certified using a simple logical formula.

Being trained in the field of Logic, Automata, and Games, I adopted the classic game involving Spoiler and Duplicator for defining bisimulation: this game formulation nicely formalises the co-inductive definition. Such a point of view did not exist for probabilistic bisimulation; I had to invent it and convince Prakash of its value. Together with the definition of the game we found a counter-example to the logical characterization above in the presence of uncountably many actions. This was the first negative result in that direction; a number of positive cases had been obtained using different assumptions and very different proof techniques (measure theory, coalgebra, domain theory).

Prakash Panangaden, Bartek Klin, and myself therefore embarked on a new venture: understanding the limits of the logical characterization for probabilistic bisimulation. This journey took us from sunny California to the topological and measure-theoretic realm of Polish spaces; we understood that a new result about analytic sets (extending the Unique Structure Theorem) was needed but its proof eluded us. As was to be expected, the city of Warsaw hosts some of the world leading experts on Polish spaces: the topologist Roman Pol helped us to prove the Positive Unique Structure Theorem. The consequence of this new theorem is a conceptually simple proof of the logical characterization theorem [START_REF] Fijalkow | Expressiveness of Probabilistic Modal Logics, Revisited[END_REF] (see the journal version [START_REF] Clerc | Expressiveness of probabilistic modal logics: A gradual approach[END_REF]), extending the existing results and matching the assumptions of the counter-example mentioned above.

The paper [START_REF] Mathias Ruggaard Pedersen | Timed Comparisons of Semi-Markov Processes[END_REF] studied the applications of probabilistic bisimulation for specifying timing properties, and the paper [START_REF] Fijalkow | Trace Refinement in Labelled Markov Decision Processes[END_REF] constructed algorithms for related equivalence relations close to probabilistic bisimulations.

Alexander Clark

I met Alexander Clark about the time I moved from (as already mentioned) sunny California to (rainy) London in January 2017. He is one of the most recognised authority on automata learning, a part of computational linguistics. His insightful talks connecting learning to logic have triggered my interests for this field which is both close -for its models and objectives -and far -for its tools, drawing from statistics, machine learning, and linguistics -from my automata theory background.

Alexander visited me at the Alan Turing Institute in Autumn 2018 and we started working together on learning probabilistic context-free grammars (PCFGs). Attacking such a well studied problem with a long history meant getting familiar with a lot of ideas completely new to me. I learned a lot from this collaboration and this has been very influential for shaping my research since then. The goal of learning PCFGs is motivated (from a computational linguistic point of view) by understanding the process of first language acquisition, in particular the early phases of the acquisition of syntactic structure. The main difficulty is that in this framework we are learning from words and not derivation trees: it would indeed be much easier -albeit unrealistic -to learn if we had access to the syntactic decomposition of the words by the grammar.

It is well known that learning the whole class of PCFGs is impossible, so the objective here is to define subclasses of PCFGs which are both relevant for the goal stated above and can be effectively learned. To this end we took inspiration from a notion discovered three times in three different research communities: anchors in computational linguistics [START_REF] Stratos | Unsupervised part-of-speech tagging with anchor hidden Markov models[END_REF], separation in complexity theory [START_REF] Arora | Computing a Nonnegative Matrix Factorization -Provably[END_REF], and residual in automata theory [START_REF] Denis | Residual Finite State Automata[END_REF]. We showed that combining this anchored property with restrictions on ambiguity of the grammar yields a subclass of PCFGs identifiable from words which can be efficiently learned [START_REF] Clark | Consistent Unsupervised Estimators for Anchored PCFGs[END_REF].

Olivier Serre

I know of Olivier Serre since my very first steps in research as his lecture notes on games were the first documents I read on the first day of my first research internship in 2009. I met him a few years later and have been in close contact with him ever since, in particular as we co-supervise Pierre Ohlmann for his PhD. Olivier Serre and coauthors introduced the notion of qualitative tree automata, a probabilistic semantics for automata over infinite trees [START_REF] Carayol | Randomization in Automata on Infinite Trees[END_REF]. During my PhD we worked together on the topic and constructed an algorithm for deciding the emptiness of alternating qualitative Büchi tree automata [START_REF] Fijalkow | Emptiness Of Alternating Tree Automata Using Games With Imperfect Information[END_REF].

Automata over infinite trees is a very old topic already introduced in the 70s: the main result is due to Rabin [START_REF] Michael | Decidability of Second-Order Theories and Automata on Infinite Trees[END_REF], it states the decidability of the monadic secondorder logic (MSO) over the infinite binary tree. Sometimes referred to as 'the mother of all decidability results', this powerful result indeed implies many other decidability results through encoding into trees.

A major open question is whether there exist even more expressive decidable logics over the infinite binary tree; many attempts have been made in the past decades, leading to more open problems -for instance with the theory of regular cost functions [Col13a; Fij+15] -or to undecidability results -for instance for MSO + U [START_REF] Bojańczyk | The MSO+U Theory of (N, <) Is Undecidable[END_REF]. Probabilistic and measure-theoretic extensions of MSO have been introduced and decidability results obtained for large fragments [START_REF] Mio | Monadic Second Order Logic with Measure and Category Quantifiers[END_REF][START_REF] Bojańczyk | Thin MSO with a Probabilistic Path Quantifier[END_REF], leaving open whether the extension of MSO with a probabilistic path quantifier is decidable. Bastien Maubert saw the connection between this question and alternating qualitative tree automata, which we used [START_REF] Berthon | Alternating Tree Automata with Qualitative Semantics[END_REF] to give a negative answer: MSO with a probabilistic path quantifier is undecidable 1 . Hence the search for a decidable extension of MSO over infinite trees remains active. Mikołaj Bojańczyk and coauthors have recently shown that in some sense there are no such extensions [START_REF] Bojańczyk | Extensions of ω-Regular Languages[END_REF].

The unexpected link to logic led us to sharpen our understanding of alternating qualitative tree automata; the paper [START_REF] Berthon | Alternating Tree Automata with Qualitative Semantics[END_REF] presents a crisp decidability frontier for the emptiness problem between Büchi and CoBüchi, and deep connections with games of imperfect information.

In another take on probabilistic automata, I have worked with Cristian Riveros and James Worrell on probabilistic automata with bounded ambiguity [START_REF] Fijalkow | Probabilistic Automata of Bounded Ambiguity[END_REF], see also the journal version [START_REF] Fijalkow | Probabilistic Automata of Bounded Ambiguity[END_REF]. Through a new correspondence with multi-objective optimisation we have constructed efficient algorithms for analysing them.

Thomas Colcombet

One of the main contributions of Thomas Colcombet (my former PhD co-advisor together with Mikołaj Bojańczyk) is the theory of regular cost functions [Col13b; Col13a]: this is a set of models (the main ones are cost automata and cost logics) and a set of algorithms for deciding boundedness properties on these models. The first example of the use of this toolbox is the star height problem: given a regular language L and a number k, does there exist a regular expression denoting L using at most k nesting of the star operator? An elegant solution to this problem is from L and k to construct a cost-automaton defining a function f : Σ ˚Ñ N Y t8u such that f is bounded if and only if the answer is positive. Intuitively, the cost-automaton is guessing a regular expression for the language and is checking its validity using the cost mechanisms (implemented by counters). Since checking whether a cost-automaton is bounded is decidable, this yields an algorithm computing the star height of a regular language. More generally, there are two types of results for the theory of regular cost functions:

• decidability results for boundedness problems applying to various models of the theory,

• reductions to boundedness problems inside the theory.

There are many examples of results of the second type, let me cite a few: in logic [BCP16], automata theory [START_REF] Barozzini | Cost Automata, Safe Schemes, and Downward Closures[END_REF], program analysis [START_REF] Colcombet | Automata and Program Analysis[END_REF], and database theory [START_REF] Benedikt | The Complexity of Boundedness for Guarded Logics[END_REF]. What comes next is an application of the theory of regular cost functions to the field of stochastic control.

Nathalie Bertrand visited the Simons Institute for a month to participate in the semester Logical Structures in Computation (mentioned above), and gave a talk about a recent result they had obtained on the control problem for population protocols [START_REF] Bertrand | Controlling a Population[END_REF] (see also the journal version [START_REF] Bertrand | Controlling a population[END_REF]). In this model, a population of agents are controlled uniformly, meaning that the controller applies the same action to every agent. The agents are represented by a finite state system, the same for every agent. The key difficulty is that there is an arbitrary large number of agents: the question is whether for every n P N, there exists a controller able to bring all n agents synchronously to a target state. The technical contribution of [START_REF] Bertrand | Controlling a Population[END_REF][START_REF] Bertrand | Controlling a population[END_REF] is to prove that in the adversarial setting where an opponent chooses the evolution of the agents, the (adversarial) control problem is EXPTIME-complete.

Nathalie introduced the stochastic variant of this problem, where each agent evolves independently according to a probabilistic distribution, i.e. the finite state system modelling an agent is a Markov decision process. The question is whether for every n P N, there exists a controller able to bring all n agents synchronously to a target state with probability one. (Almost) nothing was known about this problem that we call the stochastic control problem; before stating our results, let us discuss four motivations and related lines for works: control of biological systems, parameterised verification and control, distributed computing, and probabilistic automata.

The original motivation was for controlling population of yeasts [START_REF] Uhlendorf | In silico control of biomolecular processes[END_REF]. In this application, the concentration of some molecule is monitored through fluorescence level. Controlling the frequency and duration of injections of a sorbitol solution influences the concentration of the target molecule, triggering different chemical reactions which can be modelled by a finite state system. The objective is to control the population to reach a predetermined fluorescence state.

The formulation of the problem is rooted in parameterised verification, introduced in [GS92]: it is the verification of a system composed of an arbitrary number of identical components. The control problem introduced in [Ber+17; Ber+19] is the first step towards parameterised control : the goal is control a system composed of many identical components in order to ensure a given property. To the best of my knowledge, the contributions of [START_REF] Bertrand | Controlling a Population[END_REF][START_REF] Bertrand | Controlling a population[END_REF] are the first results on parameterised control.

The model also resembles two models introduced for the study of distributed computing. The first and most widely studied is population protocols, introduced in [Ang+06]: the agents are modelled by finite state systems and interact by pairs drawn at random. The mode of interaction is the key difference with the model we study here: in a time step, all of our agents perform simultaneously and independently the same action. This brings us closer to broadcast protocols as studied for instance in [START_REF] Esparza | On the Verification of Broadcast Protocols[END_REF], in which one action involves an arbitrary number of agents. As explained in [START_REF] Bertrand | Controlling a Population[END_REF][START_REF] Bertrand | Controlling a population[END_REF], the model can be seen as a subclass of (stochastic) broadcast protocols. The focus of the distributed computing community when studying population or broadcast protocols is to construct the most efficient protocols for a given task, such as (prominently) electing a leader. A growing literature from the verification community focuses on checking the correctness of a given protocol against a given specification; we refer to the recent survey [START_REF] Esparza | Parameterized Verification of Crowds of Anonymous Processes[END_REF] for an overview. The question here is a synthesis question: we are asking about the existence of a strategy, in other words a protocol, whose goal is to synchronise all agents in a target state.

When considering the limit case of infinitely many agents the parameterised control question becomes the value 1 problem for probabilistic automata, which was proved undecidable in [START_REF] Gimbert | Probabilistic Automata on Finite Words: Decidable and Undecidable Problems[END_REF], and even in very restricted cases [START_REF] Fijalkow | Two Recursively Inseparable Problems for Probabilistic Automata[END_REF]. Hence abstracting continuous distributions by a discrete population of arbitrary size can be seen as an approximation technique for probabilistic automata. Using n agents correponds to using numerical approximation up to 2 ´n with random rounding; in this sense the control problem considers arbitrarily fine approximations. The plague of undecidability results on probabilistic automata (see e.g. [START_REF] Fijalkow | Undecidability results for probabilistic automata[END_REF]) is nicely contrasted by our positive result, which is one of the few decidability results on probabilistic automata not making structural assumptions on the underlying graph. I started working on the stochastic control for population protocols back in 2016. The main question was whether it is decidable at all. We identified a first tool for attacking it: downward closures made the problem naturally fit into the theory of well quasi orders (see [START_REF] Schmitz | Algorithmic Complexity of Well-Quasi-Orders[END_REF] for an introduction to recent results in computer science using this theory). However despite years of efforts, we could not crack it. I became obsessed and presented the problem to a number of researchers, which led to the exploration of many beautiful ideas, but none gave us the solution. The second insight came from Thomas Colcombet, who suggested a reduction of that problem to the theory of regular cost functions. The third insight and key to the full proof is the use of the max-flow min-cut theorem on graphs, which reformulates the question in a dual form that can then be expressed using cost-automata. Our main technical result is that the stochastic control problem is decidable [START_REF] Colcombet | Controlling a Random Population[END_REF]. This is not the end of the story; first because our algorithms is highly impractical, its complexity is a priori non-elementary although the best known lower bound is EX-PTIME-hardness [START_REF] Mascle | Controlling a Random Population is EXPTIME-hard[END_REF]. The second and most interesting perspective was suggested by Blaise Genest (coauthor of [START_REF] Bertrand | Controlling a Population[END_REF][START_REF] Bertrand | Controlling a population[END_REF]): in addition to requiring to synchronise the n agents with probability one, can we bound the expected time before this happens as a function of n? It turns out that there are three natural regimes: polylogarithmic, polynomial, and exponential (the general case). Very little is known about these, except for personal conjectures I would be happy to share!

Bastien Maubert

I visited Bastien Maubert in Naples in May 2017, this was the start of a fruitful collaboration continuing today. We explored together applications of the theory of regular cost functions to controller synthesis, and more specifically to logical specifications involving bound requirements.

In order to perform strategic reasoning temporal logics of programs (such as LTL) have been extended with operators expressing the existence of strategies for coalitions of components. Among the most successful proposals are Alternating-time Temporal Logic (ATL) [START_REF] Alur | Alternating-time temporal logic[END_REF] and, more recently, the more expressive Strategy Logic (SL) [START_REF] Chatterjee | Strategy logic[END_REF]. Both logics can express the existence of strategies for coalitions that ensure some temporal properties against all possible behaviours of the remaining components. Moreover, if such strategies exist, one can also obtain witnessing finite-state strategies. As a result, synthesizing reactive systems from temporal specifications [START_REF] Pnueli | On the synthesis of a reactive module[END_REF] can be reduced to model checking such strategic logics. Strategy Logic can express important game-theoretic concepts such as the existence of Nash equilibria, but they are limited to qualitative properties. For instance important properties such as bounding the maximal number of steps between an event and its reaction cannot be expressed; parametric extensions of temporal logics have been introduced to capture such properties.

The eventually operator can be annotated with a bound: F ďb ϕ says that ϕ holds within b steps for a constant b P N. However, one may not know such bounds or care for their exact value when writing the specification, and it may not be practical to compute the bound. Prompt LTL [START_REF] Kupferman | From liveness to promptness[END_REF] considers b as a variable, and the model-checking problem asks if there exists a valuation of the variable b such that the formula holds.

In order to reason about and synthesize strategies that ensure such properties specified in Prompt LTL, we introduced Prompt Strategy Logic, an extension of SL with the F ďb operator, and developed further the theory of regular cost functions to prove the decidability of model-checking for Prompt Strategy Logic [START_REF] Fijalkow | Quantifying Bounds in Strategy Logic[END_REF].

Assume-guarantee originates as a modular approach to program verification that allows decomposition of proof obligations [START_REF] Alur | Reactive modules[END_REF]. Informally, an assume-guarantee specification consists of two specifications φ and ψ. A system S satisfies this specification if whenever it is used in a context that satisfies the assumption φ, the guarantee ψ holds on the system or, said differently, for all environments E satisfying φ, the composed system S||E satisfies ψ.

Assume-guarantee synthesis is the problem of synthesising a system S satisfying an assume-guarantee specification. We refer to [START_REF] Maoz | Assume-guarantee scenarios: Semantics and synthesis[END_REF] for a discussion of practical applications of assume-guarantee synthesis. When considering LTL specifications, assumeguarantee verification and synthesis reduce to classical LTL model checking and synthesis: if φ and ψ are LTL formulas, then the assume-guarantee specification is equivalent to the LTL specification φ ùñ ψ. But this is not true for Prompt LTL: when we ask that in all environments satisfying the assumption the system also satisfies the guarantee, there is an implicit quantification on the bounds with which the assumption and the guarantee are satisfied: a universal one for the assumption and an existential one for the guarantee. Because in Prompt LTL the only quantification on bounds is an existential one at the front of the formula, this alternation is not reflected in the formula φ ùñ ψ and, in fact, cannot be captured by a Prompt LTL formula. Classical techniques to handle Prompt LTL such as the alternating colour technique [START_REF] Kupferman | From liveness to promptness[END_REF] are thus difficult to apply, and the assume-guarantee synthesis problem for Prompt LTL has been open for a decade.

The problem of assume-guarantee synthesis for Prompt LTL as defined above can be called uniform, as the system that one aims at synthesising does not depend on the bounds for which the assumption or the guarantee are satisfied. It was observed in [START_REF] Jacobs | Distributed synthesis for parameterized temporal logics[END_REF] that this variant of the problem does not always admit finite implementations, as a satisfying system may require memory that depends on the bounds. Also, in the formulation of the problem they consider, the assumption talks about both inputs and outputs, which makes it possible to have solution systems that always falsify the assumption. To eliminate such unsatisfactory solutions we consider assumptions that only talk about inputs. Also, to account for the fact that a system's memory may depend on the bound for the assumption, we introduce a non-uniform variant of the problem, which asks whether for every bound b on the assumption, there exists a bound b 1 on the guarantee and a system S b such that whenever the assumption is satisfied with bound b, the guarantee is satisfied with bound b 1 .

Our second paper constructs an algorithm for solving the assume-guarantee synthesis problem for Prompt LTL [START_REF] Fijalkow | Assume-Guarantee Synthesis for Prompt Linear Temporal Logic[END_REF], solving this decades old open problem. Time and again the heavylifting is done within the theory of regular cost functions: the solution makes crucial use of new results about (history)-determinisability of cost-automata and solvability of cost-games.

Guillaume Lagarde

I met Guillaume Lagarde in 2017 on Friday March 3 at 2:30PM in the room 3052 of the IRIF (Paris 7) laboratory when he gave a talk about his recent works proving lower bounds for non-commutative circuits. He and coauthors extended a famous result by Nisan [START_REF] Nisan | Lower Bounds for Non-Commutative Computation (Extended Abstract)[END_REF] proving an exponential lower on non-commutative algebraic branching programs, by constructing from a circuit a matrix and analysing its rank. At this time I was becoming familiar with automata learning, and in particular the fascinating notion of Hankel matrices. I saw a connection between the following two results, which I thought could not be a coincidence:

• Nisan's result can be stated as follows: given a multivariate non-commutative polynomial P , we can construct a matrix N P such that any algebraic branching program computing P has size at least the rank of N P ;

• Fliess's result [START_REF] Fliess | Matrices de Hankel[END_REF] can be stated as follows: given a function f : Σ ˚Ñ R, we can construct a matrix H f called the Hankel matrix of f such that the size of the smallest weighted automaton computing f is exactly the rank of H f .

Fliess' result, which had been restated and rediscovered many times over the years, is a fundamental result about weighted automata, it is the key ingredient for minimising, and later for learning, these models. It took some time to find a perfect one-to-one correspondence between definitions and notions in non-commutative algebraic complexity and automata theory; once this settled we understood that Nisan's result can indeed be obtained as a simple corollary of Fliess' result. More interestingly, this implies that Nisan's approach is not only a lower bound, but also an upper bound: the size of the smallest algebraic branching program computing P is exactly the rank of N P . In other words, algebraic branching programs are characterised by the matrix defined by Nisan.

Going further, we wondered whether Guillaume's results [START_REF] Lagarde | Lower Bounds and PIT for Non-commutative Arithmetic Circuits with Restricted Parse Trees[END_REF] (extending Nisan's) also had a weighted automata counterpart. The answer is positive, and for this we needed to work with weighted automata over finite trees. Indeed Fliess' result can be extended (almost mutatis mutandis) to functions mapping trees to real numbers: this is the work of Bozapalidis and Louscou-Bozapalidou [START_REF] Bozapalidis | The Rank of a Formal Tree Power Series[END_REF]. Similarly as for the special case of algebraic branching programs, the lower bound induced by the rank of the Hankel matrix is actually also an upper bound. We were then in possession of a new tool to analyse non-commutative circuits: this was an invitation to revisit the literature. The resulting paper [START_REF] Fijalkow | Lower Bounds for Arithmetic Circuits via the Hankel Matrix[END_REF] (and the journal version [START_REF] Fijalkow | Lower Bounds for Arithmetic Circuits via the Hankel Matrix[END_REF]) draws on this newly discovered connection to give new and unified proofs of many existing results, but most importantly prove new results by decomposing and analysing the Hankel matrix.

It turns out that the notion of Hankel matrix played another fundamental role in a line of work I contributed to: lower bounds for state complexity. Motivated by a question asked by Rabin in his seminal paper [START_REF] Michael | Probabilistic Automata[END_REF], I investigated the succinctness of probabilistic automata [START_REF] Fijalkow | Online Space Complexity of Probabilistic Automata[END_REF]. This led to the introduction of (what I thought to be) a new method for proving lower bounds on the state complexity of alternating automata [START_REF] Fijalkow | The State Complexity of Alternating Automata[END_REF]; the matrix constructed in this lower bound is exactly the Hankel matrix, and the lower bounds method stated in [START_REF] Fijalkow | The State Complexity of Alternating Automata[END_REF] is a boolean counterpart of Fliess' theorem. The journal version clarifies this connection [START_REF] Fijalkow | Lower bounds for the state complexity of probabilistic languages and the language of prime numbers[END_REF].

Pierre Ohlmann

I met Pierre Ohlmann when he joined Oxford for a summer internship in 2016. As Ben accurately once said: 'Don't get fooled: he looks like a Californian surfer but he's really sharp'. I co-supervised Pierre for his next two internships (in London and in Paris), and then co-supervised him with Olivier Serre for his PhD. We worked together on many topics, but I can proudly say that I most successfully infected him with the virus of parity games, and more generally games of infinite duration.

Games of infinite duration are a widely studied model in several fields of computer science including program verification, model checking, automata theory, logic, finite model theory, and database theory: the interactions between the players can model a range of (non-terminating) systems and are therefore used for analysing, verifying, and synthesising them. There exists a variety of game models: we consider here two player zero sum deterministic (as opposed to stochastic) games with perfect information. Two of the most important open problems in this field concern parity games and mean payoff games: in both cases the complexity of solving them is in NP and in coNP, but not known to be in polynomial time. This complexity status was once shared with primality testing, linear programming, and others famous problems, which all turned out to the solvable in polynomial time. Yet although both problems have attracted a lot of attention over the past three decades, they remain widely open and exciting research directions.

Parity games are a central model in the study of logic and automata over infinite trees and for their tight relationship with model-checking games for the modal µ-calculus. Following decades of exponential and subexponential algorithms, a breakthrough happened in 2017 when Calude, Jain, Khoussainov, Li, and Stephan [START_REF] Calude | Deciding parity games in quasipolynomial time[END_REF] constructed a quasipolynomial time algorithm for solving parity games. A shockwave was felt throughout Europe: Gimbert and Ibsen-Jensen published a shorter correctness proof [START_REF] Gimbert | A short proof of correctness of the quasi-polynomial time algorithm for parity games[END_REF], Jurdziński and Lazić constructed a second quasipolynomial time algorithm [START_REF] Jurdziński | Succinct progress measures for solving parity games[END_REF], Fearnley, Jain, Schewe, Stephan, and Wojtczak reformulated the original algorithm using value iteration [START_REF] Fearnley | An ordered approach to solving parity games in quasi polynomial time and quasi linear space[END_REF], and Bojańczyk and Czerwiński presented the algorithm as the construction of a separating automaton [START_REF] Bojańczyk | An Automata Toolbox[END_REF], all of this within a matter of months. A few months after that Lehtinen constructed a third quasipolynomial time algorithm [START_REF] Lehtinen | A modal-µ perspective on solving parity games in quasipolynomial time[END_REF].

Bojańczyk's and Czerwiński's contribution [START_REF] Bojańczyk | An Automata Toolbox[END_REF] went beyond merely explaining the first algorithm: by introducing the notion of separating automata they defined a new tool for constructing and understanding algorithms; and indeed it was soon understood that all three quasipolynomial time algorithms induced separating automata. Informally, a separating automaton is a safety automaton -meaning it accepts all infinite runs and only rejects on deadlocks -which separates positional winning plays from losing ones: the observation of Bojańczyk and Czerwiński is that such an automaton induces a generic algorithm for solving parity games by reduction to safety games. I visited Jurdziński and Lazić in Warwick and Bojańczyk and Czerwiński in Warsaw around this time, and the question on everyone's lips was: can construct smaller separating automata? Diving into Jurdziński's and Lazić's succinct progress measure algorithm I extracted the notion of universal trees [START_REF] Fijalkow | An Optimal Value Iteration Algorithm for Parity Games[END_REF]: I constructed a family of value iteration algorithms parameterised by the choice of a universal tree, of which the succinct progress measure algorithm is a special case. The main technical result in [START_REF] Fijalkow | An Optimal Value Iteration Algorithm for Parity Games[END_REF] is a quasipolynomial lower bound on the size of universal trees, a purely combinatorial statement. The lower bounds offered in [START_REF] Fijalkow | An Optimal Value Iteration Algorithm for Parity Games[END_REF] match up to a polynomial factor the universal tree (implicitly) constructed in [START_REF] Jurdziński | Succinct progress measures for solving parity games[END_REF].

One month later Czerwiński, Daviaud, Jurdziński, Lazić, and Parys showed that any separating automaton induces a universal tree of the same size. Combined with my lower bounds on universal trees, this implies an unconditional quasipolynomial lower bound on the size of separating automata. Our joint paper [START_REF] Czerwiński | Universal trees grow inside separating automata: Quasi-polynomial lower bounds for parity games[END_REF] conveys a simple message: all existing quasipolynomial time algorithms are based on separating automata, hence cannot break the quasipolynomial barrier of universal trees.

Parys constructed yet another quasipolynomial time algorithm [START_REF] Parys | Parity Games: Zielonka's Algorithm in Quasi-Polynomial Time[END_REF] which is both simple and beautiful, and seemed to escape the limitations of separating automata. The algorithm is inspired by the exponential time algorithm of Zielonka [START_REF] Zielonka | Infinite Games on Finitely Coloured Graphs with Applications to Automata on Infinite Trees[END_REF] specialising an algorithm due to McNaughton [START_REF] Mcnaughton | Infinite Games Played on Finite Graphs[END_REF]. Parys' algorithm was later improved by Lehtinen, Schewe, and Wojtczak [START_REF] Lehtinen | Improving the complexity of Parys' recursive algorithm[END_REF]. Recently Jurdziński, Morvan, Ohlmann, and Thejaswini [Jur+20] constructed a generic 'universal attractor decomposition algorithm' encompassing all three algorithms. and parameterised by the choice of two universal trees (one of each player). Choosing appropriate pairs of universal trees yields the algorithms from [Zie98; Par19; LSW19], hence these algorithms do not escape the fate of universal trees and their quasipolynomial lower bounds.

In summary, all existing quasipolynomial time algorithms for parity games (and some exponential ones) are related to the combinatorial notion of universal trees, hence subjected to the quasipolynomial lower bounds. If there exists a polynomial time algorithm, we should look for it elsewhere! Beyond parity games. There are a number of other objectives of interest, the most prominent one being mean payoff. With minor adjustements the notion of separating automata can be extended to any positionally determined objective, begging the question whether they can be useful beyond parity games. Trying to extend universal trees I defined universal graphs and told Thomas Colcombet and Pierre Ohlmann about this new definition. Thomas came back the next day with a fantastic technical idea: saturation. This implied a direct and simple proof of the equivalence between separating automata and universal graphs, extending the results of [START_REF] Czerwiński | Universal trees grow inside separating automata: Quasi-polynomial lower bounds for parity games[END_REF] from parity to any positionally determined objective. The paper [CF18; CF19] states this equivalence also considering non-deterministic separating automata and the semantically restricted notion of goodfor-small-games automata. The equivalence proof implies a normal form for universal graphs called linear universal graphs, which means that they yield generic value iteration algorithms (and in particular can be implemented with quasilinear space complexity). At this point we had in our hands two equivalent tools: separating automata and universal graphs. Seeing two sides of the same coin is often useful, and in the subsequent developments going from one representation to the other was sometimes essential.

To summarise, what are universal graphs good for? Given a class of objectives, they reduce the question of constructing algorithms solving games to constructing universal graphs. This is considerably simpler as it is not anymore about the interaction of the two players but only about the combinatorial properties of the objectives. We followed this recipe for different classes of objectives:

• For mean payoff objectives [START_REF] Fijalkow | Value Iteration Using Universal Graphs and the Complexity of Mean Payoff Games[END_REF], we proved matching upper and lower bounds on the size of universal graphs: the upper bounds induce algorithms for solving mean payoff games matching the best known deterministic complexity, and the lower bounds imply that these algorithms are optimal within this class of algorithms.

The main message here is that universal graphs do not yield quasipolynomial time algorithms for mean payoff games.

• For disjunctions of mean payoff objectives, and for disjunctions of mean payoff and parity objectives, we investigated how to combine existing universal graphs for each objective into universal graphs for their disjunctions. Rather than constructing universal graphs from scratch, we wanted to define constructions using universal graphs for the atomic objectives as black boxes. In other words, we assumed the existence of universal graphs for parity objectives and for mean payoff objectives, and constructed universal graphs for combinations of these classes. An important benefit of this approach is its simplicity: both constructions and their correctness proofs are rather short and focus on the interactions between the objectives.

The paper [START_REF] Fijalkow | The Theory of Universal Graphs for Games: Past and Future[END_REF] is an introduction to universal graphs, and the (submitted) journal paper [START_REF] Colcombet | The Theory of Universal Graphs for Infinite Duration Games[END_REF] is a comprehensive account of all existing results on the nascent theory of universal graphs.

Adrià Gascón and Brooks Paige

Adrià Gascón, Brooks Paige, and myself, were research fellows at the Alan Turing Institute in London at the same time, around 2017. Adrià's background is in security and machine learning and Brooks' in probabilistic programming; as a way to collaborate we offered a summer internship at the Turing, which is aimed at PhD students. We hired Judith Clymo, who was specialising in the theory of QBF solvers, and Haik Manukian, an astrophysicist with a solid background in machine learning. This mix of five backgrounds made for a very productive summer! The goal was to work on programming by example, a program synthesis framework where the program is constructed from a few examples, and in particular study the recent 'DeepCoder' approach [START_REF] Balog | Deep-Coder: Learning to Write Programs[END_REF] guiding the search of programs using machine learning predictions.

Working on a re-implementation of DeepCoder's approach, we identified an important challenge: machine learning means training data, and in this context it is essentially nonexistent. DeepCoder's results were based on synthetic data, posing the following question: how to create a dataset of millions of programs, and for each programs of relevant and interesting inputs? Our paper [START_REF] Clymo | Data Generation for Neural Programming by Example[END_REF] introduces different approaches to data generation for program synthesis leveraging tools from formal methods (SMT solvers), and shows the influence of this question in the overall solution.

Besides the question of data generation, summer was a very exciting dive into a fascinating topic: machine learning guided program synthesis. Little was known on the theoretical side, yet its practice was booming with dozens of papers published in the machine learning community annually. The following year I was awarded a three-year research grant DeepSynth (CNRS Momentum 2018 -2021) to work on the topic and to hire a post-doc for two years. Guillaume Lagarde joined LaBRI in September 2019 to carry out this ambitious project. Our aim was to lay the theoretical foundations for machine learning guided program synthesis and to relate this question to existing approaches in computer science; see [START_REF] Fijalkow | A tutorial on machine learning Guided program synthesis[END_REF] for our tutorial.

We focused on the search aspect and it took us the whole duration of the project to define a satisfactory framework in which we could formulate existing algorithms, quantify their merits, and construct new ones. The abstract question we ask is the following: we are looking for a program in a set of programs. We do not know what the program is but we do have some predictions in the form of a probabilistic distribution D over the set of programs. The question is: how to organise the search? The most natural answer is to enumerate programs in non-increasing order: x 1 , x 2 , . . . such that Dpx 1 q ě Dpx 2 q ě . . . , meaning x 1 is the most likely program according to D, x 2 the second most likely, and so on. Unfortunately, enumerating programs in this exact order may be computationally expensive if the distribution D is complicated. This reveals a trade-off: should we enumerate many programs, albeit with low likelihood, or should we enumerate a lot of very likely programs? Another approach is sampling: choose a distribution D 1 and sample programs from it. Surprisingly enough, the optimal choice of distribution is not D 1 " D: indeed to account for the possible sample repetitions it is beneficial to skew D into what we call the square root of D. The point of the distribution based search framework we introduced is to formalise the algorithmic challenges we just sketched.

We implemented a general purpose program synthesis tool called DeepSynth [START_REF] Fijalkow | DeepSynth: Scaling Neural Program Synthesis with Distribution-based Search[END_REF]:

https://github.com/nathanael-fijalkow/DeepSynth

It serves as a basis for all our experiments and shows the improvements due to the distribution based search. Thanks to the genericity of the codebase we are exploring applications of DeepSynth to three different problems: reinforcement learning, the Abstraction and Reasoning Corpus (ARC), and synthesis of reactive controllers.

Ritam Raha

I met Ritam Raha when he joined LaBRI as an intern in Summer 2018. He started his PhD in September 2019 under the joint supervision of Guillermo Perez and Floris Geerts from the University of Antwerp (Belgium), and Jérôme Leroux (Bordeaux) and myself. The goal of Ritam's PhD is to construct algorithms for the verification of machine learning models. We have worked together on different aspects of automata learning in a passive scenario (as opposed to the celebrated active automata learning due to Angluin [START_REF] Angluin | Learning Regular Sets from Queries and Counterexamples[END_REF]).

Passive learning of languages has a long history paved with negative results. Learning automata is notoriously difficult from a theoretical perspective, as witnessed by the original NP-hardness result of learning a deterministic finite automaton (DFA) from examples by [START_REF] Gold | Complexity of Automaton Identification from Given Data[END_REF]. This line of hardness culminates with the inapproximability result of [START_REF] Pitt | The Minimum Consistent DFA Problem Cannot be Approximated within any Polynomial[END_REF] stating that there is no polynomial time algorithm for learning a DFA from examples even up to a polynomial approximation of their size.

One approach to cope with such hardness results is to change representation, replacing automata by logical formulas: their syntactic structures make them more amenable to principled search algorithms. There is a range of potential logical formalisms to choose from depending on the application domain. Linear Temporal Logic [START_REF] Pnueli | The temporal logic of programs[END_REF] is a prominent logic for specifying temporal properties over words. It has become a de facto standard in many fields such as model checking, program analysis, and motion planning for robotics.

A key property making LTL a strong candidate as a concept class is that its syntax does not include variables, contributing to the fact that LTL formulas are typically easy to interpret and therefore useful as explanations.

Over the past five to ten years learning temporal logics (of which LTL is the core) has become an active research area, with applications in program specification and anomaly and fault detections. A number of different approaches have been proposed, leveraging SAT solvers, automata, and Bayesian inference, and extended to more expressive logics such as Property Specification Language (PSL) and Computational Tree Logic (CTL).

Nothing was known about the computational complexity of the underlying problem; indeed the works cited above focused on constructing efficient algorithms for practical applications. In [START_REF] Nathanaël | The Complexity of Learning Linear Temporal Formulas from Examples[END_REF] we initiated the study of the complexity of learning LTL formulas from examples both for the exact and the approximation settings, and relating the problem to classical problems algorithmic questions on finite strings.

Together with Ritam and coauthors [START_REF] Raha | Scalable Anytime Algorithms for Learning Formulas in Linear Temporal Logic[END_REF] we have used these theoretical insights to construct a new tool performing LTL learning from examples. Thanks to succinct representations and the use of approximation algorithms, our algorithm scales to formulas of size 100, while all previous approaches could not output formulas of size larger than 10. The main appeal of our algorithm is to be anytime: whereas previous algorithms may reach the timeout and not give any output, our algorithm constructs smaller and smaller formulas along the computation, hence in most cases can output some formula even if it is not minimal.

Antonio Casares

I met Antonio Casares in Spring 2020 for an (online...) internship, which was immediately followed by the start of his PhD under the joint supervision of Thomas Colcombet (Paris), Igor Walukiewicz (Bordeaux), and myself. Antonio's research interests are in automata, logic, and games, and their applications to synthesis of reactive controllers specified in Linear Temporal Logic (LTL).

The original approach of Pnueli and Rosner [START_REF] Pnueli | On the synthesis of a reactive module[END_REF] for LTL synthesis using automata and games devised more than four decades ago is today at the heart of the state of the art synthesis tools [Esp+17; LMS20; MC18]. The bottleneck is the determinisation of Büchi automata: given a non-deterministic Büchi automaton, construct an equivalent parity automaton. This problem has a long history; it was originally solved by McNaughton in the 60s, and the first asymptotically optimal construction is due to Safra in the 80s. Most of the recent theoretical and practical solutions this problem are based on the construction of Piterman [START_REF] Piterman | From Nondeterministic Büchi and Streett Automata to Deterministic Parity Automata[END_REF]. Schewe's [START_REF] Schewe | Tighter Bounds for the Determinisation of Büchi Automata[END_REF] enlightening perspective on this construction is to decompose it into two steps: first construct a deterministic Muller automaton, and then transform it into an equivalent deterministic parity automaton. Piterman and Schewe's determinisation procedure is one of many examples of constructions using as an intermediate step (subclasses of) Muller conditions before transforming them into parity conditions, either working with automata models or games models.

During the first year of Antonio's PhD we focused on this particular step and study transformations from Muller to parity. We worked with general transition systems to seamlessly encompass both automata and games models. There are several existing constructions transforming subclasses of Muller conditions to parity. The first is the Latest Appearance Record (LAR), which applies to all Muller conditions. It was proved to be optimal in the worst case: there exists a family of Muller automata for which the obtained parity automata are minimal. Many refinements of the LAR have been constructed for subclasses of Muller conditions.

The notion of Zielonka tree of a Muller condition was introduced in [Zie98] and shown to capture the exact memory requirements of Muller games [START_REF] Dziembowski | How much memory is needed to win infinite games?[END_REF]. In the long version of [START_REF] Dziembowski | How much memory is needed to win infinite games?[END_REF], it implicitly appears that the Zielonka tree of a Muller condition can be used to construct a parity automaton recognising this Muller condition. Our first observation was to show a strong optimality result: for all Muller conditions, the parity automaton obtained from the Zielonka tree of a Muller condition is minimal both in the number of states and in the number of priorities. This optimality result is much stronger than the worst case optimality result of the LAR transformation; in essence, it shows that the Zielonka tree of a Muller condition precisely captures the properties of the Muller condition, whereas for instance the LAR only depends on the number of colours.

Our second insight was to note that all existing constructions, including the one based on Zielonka trees, only consider the Muller condition but do not take into account the structure of the underlying transition system. In other words, all transformations work at the level of conditions: they transform a Muller condition into a parity condition, and ignore the interplay between the condition and the transition structure.

In our first paper [START_REF] Casares | Optimal Transformations of Games and Automata Using Muller Conditions[END_REF] we constructed a new transformation called the alternating cycle decomposition (ACD) which captures this interplay: the ACD transforms a Muller transition system into a parity transition system, extending Zielonka trees by considering the alternation of accepting and rejecting cycles in the original transition system. We proved a strong optimality result for the ACD transformation, which had a number of important consequences. The first is an improvement of Piterman and Schewe's construction, and the second is a set of crisp characterisations for relabelling transition systems with different classes of acceptance conditions. With these new insights, Antonio [START_REF] Casares | On the Minimisation of Transition-Based Rabin Automata and the Chromatic Memory Requirements of Muller Conditions[END_REF] related an automata minimisation question to memory requirements for Muller games, solving a long standing open question of Kopczyński [START_REF] Kopczyński | Half-positional determinacy of infinite games[END_REF]. On the more practical side, the ACD transformation has been implemented by Antonio and coauthors in the state of the art tool Strix, yielding smaller controllers for many benchmarks.

The same result has been obtained concurrently with very different techniques[START_REF] Bojańczyk | MSO+∇ is undecidable[END_REF].