Temporal logics for the specification of information-flow properties are able to express relations between multiple executions of a system. Two of the most important such logics are HyperLTL and HyperCTL*, which generalise LTL and CTL* by trace quantification. It is known that this expressiveness comes at a price, i.e., satisfiability is undecidable for both logics. We settle the exact complexity of these problems, showing that both are in fact highly undecidable: we prove that HyperLTL satisfiability is \Sigma_1^1-complete and HyperCTL* satisfiability is \Sigma_1^2-complete. To prove \Sigma_1^2 membership for HyperCTL*, we prove that every satisfiable HyperCTL* formula has a model that is equinumerous to the continuum, the first upper bound of this kind. We prove this bound to be tight. This is joint work with Louwe B. Kuijer, Patrick Totzke and Martin Zimmermann.

Regular languages can be actively learned with membership and equivalence queries in polynomial time. The learning algorithm, called the L^* algorithm, constructs iteratively the right congruence relation of a given regular language L, and returns the minimal DFA recognizing L. The L^* algorithm has been adapted to various types of automata: tree automata, weighted automata, nominal automata. However, an extension to infinite-word automata has been elusive. In this talk, I will present an extension of the active learning framework, in which the algorithm can ask syntactic queries about the automaton representing a given infinite-word language.

First, I will discuss why extending L^*, which asks only semantic queries, to infinite-words languages is difficult. Next, I will present an alternative approach; instead of learning some automaton for a hidden language, we assume that there is a hidden automaton and the algorithm is supposed to learn an equivalent automaton. In this approach, the learning algorithm is allowed to ask standard semantic queries (membership and equivalence) and loop-index queries regarding the structure of the hidden automaton. These queries do not reveal the full structure of the automaton and hence do not trivialize the learning task.

In the extended framework, there are polynomial-time learning algorithms for various types of infinite-word automata: deterministic Buechi automata, LimSup-automata, deterministic parity automata and limit-average automata.

Finally, the idea to incorporate syntactic queries can be adapted to the pushdown framework; I will briefly discuss the learning algorithm for deterministic visibly pushdown automata.

To the classical way of playing in finite extensive-form games, we add a bidding mechanism: at each node of the game tree, each non-controlling player bids some amount of utility for one subgame. When the controller chooses one subgame, the utilities that were bid for this subgame are transferred to her.

The notion of subgame perfect equilibrium (SPE) is naturally extended to these bidding games, and they always always exist like in the classical games. They also enjoy new properties: - If the game tree is binary-branching, payoff-sum-maximizing SPE always exist. - If the game involves only two players, all SPE are payoff-sum-maximizing with the same payoff-tuple, which is called the bidding value of the game. - This value is computable, whereas SPE payoff-tuples are not even continuous in classical games.

This is joint work with Valentin Goranko

We wish to identify the queries that can be solved with close to optimal time guarantees over relational databases. Computing all query answers requires at least linear time before the first answer (to read the input and determine the answer's existence), and then we must allow enough time to print all answers (which may be many). Thus, we aspire to achieve linear preprocessing time and constant or logarithmic time per answer. A known dichotomy classifies Conjunctive Queries into those that admit such enumeration and those that do not: the main difficulty of query answering is joining tables, which can be done efficiently if and only if the join query is acyclic. However, the join query usually does not appear in a vacuum; for example, it may be part of a larger query, or it may be applied to a database with dependencies. We show how to use this context for more efficient computation and study how the complexity changes in these settings. Next, we aspire for an even more powerful solution for query answering: a structure that simulates an array containing the query answers. Such a structure can be used for example to enumerate all answers in a statistically meaningful order or to efficiently compute a boxplot of query answers. We call this simulation random access and study for which queries random access can be achieved with near-optimal guarantees. Our results are accompanied by conditional lower bounds showing that our algorithms can be applied to all tractable queries in some cases. Among our results, we show that a union of tractable Conjunctive Queries may be intractable w.r.t. random access, but a union of intractable Conjunctive Queries may be tractable w.r.t. enumeration.

We present a model of games with imperfect information that features explicit communication actions, by which a player can send her entire observation history to another player. Such full-information protocols are common in asynchronous distributed systems, here we consider a synchronous setting and cast it as a game on word-automatic trees. The information structures arising from such games are again automatic trees, but their branching degree can be unbounded, and then the synthesis problem becomes challenging. We present a method for constructing a finite bisimulation quotient for a representative subcase, which solves the problem effectively. The construction is a guess; if time allows, we will speculate on how to find such quotients systematically.

The talk is based on joint work (in progress) with Laurent Doyen; a part of the material is presented in [D. Berwanger, L. Doyen (2019): Observation and distinction in infinite games, https://arxiv.org/abs/1809.05978]

We give an algebraic characterisation of first-order logic with the neighbour relation, on finite words. For this, we consider languages of finite words over alphabets with an involution on them. The natural algebras for such languages are involution semigroups. To characterise the logic, we define a special kind of semidirect product of involution semigroups, called the locally hermitian product. The characterisation theorem for FO with neighbour states that a language is definable in the logic if and only if it is recognised by a locally hermitian product of an aperiodic commutative involution semigroup, and a locally trivial involution semigroup. We then define the notion of involution varieties of languages, namely classes of languages closed under Boolean operations, quotients, involution, and inverse images of involutory morphisms. An Eilenberg-type correspondence is established between involution varieties of languages and pseudovarieties of involution semigroups. This is joint work with Dhruv Nevatia.

We show that the existence of a first-order formula separating two monadic second order formulas over countable ordinal words is decidable. This extends the work of Henckell and Almeida on finite words, and of Place and Zeitoun on $\omega$-words. This is a joint work with Rémi Morvan and Sam van Gool

The topic of this talk is, once again, the transformation of rational expressions into finite automata, a much laboured subject. In our last joint work, Sylvain Lombardy and I take a shifted perspective on the derivation of expressions method (due to Brzozowski and Antimirov) which reveals that there is indeed no derivation involved. This broadens the scope of the method to expressions over non free monoids.

Automata and games over infinite words are widely used in verification and synthesis of reactive systems. Several different kinds of acceptance conditions can be used in these systems, which may differ in their complexity and expressive power. For their simplicity and usefulness, parity conditions are of special relevance. However, in many applications such as LTL-synthesis, the automata that are obtained in the first place use more complex conditions (Muller conditions) and we have to transform them in parity ones.

In this talk, I will present a construction that takes as input a Muller automaton and transforms it into a parity automaton in an optimal way. More precisely, the resulting parity automaton has minimal size and uses a minimal number of priorities among those automata that admit a locally bijective morphism to the original Muller automaton. This transformation and the optimality result can also be applied to games and other types of transition systems.

We show two applications: an improvement on the determinisation of Büchi automata into deterministic parity automata and characterisations of automata that admit parity, Rabin or Streett conditions in top of them.

This is joint work with Thomas Colcombet and Nathanaël Fijalkow, and it will appear at ICALP 2021.

We study tree-to-tree transformations that can be defined in first-order logic or monadic second-order logic. We prove a decomposition theorem, which shows that every transformation can be obtained from prime transformations, such as tree-to-tree homomorphisms or pre-order traversal, by using combinators such as function composition.

We study the dynamic membership problem for regular languages: fix a language L, read a word w, build in time O(|w|) a data structure indicating if w is in L, and maintain this structure efficiently under substitution edits on w. We consider this problem on the unit cost RAM model with logarithmic world length, where the problem always has a solution in O(log |w| / log log |w|). We show that the problem is in O(log log |w|) for languages in an algebraically-defined class QSG, and that it is in O(1) for another class QLZG. We show that languages not in QSG admit a reduction from the prefix problem for a cyclic group, so that they require \Omega(log n/ log log n) operations in the worst case; and that QSG languages not in QLZG admit a reduction from the prefix problem for the monoid U_1, which we conjecture cannot be maintained in O(1). This yields a conditional trichotomy. We also investigate intermediate cases between O(1) and O(log log n). Our results are shown via the dynamic word problem for monoids and semigroups, for which we also give a classification. We thus solve open problems of the paper of Skovbjerg Frandsen, Miltersen, and Skyum on the dynamic word problem, and additionally cover regular languages.

The concept of bounded expansion provides a robust way to capture sparse graph classes with interesting algorithmic properties. Most notably, every problem definable in first-order logic can be solved in linear time on bounded expansion graph classes. First-order interpretations and transductions of sparse graph classes lead to more general, dense graph classes that seem to inherit many of the nice algorithmic properties of their sparse counterparts.

The leading question of this talk is: “How can we generalize the beautiful existing algorithmic results of sparse graphs to dense graphs?” We start with an overview over sparse and dense graph classes and then introduce lacon- and shrub-decompositions. We show that dense graph classes can be exactly characterized by having a sparse lacon- or shrub-decoposition. If one could efficiently compute such a decomposition then one could solve every problem definable in first-order logic in linear time on these classes.

The monadic second order theory of a linear order (A,<) can be understood using the first order structure M(A,<) = (P(A),⊆,<) where P(A) is the powerset of A, ⊆ is the usual set-theoretic inclusion, and < is the ordering of (A,<) given on singleton subsets. By the pseudofinite monadic second order theory of linear order we mean the intersection of the first order theories of the structures M(A,<) across all finite linear orders (A,<).

I will present an explicit axiomatisation of this shared theory, and characterise the non-standard completions (i.e. those admitting infinite models) in terms of residue functions. I will then talk about a connection with profinite monoids using extended Stone duality. In particular I will discuss a special case of a theorem due to Gehrke, Grigorieff, and Pin saying that the free profinite monoid on one generator is the extended Stone dual of the Boolean algebra of regular languages over a singleton alphabet (together with the binary operation of concatenation).

Let n be a positive integer and M a set of rational n×n-matrices such that M generates a finite multiplicative semigroup. We show that any matrix in the semigroup is a product of matrices in M whose length is at most O(n2logn), where g(n) is the maximum order of finite groups over rational n×n-matrices. This result implies algorithms with an elementary running time for deciding finiteness of weighted automata over the rationals and for deciding reachability in affine integer vector addition systems with states with the finite monoid property.

In this talk we are going to prove the decidability of several properties on the dynamics of additive cellular automata over finite abelian groups. In the first part, we prove the results for a restricted class of additive CA, namely the linear CA by using a new ‘ad hoc’ result from algebra. In the second part, we show how to lift the all the properties to the whole class of additive CA over finite abelian groups.

In this talk, I discuss the time-bounded reachability problem for continuous-time Markov decision processes. I show that the problem is decidable subject to Schanuel’s conjecture. The decision procedure relies on the structure of optimal policies and the conditional decidability (under Schanuel’s conjecture) of the theory of reals extended with exponential and trigonometric functions over bounded domains. I further discuss that any unconditional decidability result would imply unconditional decidability of the bounded continuous Skolem problem, or equivalently, the problem of checking if an exponential polynomial has a non-tangential zero in a bounded interval. The latter problems are also decidable subject to Schanuel’s conjecture but finding unconditional decision procedures remain longstanding open problems. Time permitting, I can also discuss some algorithmic approximate computations using Lyapunov theory of dynamical systems. This talk is based on an ICALP 2020 paper joint with Rupak Majumdar and Mahmoud Salamati at MPI-SWS.

I will present FO+, a restriction of first-order logic where letters are required to appear positively, and the alphabet is partially ordered, for instance by inclusion order if letters are sets of atoms. Restricting predicates to appear positively is very natural when considering for instance logics with fixed points, or various extensions of regular languages. Here we will ask a syntax versus semantics question: FO+-definable languages are monotone in the letters, but can every FO-definable monotone language be defined in FO+ ? On general structures, Lyndon's theorem gives such a syntax/semantics equivalence for monotone first-order formulas, but it is known to fail on finite structures. We will see that it also fails on finite words, giving a much simpler proof for the failure of Lyndon's theorem on finite structures. Finally we will investigate whether FO+-definability is decidable for regular languages on ordered alphabets.

The talk is based on joint work with Thomas Colcombet. We initiate a study of the expressive power of tree algebras, and more generally infinitely sorted algebras, based on their asymptotic complexity.

Tree algebras in many of their forms, such as clones, hyperclones, operads, etc, as well as other kind of algebras, are infinitely sorted: the carrier is a multi sorted set indexed by a parameter that can be interpreted as the number of variables or hole types. Finite such algebras - meaning when all sorts are finite - can be classified depending on the asymptotic size of the carrier sets as function of the parameter, that we call the complexity of the algebra. This naturally defines the notions of algebras of bounded, linear, polynomial, exponential or doubly exponential complexity…

Our main result precisely characterizes the tree algebras of bounded complexity based on the languages that they recognize as Boolean closures of simple languages. Along the way, we prove that such algebras that are syntactic are exactly those in which, as soon as there are sufficiently many variables, the elements are invariant under permutation of the variables.

We consider the decidability of state-to-state reachability in linear time-invariant control systems over continuous time. We analyze this problem with respect to the allowable control sets, which are assumed to be the image under a linear map of the unit hypercube (\emph{i.e.} zonotopes). This naturally models bounded (sometimes called saturated) controls. Decidability of the version of the reachability problem in which control sets are affine subspaces of R^n is a fundamental result in control theory. We obtain some decidability results in low dimension or when the spectrum of the matrix is special. We also obtain some decidability conditioned on the decidability of the first-order theory of the reals with the exponential function. Finally we obtain a hardness result for a mid generalization of the problem. In this case, we show that the problem is at least as hard as the Continuous Positivity problem if the control set is a singleton, or the Nontangential Continuous Positivity problem if the control set is $[-1,1]$.

he talk will be based on joint work with Lê Thành Dũng (Tito) Nguyễn.

This work is part of an exploration of the expressiveness of the simply-typed λ-calculus (STLC) and related substructural variants (linear, affine, planar) using Church encodings of datatypes. More specifically, we are interested in the connection with automata theory for string transductions and languages.

I will first introduce the setting and motivate the problems using Hillebrand and Kanellakis' result stating that the classes of STLC-definable and regular languages coincide. I will then focus on a result stating that star-free languages correspond exactly to those obtained in a non-commutative refinement of STLC based on linear logic. I will sketch an alternative proof of this result using a semantic evaluation argument and discuss related work-in-progress concerning characterizations in the non-commutative λ-calculus of first-order regular string transductions using planar reversible 2DFTs and tree-walking automata.

(the results I will present are based on https://hal.archives-ouvertes.fr/hal-02476219 and http://nguyentito.eu/2021-01-links.pdf)

A probabilistic context-free grammar (PCFG) defines a distribution over trees: each (finite) tree has some probability of being generated. We consider the following game: a (secret) tree is generated by a PCFG. The PCFG is known and given as input, and the goal is to find the tree. How many equality queries are needed? We'll discuss algorithms for solving this problem, using either enumeration or sampling, and applications to program synthesis.

Joint (ongoing) work with Pierre Ohlmann and Guillaume Lagarde.

A numeration system associates to each element of a given set a finite word. The best known of these systems is the decimal system, which associates each positive integer with a word of the alphabet $\{0,1,\ldots,9\}$. This idea can easily be generalised to other positive integers as base such as the binary system or the hexadecimal system.

The first part deals with signed numeration systems. In these systems, we add digits to the alphabet such as the digit $-1$ in the binary system. Under certain conditions, on consecutive digits, we obtain unique representations. This is related to the concept of abstract numeration systems. We will study the shift and odometer from the point of view of dynamical systems.

Digital restrictions also play an important role in another numeration system: the Zeckendorf expansion. This is an example of the larger class of numeration systems based on linear recurrent sequences, which we discuss in the second part. A way to analyse a numeration system is to examine functions operating on the digital representation. The most famous of these functions is the sum-of-digits function and we investigate it from an analytic point of view.

In the expansion of a randomly chosen real, we expect each block of digits to occur with the same frequency. This leads to the concept of normal numbers and the related notion of uniformly distributed sequences. In the last part, we adopt a probabilistic point of view and construct normal numbers and uniformly distributed sequences related to numeration systems.

The design of SQL is based on a three-valued logic (3VL), rather than the usual two-valued Boolean logic. This 3VL accommodates the additional truth value “unknown” for handling nulls, representing missing values. This third truth value is viewed as indispensable for SQL expressiveness, but is at the same time being criticized a lot for leading to unintuitive behavior of queries and for being a source of programmer mistakes.

In a joint work with Leonid Libkin, we show that, contrary to the widely held view, SQL could have been designed based on the standard two-valued logic, without any loss of expressiveness and without giving up nulls. We show that conflating unknown, resulting from conditions referring to nulls, with false leads to an equally expressive version of SQL. Queries written under the two-valued semantics can be efficiently translated into the standard SQL and thus executed on any existing RDBMS. Our results cover the core of the SQL 1999 Standard, including SELECT-FROM-WHERE-GROUP BY-HAVING queries extended with subqueries and IN/EXISTS/ANY/ALL conditions, and recursive queries. In addition, we show that no other many-valued logic for treating nulls could have possibly led to a more expressive language.

Successor-invariant first-order logic is the extension of first-order logic where one has access to an additional successor relation on the elements of the structure, as long as the validity of formulas doesn't depend on the choice of a particular successor. It has been shown by Rossman that this formalism allows to express properties that are not FO-definable. However, his separating example involves dense classes of structures, and the expressive power of successor-invariant first-order logic is an open question for sparse classes of structures. We prove that when the degree is bounded, successor-invariant first-order logic is no more expressive than first-order logic.

It is shown that if a pushdown system is bisimulation equivalent to a finite system, there is already such a finite system whose size is elementary in the description size of the pushdown system. As a consequence, it is elementarily decidable if a pushdown system is bisimulation-finite. This is joint work with Pawel Parys.

In this talk we present a categorical approach to learning automata over words, in the sense of the $L^*$-algorithm of Angluin. This yields a new generic $L^*$-like algorithm which can be instantiated for learning deterministic automata, automata weighted over fields, as well as subsequential transducers. The generic nature of our algorithm is obtained by adopting an approach in which automata are simply functors from a particular category representing words to a “computation category”. We establish that the sufficient properties for yielding the existence of minimal automata in combination with some additional hypotheses relative to termination ensure the correctness of our generic algorithm.

This is joint work with Thomas Colcombet and Riccardo Stabile.

Register automata are finite automata equipped with a finite set of registers in which they can store data, i.e. elements from an infinite alphabet, and compare this data for equality. They provide a simple formalism to specify the behaviour of reactive systems operating data. Initially defined with the equality predicate only, they can be extended to allow for comparison of data with regards to a linear order, like (N,<) or (Q,<). We study the synthesis problem for those specifications. To that end, we extend the classical Church synthesis game to infinite alphabets: two players, Adam and Eve, alternately pick some data, and Eve wins whenever their interaction satisfies the specification, which is a language of infinite words over infinite data alphabet. Unfortunately, such games are undecidable already for specifications described by deterministic register automata. Therefore, we study one-sided Church games, where Eve uses a finite alphabet but Adam still manipulates data. We show such games are decidable in exponential time in the number of registers in the specification, both for Q and N, are determined, and strategies describable by finite-state register transducers suffice for Eve to win. To obtain this result we study constraint sequences, which abstract the behaviour of register automata and allow for reduction of Church games to omega-regular games. Finally, we apply these results to the transducer-synthesis problem. I will end the talk with the discussion of bounded synthesis. There, specification automata are universal (aka co-nondeterministic), and we search for a realizing transducer with an a-priori given number of registers (hence the term 'bounded synthesis'). This problem is known to be decidable for register automata comparing data for equality only, and we will look at the challenges arising for the case of (N,<).

(This is the joint work by Léo Exibard, Emmanuel Filiot, Ayrat Khalimov)