GT ALGA Annual Meeting 2018

Abstract: Since it was established by Büchi, Elgot and Trakhtenbrot in the early 60's, the connection between automata theory and formal logic has been intensively developed in many directions. An important application is decision algorithms for logical theories. Since those pioneer works, the compositional method introduced by Sheilah in 1975 gave a more general framework than automata theory for deciding logical theories. However, automata theory has a lot of other usages, for example the characterisation of fragments of logics. Among the wide range of results in this direction, let us cite for example McNaughton, Papert and Schützenberger: a formula of the monadic second-order logic (MSO) is effectively equivalent to a formula of its first-order fragment if and only if its associated finite monoid is group-free. Since then, many notions of automata have been introduced: automata on trees, on linear orderings, etc. In this work, we focus on automata over the class of transfinite N-free posets. They are a generalisation of branching automata over finite N-free posets, or equivalently series-parallel posets, and of automata over scattered and countable linear orderings. We give an effective logical characterisation of the class of languages recognised by such automata. The logic involved is an extension of MSO with Presburger arithmetic, named P-MSO. The effective construction of an automaton from a formula of P-MSO is a mere adaptation of the case of finite words. The converse however is much less usual. Starting from a rational expression (effectively equivalent to automata), we build a graph, that we parse and transform into a formula of P-MSO. In the parsing of the graph, recursivity is avoided by a MSO-expressible identification of particular factors of posets.

Abstract: Recent years have seen an increasing interest in ontology-mediated query answering (OMQA), in which the semantic knowledge provided by an ontology is exploited when querying data. Adding an ontology has several advantages (e.g. simplifying query formulation, integrating data from different sources, providing more complete answers to queries), but it also makes the query answering task more difficult. Query rewriting, which reduces OMQA to the evaluation of database queries, is a key algorithmic technique that allows OMQA to be implemented on top of existing database systems, thereby benefitting from the maturity and performance of such systems.

In this talk, I will give a short introduction to ontology-mediated query answering, focusing on ontologies formulated using description logics. Then I will consider two natural analysis tasks related to query rewriting (concerning the existence and succinctness of rewritings) and present solutions obtained by leveraging connections to different areas of theoretical computer science (namely, circuit complexity, automata, and constraint satisfaction).

Abstract: In this talk I will show a unifying approach for the three recent quasipolynomial time algorithms for parity games. The first outcome is to give simple presentations and proofs of the algorithms. The second and main outcome is to prove lower bounds in this framework.

Abstract: Being able to explicitly and naturally model data-sharing in multi-agent systems (MAS) is essential in a number of applications: from access-controlled information-flow systems to group-based protocols. However, the MAS formalism do not cater for the explicit or natural expression of data-sharing between agents, not syntactically nor semantically. To fill this gap, we put forward a formalism for the explicit expression of private data-sharing in MAS, i.e., agent a and agent b have an explicit syntactic/semantic endowment to “see” some of each others’ variables, without other agents partaking in this. On these “MAS with 1-to-1 private channels”, we study the model checking problem for Alternating-time Temporal Logic (ATL).

Abstract: We define and evaluate a new preprocessing technique for propositional model counting. This technique leverages definability, i.e., the ability to determine that some gates are implied by the input formula F. Such gates can be exploited to simplify F without modifying its number of models. Unlike previous techniques based on gate detection and replacement, gates do not need to be made explicit in our approach. Our preprocessing technique thus consists of two phases: computing a bipartition (I,O) of the variables of F where the variables from O are defined in F in terms of I, then eliminating some variables of O in F. Our experiments show the computational benefits which can be obtained by taking advantage of our preprocessing technique for model counting.

Abstract: Cypher is a query languages for databases that are structured as property graphs. It was originally implemented as part of the proprietary graph database Neo4j and it is now widely used in industry. Cypher was designed to be easily readable and usable by non-experts. As a result, the semantics of Cypher queries is described using natural language and the expected result is often ambiguous. Our work aims at defining a full denotational semantics of Cypher, in order to pave the way for a future open standard.

Abstract: Arithmetic circuit are the algebraic analogue of boolean circuits. As a natural model for computing multivariate polynomials, they have been extensively studied. The most important open question in the field of algebraic complexity theory is that of separating the classes VP and VNP, the analogues of P and NP. More precisely, can one obtain super-polynomial lower bounds for circuits computing a given explicit polynomial ?

Despite decades of efforts, this question yet seems out of reach, the best general lower bound being only slightly super-linear. The most common approach is to prove lower bounds for restricted classes of circuits, such as monotone or constant-depth circuits. Another approach would be removing relations arising from the mathematical structure underlying the computations, making it harder for circuits to compute polynomials and thus conceivably easier to obtain lower bounds. In this line of thought, Nisan (1991) was able to obtain breakthrough results in the context of non-commutative computations, separating circuits and formulas and characterizing the minimal size of Algebraic Branching Programs (ABP).

Likewise, circuits for which the multiplication is assumed to be non-associative, meaning that (xy)x and x(yx) are different monomials, have been considered. General exponential lower bounds can be proved in this setting. We highlight a syntactical equivalence between non-associative circuits and acyclic Multiplicity Tree Automata (MTA), which leads to a general algebraic characterization of the size of the smallest non-associative circuit computing a given non-associative polynomial.

As a direct consequence of this characterization, we unify several recent circuit lower bounds in the non-commutative setting. Going deeper in the comprehension of this new algebraic tool, we are able to considerably extend a known lower bound to a class which is very close to general.

Abstract: In this work, we study the problem of deciding whether a given deterministic transducer outputs a normal word whenever it is fed with a norm al word, equivalently, whether it preserves normality or not. An infinite word x is normal if every block of the same length occurs in x with the same asymptotic frequency. Previous works characterize some families of transducers which preserve normality: Agafonov selectors, removal of all occurrences of a symbol (when alphabets contain at least three symbols), removal of a finite number of symbols.

Abstract: In this talk, Ι will present a problem that has attracted the attention of two different communities: mathematical linguistics and computational group theory. This problem is about the definability of the language MIX which is made of the permutations of words in (abc)*. It has been shown that this language is recognized by a generalization of context-free grammars kown as multiple context free grammars. I will present several recent results related to this problem. An interesting point is that these results all rely on the use of techniques coming from topology.

Abstract: In this talk, we focus on the concept of rational behaviour in multi-player games on finite graphs, taking the point of view of a player that has access to the structure of the game but cannot make assumptions on the preferences of the other players. In the qualitative setting, admissible strategies have been shown to fit the rationality requirements, as they coincide with winning strategies when these exist, and enjoy the fundamental property that every strategy is either admissible or dominated by an admissible strategy. However, as soon as there are three or more payoffs, one finds that this fundamental property does not necessarily hold anymore: one may observe chains of strategies that are ordered by dominance and such that no admissible strategy dominates any of them. Thus, to recover a satisfactory rationality notion (still based on dominance), we depart from the single strategy analysis approach and consider instead chains of strategies as families of behaviours. We establish a sufficient criterion for games to enjoy a similar fundamental property, ie, all chains are below some maximal chain, and, as an illustration, we present a class of games where admissibility fails to capture some intuitively rational behaviours, while our chain-based analysis does. Based on a joint work with N.Basset, I. Jecker, A. Pauly and J.-F. Raskin, presented at CSL'18.