During my thesis, I studied a subclass of Petri nets called observation Petri nets. The complexity results obtained show that this class is particularly suited for checking parameterized properties, where the parameter is the number of tokens present in the net. Observation Petri nets were introduced for their application to population protocols, a distributed computing model. Population protocols are part of a class of models of concurrent systems in which we are interested in parameterized verification, and in which there are identical agents which synchronize through “simple” communication primitives. I studied other models of this class, like reconfigurable broadcast networks and register protocols and in the future I would like to turn my research towards the analysis of these kinds of distributed systems for which the parameterized problems are not immediately undecidable, broadening the range of formal method techniques used.

Primary key constraints in databases state there can be at most one tuple for every primary key in a given relation. However, these days it is common to have situations where this property cannot be maintained. Databases that violate constraints are called « inconsistent databases ». In particular, if a database violates primary key constraint, it will contain more than one tuple for the same primary key. In this setting, the notion of a repair is defined by picking exactly one tuple for each primary key (maximal consistent subset of the database). A Boolean conjunctive query q is certain for an inconsistent database D if q evaluates to true over all repairs of D. In this context, there is a dichotomy conjecture that states that for a fixed boolean conjunctive query q, testing whether q is certain for an input database D is either polynomial time or coNP-complete.

The conjecture is open in general and has been open for more than two decades. In this talk we will introduce two new algorithms that we have devised, one based on fix-point computation and the other based on bipartite matching. We will also see how these algorithms can be used to prove the dichotomy for the cases that were previously open.

These results were obtained in collaboration with Diego Figueira, Luc Segoufin and Cristina Sirangelo and combine the results that were presented at ICDT 2023 and what will be presented at PODS 2024.

In the study of MSO on graphs, especially on graphs of bounded treewidth, an important tool is MSO transductions. I will show that tool is not only useful, but also somehow canonical: MSO transductions are exactly those graph-to-graph transformations which respect the structure of graphs.

A Timed Automaton is said to be robust if properties (such as reachability) can still be verified despite small perturbations. Our goal in this work is to model perturbations on delays and to quantify them in a function called permissiveness. We present how we compute the maximally permissive strategies to reach a location in a timed automaton.

We will discuss how one may solve modal equations by constructing homomorphisms between graphs. To “solve a modal equation” means: given two modal formulas A and B, to find a syntactic substitution of the propositional variables which renders A and B equivalent. Such a substitution, if it exists, is called a “unifier” of the modal equation A = B, and the problem of deciding whether or not a given equation has a unifier is called the “unifiability” problem. We show that one may construct, for any modal equation E, a relational structure G(E) and a bijection between the set of unifier classes of E and the set of homomorphisms from a fixed sequence of structures to G(E).

Instantiating this construction to the neXt-fragment of Linear Temporal Logic (LTL-X), the unifiability problem for LTL-X becomes equivalent to the following purely graph-theoretic problem. Given a finite edge-colored graph G, decide whether or not G is the homomorphic image, also called “folding”, of a de Bruijn graph B_n for some n. (Here, the de Bruijn graph B_n is the graph underlying the minimal DFA that recognizes the languages A* a A^(n-1) for a in the alphabet A.) We show that this problem is decidable, by giving a complete characterization of the graphs that are foldings of de Bruijn graphs. This then allows us to conclude in particular that the unifiability problem for LTL-X is decidable.

We also apply our method to prove PSPACE-completeness of unifiability for a logic called Alt1, and we formulate a problem about hypergraphs which is equivalent to the unifiability problem for normal modal logic K. The decidability of the latter problem remains open.

This is joint work with Johannes Marti and Michelle Sweering; a preliminary version of part of the work was presented at the workshop UNIF'23 and we are currently working on the full version.

Presheaf automata are presheaves over a fixed directed category. Depending on the choice of the underlying category we obtain different “species” of automata: eg. finite state automata, Petri nets, vector addition systems and, last but not least, various variants of higher dimensional automata. For each such choice, one can define notions of run, language recognized by an automaton, regular and rational languages, bisimulation, determinism, etc. Furthermore, functors between directed categories induce translations between different types of presheaf automata.

Discrete linear dynamical systems (LDS) are a fundamental modelling paradigm in several branches of science, and have been the subject of extensive research for many decades. Within Computer Science, LDS are used, for example, to analyse linear loops and Markov chains, and also arise in areas such as automata theory, differential privacy, control theory, and the study of formal power series, among others.

Perhaps surprisingly, many decision problems concerning LDS (such as reachability of a given hyperplane, known as the Skolem Problem) have been open for many decades. In this talk, we explore the landscape of such problems, focussing in particular on model-checking questions.

In the context of infinite duration games over graphs, a central question is: For which objectives can the existential player always play optimally using positional (memoryless) strategies? In this talk, we characterize omega-regular objectives with this property. Using this characterization, we obtain decidability of half-positionality in polynomial time, get finite-to-infinite and 1-to-2-players lifts, and show the closure under union of prefix-independent half-positional objectives, answering a conjecture by Kopczyński. This is joint work with Pierre Ohlmann.

End of july 2023 Jeff Shallit asked me the following question: assuming that a synchronous automaton (two tapes read simultaneously) recognizes an ordering on the free monoid, is it decidable whether or not this ordering has infinite chains? infinite antichains? and questions of the like. I suspect(ed) that this is not the case but I started to work in the special unary case (the alphabet has a unique letter). I proved that these questions are decidable (it's easy), I characterized the orders that are linear and showed that the equivalence of two linear orders is polynomial (more interesting). I posted it on arxiv on september 19. Then I thought that I should enrich my introduction … and found out that these were (very) old results.

The characterization of linear synchronous orderings on the integers is mentioned in a paper of Liu and Minnes (2009), which refers to a paper of Khoussainov and Rubin (2001) where it is implicit and is obtained as a general result on unary relations (not necessarily orderings). In my talk I will also comment on these results and propose some possible (hopefully genuinely novel!) extensions.

Church’s Problem asks for the construction of a procedure which, given a logical specification φ(I, O) between input ω-strings I and output ω-strings O, determines whether there exists an operator F that implements the specification in the sense that φ(I, F(I)) holds for all inputs I. Büchi and Landweber gave a procedure to solve Church’s problem for MSO specifications and operators computable by finite-state automata. We investigate a generalization of the Church synthesis problem to the continuous time of the non-negative reals. It turns out that in the continuous time there are phenomena which are very different from the canonical discrete time domain of the natural numbers.

Most database management systems use the relational model: data is stored in tables and the SQL query language is used to extract information. Another data model, property graphs, has seen increasing practical use over the last fifteen years.

Most query languages for property graphs are based on the theoretical formalism of Regular Path Queries (RPQs). The query is a regular expression that searches for walks in the graph labeled by words that match the expression.

There is no real consensus on what the correct answer to an RPQ is, or even what the nature of the answer should be. Different real-world languages use different semantics, and these fundamentally differ from the traditional semantics of RPQs used in theory. The core of this talk is about all these differences and their implications.

A seminal paper published in 2012 by Berstel et al. in the Journal of Algebra initiated the systematic study of intersections of recurrent languages and complete bifix codes. One of the main results of this line of research, obtained in 2015 by Berthé et al., states that if F is a uniformly recurrent dendric language (for example, a Sturmian language), then every complete bifix decoding of F is also uniformly recurrent dendric. A delicate part of the proof is showing that the decoding is indeed uniformly recurrent. We introduce a method, relying on the free profinite monoid, giving a new proof of that part, and in fact a significant generalization based on the notion of F-charged bifix code.

Timed languages contain sequences of discrete events (“letters”) separated by real-valued delays, they can be recognized by timed automata, and represent behaviors of various real-time systems. The notion of bandwidth of a timed language defined in a previous paper characterizes the amount of information per time unit, encoded in words of the language observed with some precision ε.

In this paper, we identify three classes of timed automata according to the asymptotics of the bandwidth of their languages with respect to this precision ε: automata are either meager, with an O(1) bandwidth, normal, with a Θ(log (1/ε)) bandwidth, or obese, with Θ(1/ε) bandwidth. We define two structural criteria and prove that they partition timed automata into these 3 classes of bandwidth, implying that there are no intermediate asymptotic classes.

Both criteria are formulated using morphisms from paths of the timed automaton to some finite monoids extending Puri's orbit graphs, and the proofs are based on Simon's factorization forest theorem.

Joint work with A.Degorre, C.Dima, B. Jacobo Inclán

We will introduce the new graph parameter, twin-width, and present some of its structural and algorithmic properties. One of them is that on graphs of bounded twin-width, one can efficiently solve many different problems, in particular those that correspond to a FO formula.

While the twin-width of several graph classes is well known, we will show that determining whether an n-vertex graph has twin-width at most 4 is NP-complete, and that it requires time 2^Ω(n/log n) under ETH.

This talk is based on joint work with Pierre Bergé and Édouard Bonnet.

Given two finite automata A1, A2, recognising languages L1, L2, respectively, the state complexity of union (or intersection, or complement, etc.) is how many states (in terms of the number of states in A1, A2) may be needed in the worst case for an automaton that recognises L1 union L2 (or L1 intersect L2, or the complement of L1, etc.). The state complexity of complementing unambiguous finite automata has long been open, and as late as 2015 Colcombet asked whether unambiguous automata can be complemented with a polynomial blowup. I will report on progress on this question in recent years, both in terms of lower and upper bounds. For the currently best lower bound, techniques from communication complexity play an essential role.

Previous work reduces the problem of deciding whether a weighted finite automaton (WFA) over a field is equivalent to a sequential, respectively, unambiguous, WFA to the computation of the linear hull. The linear hull is the topological closure of the reachability set in a certain linear version of the Zariski topology. We discuss an algorithm to compute the linear hull that works essentially entirely in the realm of linear algebra (i.e., without first resorting to the computation of the finer Zariski topology). Further, we show how this leads to double-exponential bounds on the size of the linear hull.

This talk is on joint work with J. Bell.

Joint work with Nadime Francis, Amélie Gheerbrant, Paolo Guagliardo, Leonid Libkin, Victor Marsault, Wim Martens, Filip Murlak, Liat Peterfreund and Domagoj Vrgoč The development of practical query languages for graph databases runs well ahead of the underlying theory. The ISO committee in charge of database query languages is currently developing a new standard called Graph Query Language (GQL), the main component of which is the pattern matching facility. In many aspects, it goes well beyond RPQs, CRPQs, and similar queries on which the research community has focused for years. In this talk, I will present our distillation of the lengthy standard into a simple Graph Pattern Calculus (GPC) that reflects all the key pattern matching features of GQL.

Given a metric over words, define the distance between two transducers with identical domain as the supremum of the distances of their respective outputs over all inputs. This is a useful generalization for comparing transducers that goes beyond the equivalence problem. Two transducers are said to be close (resp. k-close) if their distance is finite (resp. at most k). We will discuss the decidability of the problem that asks whether two given transducers are close (resp. k-close), for common edit distances.

This is a joint work with Amaldev Manuel (IIT Goa) and Saina Sunny (IIT Goa).

Guarded tuple-generating dependencies (GTGDs) are a natural extension of description logics and referential constraints. It has long been known that queries over GTGDs can be answered by a variant of the chase —a quintessential technique for reasoning with dependencies. However, there has been little work on concrete algorithms and even less on implementation. To address this gap, we revisit Datalog rewriting approaches to query answering, where GTGDs are transformed to a Datalog program that entails the same base facts on each base instance. In our work, we show that the rewriting can be seen as containing “shortcut” rules that circumvent certain chase steps, we present several algorithms that compute the rewriting by simulating specific types of chase steps, and we discuss important implementation issues. Finally, we show empirically that our techniques can process complex GTGDs derived from synthetic and real benchmarks and are thus suitable for practical use.

In recent years we have witnessed an unprecedented confluence of methods from discrete and continuous mathematics, especially in subjects having to do with logic and topology. One can cite fields such as continuous model theory, homotopy type theory and, most relevant to this talk, combinatorial limits. The latter have started from the notion of graphons and have been generalised to other contexts, including the very general Stone pairings. In this subject one looks at uncountable limits of a countable sequence of finite objects, with various logical properties that carry through. In the context of first order logic, one can think of Los’s theorem for ultraproducts, but various other transfer theorems have been obtained in other contexts. In this talk we shall review some of these notions and then connect them with the study of abstract logics through new satisfaction relations, and the comparison between such logics using Chu transforms.

Free profinite monoids are compact totally disconnected monoids obtained in a natural way by “completing” free monoids, roughly similar to how Q is obtained from R. Inside free profinite monoids, various combinatorial or algebraic statements about languages admit topological counterparts. A well-known example of this is the topological characterization of regular languages: a language is regular if and only if its topological closure in the free profinite monoid is open. A second, much subtler example is the correspondence with symbolic dynamics discovered by Almeida in the late 2000s. Almeida showed that minimal shift spaces can be represented inside free profinite monoids as regular J-classes.

In the first part of the talk, I will present basic concepts related with free profinite monoids and survey some key results, including the connections with regular languages and with symbolic dynamics. In the second part, I will explain how free profinite monoids can be used in a practical way to study dynamical systems defined by primitive substitutions. More precisely, I will explain how Almeida's representation produces easy-to-compute numerical invariants for these systems.

This talk is about winning strategies in Markov decision processes and stochastic games and is aimed at a general computer science audience. We start by recalling some of the basic notions in game theory, such as values, strategies, and the memory requirements of optimal and ε-optimal strategies. We will describe a set of recent advances on strategy complexity of verification-centered objectives, such as subclasses of parity objectives, in terms of parameters such as the cardinality of the state space, branching factor of the transition function, and whether the game is concurrent or turn-based.

This talk is about the identification of ω-automata from sets of positive and negative ultimately periodic example words. We'll recap the core mechanisms underlying learning algorithms for deterministic finite automata, then illustrate the difficulties one faces in extending these approaches to deterministic ω-automata and finally, we'll discuss a polynomial time algorithm for constructing a deterministic parity automata (DPA) from a given set of positive and negative ultimately periodic example words. This is joint work with Christof Löding. The talk is aimed at a general computer science audience.

Ontology-mediated query answering (OMQA) is a promising approach to data access and integration that has been actively studied in the knowledge representation and database communities for more than a decade. The vast majority of work on OMQA focuses on conjunctive queries, whereas more expressive queries that feature counting or other forms of aggregation remain largely unexplored. We introduce a general form of counting conjunctive query (CCQ), relate it to previous proposals, and study the complexity of answering such queries in the presence of ontologies expressed in the description logic ALCHI or its sublogics. As the general case of CCQ answering is intractable and often of high complexity over such ontologies, we consider two practically relevant restrictions, namely rooted CCQs and Boolean atomic CCQs, for which we establish improved complexity bounds.

Nous revisitons le problème de la réduction des machines de Mealy incomplètement spécifiées avec la synthèse réactive en tête. Nous proposons deux techniques : la première est inspirée de l’outil MeMin et résout le problème de minimisation, la seconde est une nouvelle approche dérivée des réductions basées sur la simulation mais ne garantit pas forcément une machine minimale. Nous soutenons cependant qu’elle offre un assez bon compromis entre la taille de la machine résultante et les performances. Les méthodes proposées sont comparées à MeMin sur une large collection de cas de test composés d’instances bien connues ainsi que de nouvelles instances.

In his article “Teaching Concurrency” (L. Lamport. Teaching concurrency. ACM SIGACT News Distrib. Com- put. Column 40(1), 58-62 (2009)) Lesely Lamport presents a very short program (see below) and challenges the reader to find an invariance with which the program's correctness can be proved. Here I reproduce the program.

`` 1. x[i] := 1; 2. y[i] := x[(i − 1) mod N] ``

Here N is the number of processes, and p0, . . . , pN−1 are the processes. Process pi writes on register x[i] and all other processes can read it. The registers are serial. The invariant should be good enough to prove the following statement:

After every process has stopped executing its simple protocol, 
   at least one process pi has set y[i] = 1. 

Try to find an invariant and prove this statement. This algorithm will serve to discuss the notion of invariants and to describe a method that can help in developing invariants for more sophisticated algorithms. We will also discuss the question ``what is a state'' (which is relevant to the notion of invariance of course).

Two finite words u and v are called abelian equivalent if each letter of the alphabet occurs the same number of times in both u and v. The abelian subshift A_x of an infinite word x is the set of words y such that, for each factor u of y, there exists a factor v of x such that u and v are abelian equivalent. The notion of an abelian subshift gives a new characterization of Sturmian words: among binary uniformly recurrent words, Sturmian words are exactly those words for which A_x equals the subshift \Omega_x generated by x. In this talk, we are going to discuss general properties of abelian subshifts of binary words, as well as possible extensions of the property A_x =\Omega_x to the non-binary alphabets.

Parikh automata extend finite automata by counters that can be tested for membership in a semilinear set, but only at the end of a run, thereby preserving many of the desirable algorithmic properties of finite automata. In this talk, I will present the extension of the classical Parikh automaton framework onto infinite inputs: We will analyse reachability, safety, Büchi, and co-Büchi Parikh automata on infinite words, and study their expressiveness, their closure properties, and the complexity of the related verification problems.

The growing amount of data collected by sensors or generated by human interaction has led to an increasing use of graph databases, an efficient model for representing intricate data. Techniques to keep track of the history of computations applied to the data inside classical relational database systems are also topical because of their application to enforce Data Protection Regulations (e.g., GDPR). Our research work mixes the two by considering a semiring-based provenance model for navigational queries over graph databases. In the first part, we will focus on the model itself by introducing a toolkit of provenance-aware algorithms, each targeting specific properties of the semiring of use. We notably introduce a new method based on lattice theory permitting an efficient provenance computation for complex graph queries. We propose an open-source implementation of the above-mentioned algorithms, and we conduct an experimental study over real transportation networks of large size, witnessing the practical efficiency of our approach in practical scenarios. From the richness of the literature, we notably obtain a lower bound for the complexity of the full provenance computation in our setting. We finally consider how this framework is positioned compared to other provenance models such as the semiring-based Datalog provenance model. We make explicit how the methods we applied for graph databases can be extended to Datalog queries, and we show how they can be seen as an extension of the semi-naïve evaluation strategy. To leverage this fact, we extend the capabilities of Soufflé, a state-of-the-art Datalog solver, to design an efficient provenance-aware Datalog evaluator. Experimental results based on our open-source implementation entail the fact this approach stays competitive with dedicated graph solutions, despite being more general. In a final round, we discuss some research ideas for improving the model, and state open questions raised by this work.

This is joint work with Silviu Maniu and Pierre Senellart.

I will give a gentle introduction to higher-dimensional automata (HDAs) and their language theory. HDAs have been introduced some 30 years ago as a model for non-interleaving concurrency which generalizes, for example, Petri nets while retaining some automata-theoretic intuition. They have been studied mostly for their operational and geometric aspects and are one of the original motivations for directed algebraic topology. In a series of papers we have recently started to work on the language theory of HDAs: we have introduced languages of HDAs as weak sets of interval pomsets with interfaces and shown that HDAs satisfy Kleene and Myhill-Nerode type theorems. The picture which emerges is that, even though things can sometimes get hairy in proofs, HDAs have a rather pleasant language theory, a fact which should be useful in the theory of non-interleaving concurrency and its applications. Joint work with Christian Johansen, Georg Struth, and Krzysztof Ziemiański

A context-free language is inherently ambiguous if any grammar recognizing it is ambiguous, i.e. there is a word that is generated in two different ways. Deciding the inherent ambiguity of a context-free language is a difficult problem, undecidable in general. The first examples of inherently ambiguous languages were discovered in the 1960s, using iteration techniques on derivation trees. They belonged to a particular subfamily of context-free languages, called bounded context-free languages.

    Although they made it possible to prove the inherent ambiguity of several languages, as for example the language L = a^n b^m c^p with n=m or m=p, iteration techniques are still very laborious to implement, are very specific to the studied language, and seem even sometimes unadapted. For instance, the relative simplicity of the proof of inherent ambiguity of L completely collapses by replacing the constraint "n=m or m=p" by "n≠m or m≠p". 
    In this talk, I will present two useful criteria based on generating series to prove easily the inherent ambiguity of some bounded context-free languages. These languages, which have a rational generating series, resisted both the classical iteration techniques developed in the 1960’s and the analytic methods introduced by Philippe Flajolet in 1987.

Schensted a montré comment on insère un nouvel élément dans un tableau de Young. Cet algorithme consiste à insérer cet élément dans la ligne (=suite non décroissante d’entiers) du bas du tableau puis à itérer vers le haut du tableau si un élément est chassé de la ligne au cours de l'exécution. On s’intéresse ici à l’action du monoide libre sur une seule ligne sans poursuivre sur les lignes supérieures (si un élément est chassé il est perdu). Pour rappel dans un séminaire de Mai 2022 Christophe Reutenauer s’était intéressé à l’action sur les colonnes. Dans ce dernier cas le monoide de transition, qu'il appelle stylique, est fini (il y a un nombre fini de colonnes pour une alphabet donné) alors que l’action sur les lignes définit un monoide infini, le monoide grammique.

La relation qui met ensemble deux mots qui ont la même action sur l’ensemble des lignes est une congruence plus grossière que le congruence plaxique (celle des tableaux de Young) et elle est décidable. Je considère le cas d’un alphabet à 3 lettres pour lequel elle est obtenue en ajoutant aux règles de Knuth une seule nouvelle règle très simple. Je m’aventurerai à proposer un conjecture sur les alphabets à plus de 3 lettres et en passant je parlerai des (très jolis et peut-être utiles) travaux de Okninski et al. sur les algèbres de monoids plaxiques.

—

Schensted showed how to insert a new element in a Young tableau. It consists of inserting this element in the bottom row (row= nondecreasing sequence of elements) and iterating the process further up in case an element of the bottom row is bumped. I am interested in the action of the free monoid which assigns to a row, the row obtainded by Schensted insertion, but ignoring the possible bumped element. Christophe Reutenauer considered in his May seminar the action on the set of columns. His (stylic) monoid is finite (there exist finitely many columns for a fixed alphabet) while mine, the grammic monoid, is infinite.

The relation between two words having the same action on the set of rows is a congruence which is coarser than the plactic congruence (that defining the Young tableaux) and decidable. I consider the case of a 3 letter alphabet for which the congreunce is generated by the Knuth rules plus a unique simple rule. I will risk a conjecture for alphabets of more than 3 letters and say a few words on the (very nice and possibly related) works of Okninski and al. on the algebras of the plactic monoids.