Liste des événements uniques du groupe Séminaire Méthodes Formelles


2022-04-05TBA
07:00-07:00
Online
TBA
 Plus d'infos  


2022-03-01 Logics with concrete domains: an introduction
14:00-15:00
Online
In this talk, we present logical formalisms in which reasoning about concrete domains is embedded in formulae at the atomic level. These mainly include temporal logics with concrete domains and description logics with concrete domains.
For the simple concrete domain (N,<), we present known proof techniques to handle satisfiable (infinite) symbolic models, sometimes at the cost of going beyond $omega$-regularity.
The talk is freely inspired from the paper "Concrete domains in logics: a survey" (2021) written with Karin Quaas (Leipzig University).
 Plus d'infos  


2022-02-15Learning Automata and Transducers: A Categorical Approach
14:00-15:00
Salle 178 (Hybride)
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 (that were disclosed in a previous paper), in combination with some additional hypotheses relative to termination, ensure the correctness of our generic algorithm.
 Plus d'infos  


2022-01-18Orbit-finite-dimensional vector spaces, with applications to weighted register automata
14:00-15:00
Online
I will discuss vector spaces spanned by orbit-finite sets. These spaces are infinite-dimensional, but their sets of dimensions are so highly symmetric that the spaces have many properties enjoyed by finitely-dimensional spaces.

Applications of this include a decision procedure for equivalence of weighted register automata, which are the common generalization of weighted automata and register automata for infinite alphabets. The algorithm runs in exponential time, and in polynomial time for a fixed number of registers. As a special case, we can decide, with the same complexity, language equivalence for unambiguous register automata.

(Joint work with Mikolaj Bojanczyk and Joshua Moerman.)
 Plus d'infos  


2021-12-14Active learning automata with syntactic queries
14:00-15:00
Online
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 Büchi 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.
 Plus d'infos  


2021-12-07Extending Reactive Synthesis to Infinite Data Domains through Machines with Registers
14:00-15:00
Salle 178 (Hybride)
In reactive synthesis, the goal is to automatically generate an implementation from a specification of the reactive and non-terminating input/output behaviours of a system. Specifications are usually modelled as logical formulas or automata over infinite sequences of signals (omega-words), while implementations are represented as transducers. In the classical setting, the set of signals is assumed to be finite.

The aim of this talk is to investigate the case of infinite alphabets. Correspondingly, executions are modelled as data omega-words. In this context, we study specifications and implementations respectively given as automata and transducers extended with a finite set of registers, used to store and compare data values. We consider different instances, depending on whether the specification is nondeterministic, universal (a.k.a. co-nondeterministic) or deterministic: contrary to the finite-alphabet case, those classes are expressively distinct.

When the number of registers of the target implementation is unbounded, the synthesis problem is undecidable, while decidability is recovered in the deterministic case. In the bounded setting, undecidability still holds for non-deterministic specifications, but decidability is recovered for universal ones.

The study was initially conducted over data domains with the equality predicate only, but the techniques can be lifted to the dense order (Q,<) and so-called oligomorphic data domains, over which register automata behave in an omega-regular way. A further exploration of the problem allows to extend the results to the discrete order (N,<), where the behaviours can be regularly approximated. Finally, decidability can be transferred to the case of words with the prefix relation (A^*,<) through a notion of reducibility between domains.
 Plus d'infos  


2021-11-30Efficiently Simulating a Sorted Array with Conjunctive Query Answers
14:00-15:00
Salle 178 (Hybride)
A sorted list of query answers may be much larger than the size of the input database. If its use-case does not entail going over this list one-by-one, but rather it is needed in order to compute the median, a boxplot, or another task that requires jumping arbitrarily to answers by their indices, computing this entire list is unnecessary and inefficient. In this talk, we inspect the question of when a sorted array of query answers can be efficiently simulated. We call this task ranked direct access and focus on near-optimal time guarantees. We ask in which cases ranked direct access can be achieved with only logarithmic factors as overhead on top of the linear time required to determine whether there is an answer, and the constant time required per accessed answer. Thus, we ask which CQs and orders can be answered with quasilinear preprocessing and polylogarithmic access time. We show algorithms for lexicographic and sum-of-weight orders, and prove conditional lower bounds implying that (under some complexity assumptions) our algorithms capture all tractable cases for self-join-free CQs.
 Plus d'infos  


2021-11-16Constructing Deterministic Omega-Automata from Examples by an Extension of the RPNI Algorithm
07:00-07:00
Online
Learning techniques for deterministic finite automata (DFA) have been developed starting from the 1970ies. The two main settings are the construction of DFA from examples (finite sets of words that should be accepted or rejected by the DFA), and from queries to an oracle. These problems are already well understood for DFA, and various learning algorithms for these two settings exist. Deterministic automata on infinite words define languages of infinite words, and are syntactically very similar to DFA. However, certain key properties of DFA that are used in learning algorithms do not hold for automata on infinite words. Therefore, only few results for learning automata over infinite words have been obtained up to now. In this talk, I present an algorithm for the construction of deterministic omega-automata from examples that is obtained by adapting an algorithm called RPNI from the setting of finite words.
 Plus d'infos  


2021-10-19Concurrent NetKAT: Modeling and analyzing stateful, concurrent networks
14:00-15:00
Online
We introduce Concurrent NetKAT (CNetKAT), an extension of the network programming language NetKAT with multiple packets and with operators to specify and reason about concurrency and state in a network. We provide a model of the language based on partially ordered multisets, well-established mathematical structures in the denotational semantics of concurrent languages. We prove that CNetKAT is a sound and complete axiomatization of this model, and we illustrate the use of CNetKAT through various examples. More generally, CNetKAT is an algebraic framework to reason about programs with both local and global state. In our model these are, respectively, the packets and the global variable store, but the scope of applications is much more general, including reasoning about hardware pipelines inside an SDN switch.
This is joint work with Jana Wagemaker, Nate Foster, Tobias Kappe, Dexter Kozen, and Jurriaan Rot.
 Plus d'infos  


2021-10-12Context-bounded verification of liveness properties for multithreaded shared-memory programs
07:00-07:00
Online
We study context-bounded verification of liveness properties of multi-threaded, shared-memory programs, where each thread can spawn additional threads. Our main result shows that context-bounded fair termination is decidable for the model; context-bounded implies that each spawned thread can be context switched a fixed constant number of times. Our proof is technical, since fair termination requires reasoning about the composition of unboundedly many threads each with unboundedly large stacks. In fact, techniques for related problems, which depend crucially on replacing the pushdown threads with finite-state threads, are not applicable. Instead, we introduce an extension of vector addition systems with states (VASS), called VASS with balloons (VASSB), as an intermediate model; it is an infinite-state model of independent interest. A VASSB allows tokens that are themselves markings (balloons). We show that context bounded fair termination reduces to fair termination for VASSB. We show the latter problem is decidable by showing a series of reductions: from fair termination to configuration reachability for VASSB and thence to the reachability problem for VASS. For a lower bound, fair termination is known to be non-elementary already in the special case where threads run to completion (no context switches).

We also show that the simpler problem of context-bounded termination is 2EXPSPACE-complete, matching the complexity bound---and indeed the techniques---for safety verification. Additionally, we show the related problem of fair starvation, which checks if some thread can be starved along a fair run, is also decidable in the context-bounded case. The decidability employs an intricate reduction from fair starvation to fair termination. Like fair termination, this problem is also non-elementary.

https://doi.org/10.1145/3434325
 Plus d'infos  


2021-09-28Positive first-order logic on words
14:00-15:00
178 (hybride)
I will present FO+, a restriction of first-order logic on words, where letter predicates are required to appear positively. The words considered here are on a "powerset alphabet": predicates a(x) and b(x) can be true simultaneously. We will ask a syntax versus semantics question: FO+-definable languages are monotone in the letters (with respect to inclusion), but can every FO-definable monotone language be expressed in FO+ ? On general structures, Lyndon's theorem gives a positive answer to this question, but it is known to fail on finite structures. We will see that it also fails on finite words, by giving a simple counter-example language. This gives a new proof for the failure of Lyndon's theorem on finite structures, that is much more elementary than previous proofs. Finally we will see that surprisingly, FO+-definability is undecidable for regular languages.
 Plus d'infos  


2021-06-29Multi-cost Bounded Tradeoff Analysis in MDP
07:00-07:00
Online
We present a memory-efficient algorithm for multi-objective model checking problems on Markov decision processes (MDPs) with multiple cost structures. The key problem at hand is to check whether there exists a scheduler for a given MDP such that all objectives over cost vectors are fulfilled. We cover multi-objective reachability and expected cost objectives, and combinations thereof. An empirical evaluation using a prototypical implementation on top of the Storm model checker shows the scalability of our approach both in terms of memory consumption and runtime.
(Joint work with Arnd Hartmanns, Sebastian Junges and Tim Quatmann)
 Plus d'infos  


2021-06-01Learning Pomset Automata
07:00-07:00
Online
Abstract: We adapt the L* algorithm to learn bimonoids recognising pomset languages. We then show how to convert between bimonoids and a class of pomset automata that accepts precisely the class of pomset languages recognised by bimonoids.
 Plus d'infos  


2021-05-18Reachability in Vector Addition Systems is Ackermann-complete
07:00-07:00
Online
Complexity of the reachability problem in Vector Addition Systems (VASes) was a long standing problems for a few decades. Very recently two proofs of Ackermann-hardness were obtained independently
(one by Jerome Leroux, one by us). I will present you the proof obtained in a joint work with Lukasz Orlikowski, which is based mostly on one new technique proposed in the paper: possibility of performing many zero-tests in VASes by use of just one additional counter.

Recording: https://u-bordeaux-fr.zoom.us/rec/share/1CiiKX5ILxhdO_QnkVPaSo3l9lAWRlN93okSHDV7rSDkmdqOU73z8mP4SPElg3p-.dEmVj102j1GrMLiV
 Plus d'infos  


2021-05-04Verifying higher-order concurrency with data automata
07:00-07:00
Online
Using a combination of automata-theoretic and game-semantic techniques, we propose a method for analysing higher-order concurrent programs. Our language of choice is Finitary Idealised Concurrent Algol (FICA) due to its relatively simple fully abstract game model.

Our first contribution is an automata model over a tree-structured infinite data alphabet, called split automata, whose distinctive feature is the separation of control and memory. We show that every FICA term can be translated into such an automaton. Thanks to the structure of split automata, we are able to observe subtle aspects of the underlying game semantics.

This enables us to identify a fragment of FICA with iteration and limited synchronisation (but without recursion), for which, in contrast to the whole FICA, a variety of verification problems turn out to be decidable.

This is joint work with Alex Dixon (Warwick), Ranko Lazic (Warwick) and Igor Walukiewicz (Bordeax), to appear at LiCS’21. I will also discuss earlier related work from FoSSaCS’21

Recording: https://u-bordeaux-fr.zoom.us/rec/share/IC3Uv_FTVnghe5s_7rpTzqwzCdKo27G0IgjZyZY8az-ehFCdSYgbBwNY8-fX7eeJ.sf6r4vpSXb1A--Z8
 Plus d'infos  


2021-04-27Cyclotomic Identity Testing and Application
07:00-07:00
Online
We consider the cyclotomic identity testing (CIT) problem: given a polynomial f(x_1,...,x_k),
decide whether f(zeta_n^{e_1},...,zeta_n^{e_k}) is zero, where zeta_n = e^{2pi i/n} is a primitive complex n-th root of unity and e_1,...,e_k are integers, represented in binary.
In case f is given by an algebraic circuit we give a randomized polynomial-time algorithm for CIT. When f is given by a circuit of polynomially bounded degree, we give a randomized NC algorithm.
In case f is a linear form we show that the problem lies in NC. Towards understanding when CIT can be solved in deterministic polynomial-time, we consider so-called diagonal depth-3 circuits, i.e., polynomials
f=sum_{i=1}^m g_i^{d_i}, where g_i is a linear form and d_i a positive integer given in unary.
We observe that a polynomial-time algorithm for CIT on this class would yield a sub-exponential-time algorithm for polynomial identity testing. However, assuming the generalised Riemann hypothesis, we show that if the linear forms g_i are all identical then CIT can be solved in polynomial time. Finally, we use our results to give a new proof that equality of compressed strings, i.e., strings presented using context-free grammars, can be decided in randomized NC.
This work is in collaboration with Nikhil Balaji, Sylvain Perifel and James Worrell.

Recording: https://u-bordeaux-fr.zoom.us/rec/share/-NGKM1iAWimIjdg2pXceRQv83jQMN-StdegWO13IwPJwZ6tURH4fu4IgeFfDD027.HiQiIQxJ5uFUM_N9
 Plus d'infos  


2021-04-13Learning-based LTL synthesis
07:00-07:00
Online
In LTL synthesis, the task is to construct a reactive system producing an output stream ensuring a given formula of linear temporal logic is satisfied for any input stream. Recent results on translating LTL to automata open avenues to learning-based approaches and heuristics for such problems. In particular, the automata-theoretic approach to LTL synthesis can utilize not only topological information through standard graph algorithms, but can now also profit from semantic information through learning algorithms. As a result, in many cases an optimal solution can be obtained without any computation; in more general cases, the approach might yield more explainable controllers and scale better.

Recording: https://u-bordeaux-fr.zoom.us/rec/share/8DKuNeylXNZZTxxwmxzIO5I-Uvf9wYq_sgQG3GmZXp9AqSUZ1KgBN1x9tGkhn3nU.Tlcq0tUXut3h98_2
 Plus d'infos  


2021-03-30Register Automata with Extrema Constraints, and an Application to Two-Variable Logic
07:00-07:00
Online
In this talk I will introduce a model of register automata over infinite trees with extrema constraints. Such an automaton can store elements of a linearly ordered domain in its registers, and can compare those values to the suprema and infima of register values in subtrees. We will see that the emptiness problem for these automata is decidable. As an application, I will outline how the satisfiability problem for two-variable logic with arbitrary predicates, two of them interpreted by linear orders, can be decided.

This talk is based on joint work with Szymon Torunczyk.
 Plus d'infos  


2021-03-23Shuffles, Operads, and Associahedra in Theoretical Computer Science
07:00-07:00
Online
The use of "shuffling together decks of cards" as a metaphor for interleaving execution of processes is well-established in computer science, and has allowed for the transfer of concepts and tools from pure mathematics to areas such as the analysis of Race Conditions. This talk aims to demonstrate that, when we extend this intuition and related models to the infinitary case, we find further connections with many topics in theoretical computing. These range from logical models to cryptographic platforms and questions of complexity and computability.

The starting point for the talk is a (still unresolved) conjecture of Lothar Collatz. We describe this in these terms as a simple game played between three players, and consider how the individual steps may be modelled and composed. Doing this allows us to place the core operator from his conjecture within a suitably general setting : the theory of operads based on invertable operations, and closely related geometric / combinatorial polyhedra such as the associahedra of J. Stasheff.

We give an overview of such structures in a variety of different fields, with particular emphasis on a series of closely related examples from theoretical computer science and logic. We then take a categorical approach and - based on constructions from a well-known series of models of linear logic - give a categorical framework within which the structures we study may be thought of as canonical coherence arrows. This includes the operator from our original motivating example, as a particularly significant example.
 Plus d'infos  


2021-03-16Subcubic Certificates for CFL Reachability
07:00-07:00
Online
The context-free language (CFL) reachability problem on graphs, as well as
a closely related problem of language emptiness for pushdown automata, are
core problems in interprocedural program analysis and model checking,
respectively. Both can be solved in cubic time but, despite years of
efforts, there are no truly sub-cubic algorithms known for either.

We study the related certification task: given a problem instance, are
there small and efficiently checkable certificates for the existence and
for the non-existence of a path (or language non-emptiness and emptiness,
respectively)? We show that, in both scenarios, there exist succinct
certificates (O(n^2) in the size of the problem) and these certificates
can be checked in subcubic (matrix multiplication) time.

A natural question is whether faster algorithms for CFL reachability or
PDA emptiness will lead to faster algorithms for other combinatorial
problems such as SAT. As a consequence of our certification results, we
show that there cannot be a fine-grained reduction from SAT to CFL
reachability or PDA emptiness for a conditional lower bound stronger than
$n^omega$, unless the nondeterministic strong exponential-time hypothesis
(NSETH) fails.

This is joint work with Rupak Majumdar and Philipp Schepper.
A preprint is available at https://arxiv.org/abs/2102.13095 .

Enregistrement : https://u-bordeaux-fr.zoom.us/rec/share/kcrUh-SsH97onePRKAyCrw_B2H7Y2iVQAbGVLdumtgI_0-ZMCnxflRjbBeVv5iCH.Qzri0hDgia6JjQnU
 Plus d'infos  


2021-03-02The Complexity of Answering Unions of Conjunctive Queries
07:00-07:00
Online
We discuss the fine-grained complexity of enumerating the answers to a query over a relational database. With the ideal guarantees, linear time is required before the first answer to read the input and determine its existence, and then we need to print the answers one by one. Consequently, we wish to identify the queries that can be solved with linear preprocessing time and constant or logarithmic delay between answers. A known dichotomy classifies CQs into those that admit such enumeration and those that do not. The computationally expensive component 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 inspect how the complexity changes in these settings and chart the borders of tractability within. In addition, we consider the task of enumerating query answers with a uniformly random order, and we propose to do so using an efficient random-access structure for representing the set of answers. We also prove conditional lower bounds showing that our algorithms capture 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; on the other hand, a union of intractable conjunctive queries may be tractable w.r.t. enumeration.

Enregistrement : https://u-bordeaux-fr.zoom.us/rec/share/QOU7TB0aeSrBV5ZpIKNRc2ATR-9p_C0cLYfpjo1-pGGtK48YGrzCdJj_6S4hVTcJ.loUHSiQ8Wr5tVMgW
 Plus d'infos  


2021-02-02Bisimulation Finiteness of Pushdown Systems Is Elementary
07:00-07:00
Online
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.

Enregistrement ! https://u-bordeaux-fr.zoom.us/rec/share/j6rrjZ1m6oS6b_dpH0xMZD6ip1zb3v53ML5VCtRkAmV6T-kXK1VyjuSkhOv0k7dA.0EtTQChWwRQ_J-6J
 Plus d'infos  


2020-12-15Reachability in dynamical systems with rounding
07:00-07:00
Online
We consider reachability in dynamical systems with discrete linear updates, but with fixed decimal precision, i.e., such that values of the system are rounded at each step. Given a matrix M in Q^{d*d}, an initial vector x in Q^d, a granularity g in Q_+ and a rounding operation [·] projecting a vector of Q^d onto another vector whose every entry is a multiple of g, we are interested in the behaviour of the orbit O=<[x],[M[x]],[M[M[x]]],...>, i.e., the trajectory of a linear dynamical system in which the state is rounded after each step. For arbitrary rounding functions with bounded effect, we show that the complexity of deciding point-to-point reachability—whether a given target y in Q^d belongs to O—is PSPACE-complete when no eigenvalue of M has modulus one. We also establish decidability without any restrictions on eigenvalues for several natural classes of rounding functions.
Joint work with Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, Amaury Pouly, and Markus A. Whiteland
 Plus d'infos  


2020-12-08 On monotonic determinacy and rewritability for recursive queries and views
07:00-07:00
Online
Answering queries using views is a classical and well-studied topic in database theory. Some key associated problems are (monotone) determinacy – can the query Q be expressed as a (monotone) function of the set of views? -- and rewritability – can the query Q be rewritten in certain language over the schema of the views?
In this talk, we will introduce these problems and review some relevant results. We will also discuss some recent results about monotonic determinacy and rewritability for recursive queries and views.

Joint work with Michael Benedikt, Stanislav Kikot and Piotr Ostropolski-Nalewaja.

Enregistrement : https://u-bordeaux-fr.zoom.us/rec/share/kw54X2AGRvmBlKaTxXlauYbrf661UpuEilJEg-oMNZcZtD2S29kXMqGCaEI2agfP.do8D65tAfF7jsSwY
 Plus d'infos  


2020-12-01Optimal transformations of Muller conditions
14:00-15:00
Online
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 a new proof of the fact that a Muller automaton can be labelled with a parity condition iff it can be labelled with both a Rabin and a Sttreet condition (recognizing the same language).

This work was done during my master's internship at the IRIF with Thomas Colcombet and Nathanaël Fijalkow.
 Plus d'infos  


2020-11-24Monotone ABPs complexity vs. monotone rank of some explicit polynomials
14:00-15:00
Online
In this talk, I will introduce a few computational models, known as (algebraic) circuits and formulas, and as branching programs (ABPs). Restricted classes of computation, such as monotone circuits, or non-commutative ABPs, have been investigated through the past decades. In the latter setting, a family of matrices (Nisan matrices) naturally appears, their ranks are related to the optimal size of a circuit computing the target polynomial. Recently, we investigated weak monotonicity (a relaxation of the monotonicity constraint), and found some explicit polynomials for which the weak-non-negative ranks don’t characterize the minimal size of an ABP computing them. The sum of ranks still gives a lower bound on minimal-size computation, and this can be used, for instance, to obtain a quadratic lower bound when computing the elementary symmetric polynomial. Joint work with Hervé Fournier, Guillaume Malod, and Sébastien Tavenas.
 Plus d'infos  


2020-11-17Holonomic Techniques, Periods, and Decision Problems
07:00-07:00
Online

Holonomic techniques have deep roots going back to Wallis, Euler, and Gauss, and have evolved in modern times as an important subfield of computer algebra, thanks in large part to the work of Zeilberger and others over the past three decades. In this talk, I will give an overview of the area, and in particular will present a select survey of known and original results on decision problems for holonomic sequences and functions. I will also discuss some surprising connections to the theory of periods and exponential periods, which are classical objects of study in algebraic geometry and number theory; in particular, I will relate the decidability of certain decision problems for holonomic sequences to deep conjectures about periods and exponential periods, notably those due to Kontsevich and Zagier.

Parts of this talk will be based on the paper "On Positivity and Minimality for Second-Order Holonomic Sequences", https://arxiv.org/abs/2007.12282 .
 Plus d'infos  


2020-11-03DeepSynth, two years later: what have we learned about program synthesis?
07:00-07:00
178
In January 2019 we started the DeepSynth project to understand the use of machine learning for program synthesis. Two years later, I will discuss our current understanding, the ideas we had, and some perspectives.

Joint work with Guillaume Lagarde, and many others.
 Plus d'infos  


2020-10-20Solving Random Parity Games in Polynomial Time
14:00-15:00
Online
We consider the problem of solving random parity games. We prove that parity games exibit a phase transition threshold so that when the degree of the graph that defines the game has a degree large enough then there exists a polynomial time algorithm that solves the game with high probability when the number of nodes goes to infinity. We further propose the SWCP (Self-Winning Cycles Propagation) algorithm and show that, when the degree is large enough, SWCP solves the game with high probability. Furthermore, the complexity of SWCP is polynomial. The design of SWCP is based on the threshold for the appearance of particular types of cycles in the players' respective subgraphs. We further show that non-sparse games can be solved in polynomial time with high probability. This is a joint work with Mickael Touati. More information at https://arxiv.org/abs/2007.08387
 Plus d'infos  


2020-10-06Using TLA+ and Apalache to specify and check the Tendermint light client
14:00-15:00
Virtual
TLA+ is a language for formal specification of all kinds of computer systems. System designers use this language to specify concurrent, distributed, and fault-tolerant protocols, which are traditionally presented in pseudo-code. At Informal Systems, we are using TLA+ to specify and reason about the protocols that are implemented in the Tendermint blockchains and Cosmos ecosystem.

In this talk, I give an introduction into Apalache, a symbolic model checker for TLA+. It assumes that all specification parameters are fixed and all states are finite structures. Apalache translates the underlying transition relation into quantifier-free SMT constraints, which allows us to exploit the power of SMT solvers, while keeping the verification problems decidable. Recently, we have designed the Tendermint light client protocol. The light client checks, whether a block originates from the blockchain, without retrieving and verifying all the blocks of the blockchain. I will present our solutions to modeling this protocol in TLA+ and model checking it with Apalache.

Bio: Igor Konnov is a principal scientist at Informal Systems (Austria), a spin-off of Interchain Foundation (Switzerland). Igor is leading research and development of Apalache -- a symbolic model checker for TLA+. Before joining Informal Systems and Interchain Foundation, Igor Konnov worked as a researcher at Inria Nancy (France) and as a postdoc at TU Wien (Austria). He received his MSc and Ph.D. in Applied Mathematics and Computer Science from Lomonosov Moscow State University (Russia) in 2003 and 2009. In 2019, Igor received his Habilitation from TU Wien (Austria).
 Plus d'infos  


2020-09-29Title: Counting Problems over Incomplete Databases
07:00-07:00
Online
In this presentation I will talk about various counting problems that naturally arise in the context of query evaluation over incomplete databases. Incomplete databases are relational databases that can contain unknown values in the form of labeled nulls. We will assume that the domains of these unknown values are finite and, for a Boolean query $q$, we will consider the following two problems: given as input an incomplete database $D$, (a) return the number of completions of $D$ that satisfy $q$; or (b) return or the number of valuations of the nulls of $D$ yielding a completion that satisfies $q$.


We will study the computational complexity of these problems when $q$ is a self-join--free conjunctive query, and study the impact on the complexity of the following two restrictions: (1) every null occurs at most once in $D$ (what is called *Codd tables*); and (2) the domain of each null is the same. Roughly speaking, we will see that counting completions is much harder than counting valuations, and that both (1) and (2) can reduce the complexity of our problems.

I will also talk about the approximability of these problems and prove that, while counting valuations can efficiently be approximated, in most cases counting completions cannot.

On our way, we will encounter the counting complexity classes #P, Span-P and Span-L.

The presentation will be based on joint work with Marcelo Arenas and Pablo Barcelo; see https://arxiv.org/abs/1912.11064
 Plus d'infos  


2020-09-15Monte Carlo Tree Search guided by Symbolic Advice for MDPs
14:00-15:00
178
We consider the online computation of a strategy that aims at optimizing the expected average reward in a Markov decision process. The strategy is computed with a receding horizon and using Monte Carlo tree search (MCTS). We augment the MCTS algorithm with the notion of symbolic advice, and show that its classical theoretical guarantees are maintained. Symbolic advice are used to bias the selection and simulation strategies of MCTS. We describe how to use QBF and SAT solvers to implement symbolic advice in an efficient way. We illustrate our new algorithm using the popular game Pac-Man and show that the performances of our algorithm exceed those of plain MCTS as well as the performances of human players.
 Plus d'infos  


2020-09-08 Safe Learning for Near Optimal Scheduling
14:00-07:00
Online
We formalize the problem of maximizing the mean-payoff value with high probability while satisfying a parity objective in a Markov decision process with unknown probabilistic transition function and unknown reward function. Assuming the support of the unknown transition function and a lower bound on the minimal transition probability are known in advance, we show that in single end components two combinations of guarantees on the parity and mean-payoff objectives can be achieved depending on how much memory one is willing to use.

(i) For all epsilon we can construct an online-learning finite-memory strategy that satisfies the parity objective and which achieves an epsilon-optimal mean payoff, both almost surely.

(ii) Alternatively, for all epsilon and gamma there exists an online-learning infinite-memory strategy that satisfies the parity objective surely and which achieves an epsilon-optimal mean payoff with probability at least 1 - gamma.

We apply (i) to obtain safe and near optimal schedulers for a preemptible task scheduling problem. Our learning-based approach is compared against offline model checking and (shielded) model-free learning techniques based on shielded deep Q-learning. All the algorithms have been implemented to conduct experimental evaluations.
 Plus d'infos  


2020-06-30When Is a Bottom-up Deterministic Tree Transducer Top-down Deterministic?
14:00-15:00
Virtual
We consider two natural subclasses of deterministic top-down tree-to-tree transducers, namely, linear and uniform-copying transducers. For both classes we show that it is decidable whether the translation of a transducer with look-ahead can be realized by a transducer from the same class without look-ahead.

The transducers constructed in this way, may still make use of inspection, i.e., have an additional top-down deterministic tree automaton restricting the domain. We provide a second procedure which decides whether inspection can be removed and if so, constructs an equivalent transducer without inspection.

The construction relies on a precise abstract interpretation of inspection requirements and a dedicated earliest-normal form for linear as well as uniform-copying transducers which can be constructed in polynomial time. As a consequence, equivalence of these transducers can be decided in polynomial time.

Applying these results to deterministic bottom-up transducers, we obtain that it is decidable whether or not their translations can be realized by deterministic uniform-copying top-down transducers without look-ahead (but with inspection) - or without both look-ahead and inspection.
 Plus d'infos  


2020-06-23A Congruence-based Perspective on Automata Minimization Algorithms
14:00-15:00
Virtual
Getting the deterministic finite-state automaton with the least possible number of states is an essential question in many applications such as text processing, image analysis and program verification and synthesis.
Most of the minimization methods that have been proposed in the literature rely on building a partition of the set of states of the input automaton to obtain the minimal deterministic automaton. This is the case of Hopcroft's and Moore's algorithm.
Another independent method is the classical textbook procedure proposed by Brzozowski. This algorithm simply combines a determinization (D) and reverse (R) operation twice applied to the input automaton N, i.e., DoRoDoR(N), to obtain the minimal automaton. Despite having an exponential worst-case complexity, its simplicity has recently motivated the study of this method and its connection with the partition-based methods, with the goal of providing more efficient versions of it.
In this talk, I will address this study from a language-theoretical perspective. I will use equivalence relations on words to give a new and simple proof of correctness of the double-reversal method and shed light on the connection between this method and Moore's algorithm, a partition-based method.
 Plus d'infos  


2020-06-02Learning Description Logic Ontologies
14:00-15:00
178
Ontologies have been used to describe knowledge in various domains, in particular, in those related to life sciences. Semi-automating the process of building an ontology has attracted researchers from various communities into a field called "Ontology Learning". The process of building an ontology can be divided into two main tasks: finding the relevant vocabulary and the appropriate ontology language, and discovering how the vocabulary should be related using the logical constructs available in the chosen ontology language. In this presentation, I will provide a brief overview of five approaches from the literature which have been proposed to semi-automate the process of building an ontology formulated in description logic (DL), focusing on the second task. I will then present some results on the complexity of learning lightweight DL ontologies in the exact and probably approximately correct learning models from computational learning theory.

Main references for this talk:

Learning Query Inseparable ELH Ontologies AAAI 2020
Learning Description Logic Ontologies. Five Approaches. Where Do They Stand? KI 2020 (under review, minor revision)
Exact Learning of Lightweight Description Logic Ontologies JMLR 2018
ExactLearner: A Tool for Exact Learning of EL Ontologies KR 2018
A Model for Learning Description Logic Ontologies Based on Exact Learning AAAI 2016
 Plus d'infos  


2020-05-26A parallel syntax for non-wellfounded proof theory
14:00-15:00
Virtual
Proof theory is the study of proofs as mathematical objects in their own right. Infinite proofs (eg. infinite descent proofs) are pervasive in mathematics. A formal way of characterizing such proofs can be done by looking at fixed point logics (eg. mu calculus) from proof-theoretic lenses. Baelde et. al. have proposed an infinitary sequent calculus (i.e. infinitely deep, finitely wide proofs) for linear logic with fixed points (muMALL). In this talk, following a brief history of proof theory and infinite proofs, I will introduce muMALL. However, the sequent calculus of muMALL turns out to be ``too sequential". In order to achieve more liberal cut elimination, we have devised infinets which are proofs nets (à la Curien) for the multiplicative fragment (muMLL). The later part of the talk will focus on infinets and ongoing work on these nets.

Joint work with: Alexis Saurin, Luc Pellisier
 Plus d'infos  


2020-05-19Query evaluation on probabilistic data: a story of dichotomies
14:00-15:00
Virtual
Query evaluation is the problem of checking if some input data
satisfies a fixed query, and probabilistic query evaluation (PQE) is its
extension to probabilistic data, where we must compute the probability
that the query is true. Specifically, we study this problem on
tuple-independent databases of arity 2, aka probabilistic graphs: the
graph has edges labeled with probabilities denoting how likely it is
that the edge exists, independently from other edges. The PQE problem
for a query Q, called PQE(Q) is to then take an input probabilistic
graph of this kind, and compute the exact probability that a random
possible world of this graph satisfies Q. We study this problem in data
complexity, i.e., its complexity is measured as a function of the graph,
when Q is fixed.

The talk will present several dichotomies around the PQE problem. The
first one is by Dalvi and Suciu [JACM'12] and applies to unions of
conjunctive queries. They showed that for any such query Q, either
PQE(Q) is in PTIME or it is #P-hard. I will present our recent extension
of this dichotomy with Ismail Ilkan Ceylan [ICDT'20], for the larger
query class of homomorphism-closed queries: for any such query Q, either
PQE(Q) is in PTIME or it is #P-hard. Actually, the main result is that
PQE(Q) is #P-hard for any homomorphism-closed query which is not a UCQ.
I will also present our dichotomy with Pierre Bourhis and Pierre
Senellart [ICALP'15, PODS'16] on restricting instance classes. We show
that PQE(Q) is in PTIME, for the larger class of MSO queries, when the
input probabilistic graphs are required to be trees or have
bounded-treewidth. Conversely, PQE is intractable on unbounded-treewidth
graphs under some technical assumptions. Last, I will present our
ongoing work with Benny Kimelfeld, showing that the PQE dichotomy on
self-join-free conjunctive queries also applies to unweighted PQE, i.e.,
when all probabilities of the graph are 1/2.
 Plus d'infos  


2020-05-05Order problem for automaton semigroups
14:00-15:00
TBA
The class of automaton (semi)groups--that is (semi)groups generated by functions defined using transducers--has been studied since the late 70's as many very interesting (semi)groups arise from it. From a computer scientist point of view it is also very nice because the underlying automaton structure allows to apply known tools, and for instance one can decide if an element represents the identity element using automaton minimization.
In this talk, we focus on a the order problem, that is given an element g in the (semi)group, does there exist two distinct integers l,m such that g^l=g^m ? This problem was proven undecidable for general automaton (semi)groups by Gilibert, but Bondarenko, Bondarenko, Sidki and Zapata showed that, if one restricts the automaton, then the problem is decidable in the group case. We extend their result to the semigroup case, introducing several extensions of their work.

This is joint work with Laurent Bartholdi, Ines Klimann and Matthieu Picantin
 Plus d'infos  


2020-04-21On polynomial recursive sequences
14:00-15:00
online
We study the expressive power of polynomial recursive sequences, a nonlinear extension of the well-known class of linear recursive sequences. These sequences arise naturally in the study of nonlinear extensions of weighted automata, where (non)expressiveness results translate to class separations. A typical example of a polynomial recursive sequence is b_n=n!. Our main result is that the sequence u_n=n^n is not polynomial recursive.

This is joint work with Michaël Cadilhac, Charles Paperman, Michal Pilipczuk and Géraud Sénizergues available on arxiv https://arxiv.org/abs/2002.08630
 Plus d'infos  


2020-04-14Controlling a random population
14:00-15:00
178
Bertrand et al. (2017) introduced a model of parameterised systems, where each agent is represented by a finite state system, and studied the following control problem: for any number of agents, does there exist a controller able to bring all agents to a target state? They showed that the problem is decidable and EXPTIME-complete in the adversarial setting, and posed as an open problem the stochastic setting, where the agent is represented by a Markov decision process. In this paper, we show that the stochastic control problem is decidable. Our solution makes significant uses of well quasi orders, of the max-flow min- cut theorem, and of the theory of regular cost functions.
 Plus d'infos  


2020-03-31Reachability in fixed dimension vector addition systems with states
07:00-07:00
The reachability problem is a central decision problem for formal verification based on vector addition systems with states (VASS), which are equivalent to Petri nets and form one of the most studied and applied models of concurrency. Reachability for VASS is also inter-reducible with a plethora of problems from a number of areas of computer science. In spite of recent progress, the complexity of the reachability problem remains unsettled, and it is closely related to the lengths of shortest VASS runs that witness reachability. We consider VASS of fixed dimension, and obtain three main results. For the first two, we assume that the integers in the input are given in unary, and that the control graph of the given VASS is flat (i.e., without nested cycles). We obtain a family of VASS in dimension 3 whose shortest reachability witnessing runs are exponential, and we show that the reachability problem is NP-hard in dimension 7. These results resolve negatively questions that had been posed by the works of Blondin et al. in LICS 2015 and Englert et al. in LICS 2016, and contribute a first construction that distinguishes 3-dimensional flat VASS from 2-dimensional VASS. Our third result, by means of a novel family of products of integer fractions, shows that 4-dimensional VASS can have doubly exponentially long shortest reachability witnessing runs. The smallest dimension for which this was previously known is 14. Joint work with Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Filip Mazowiecki. Paper available at https://arxiv.org/abs/2001.04327
 Plus d'infos  


2020-03-24A parallel syntax for non-wellfounded proof theory
14:00-15:00
178
Proof theory is the study of proofs as mathematical objects in their own right. Infinite proofs (eg. infinite descent proofs) are pervasive in mathematics. A formal way of characterizing such proofs can be done by looking at fixed point logics (eg. mu calculus) from proof-theoretic lenses. Baelde et. al. have proposed an infinitary sequent calculus (i.e. infinitely deep, finitely wide proofs) for linear logic with fixed points (muMALL). In this talk, following a brief history of proof theory and infinite proofs, I will introduce muMALL. However, the sequent calculus of muMALL turns out to be ``too sequential". In order to achieve more liberal cut elimination, we have devised infinets which are proofs nets (à la Curien) for the multiplicative fragment (muMLL). The later part of the talk will focus on infinets and ongoing work on these nets.

Joint work with: Alexis Saurin, Luc Pellisier
 Plus d'infos  


2020-03-17Finite automata presentable groups
14:00-15:00
178

A mathematical structure M is called finite automata presentable if the elements of M can be represented by strings in a regular language,
in such a way that the relations and functions of M are also decided by finite automata. We will discuss the extent of this notions in. the context of groups.
Older work with Thomas shows that every finitely generated subgroup is abelian by finite. Recent work with Stephan gives new examples and counterexamples in the setting of groups that are nilpotent of class 2. We will also discuss the possibility of a complete description of such groups.
 Plus d'infos  


2020-03-10An introduction to Knowledge compilation
07:00-07:00
178
Knowledge compilation aims to transform knowledge on a system, often
represented in a natural but hard to query way, into a - hopefully small - data
structure that is more practical to reason with. The idea is that after a
potentially expensive offline compilation phase, one can efficiently extract new
knowledge by directly querying the data structure.

Originating in symbolic AI where it was mainly used to find better
representations of CNF-formulas or to efficiently solve configuration problems,
this idea has spread in many adjacent fields such as database theory where it
has been used to efficiently compute aggregates in databases.

In this talk, we will give a broad overview of knowledge compilation and its
applications. We will presente some interesting data structure used in knowledge
compilation and how they are used both theoretically and in practice.
 Plus d'infos  


2020-02-28Two Variable Logic with a Between Relation
14:00-15:00
76
It is well-known that every sentence of first-order logic over <, interpreted in finite words (FO[<]), is equivalent to a sentence in which only three variables are used. The fragment FO2[<] of sentences using only two variables, has been the subject of considerable study, and admits interesting characterizations in algebra and temporal logic.


In this talk, I will describe an extension of FO2[<] in which one allows a new binary relation that says, ‘there is an occurrence of the letter a between x and y’. In a sense, this is the simplest property that one can express that requires 3 variables.


I will present several logics, both first-order and temporal, that have the same expressive power; matching lower and upper bounds for the complexity of satisfiability for each of these formulations; and effective necessary and sufficient conditions, based on the syntactic monoid, for a property to be expressible in these logics. This algebraic analysis allows one to prove, among other things, that these new logics have strictly less expressive power than full first-order logic FO[<]. The proofs use a novel method for obtaining factorizations of words that may have independent interest.


This is joint work with Andreas Krebs, Kamal Lodaya, and Paritosh Pandya. The results are described in two papers presented at LICS 2016 and CSL 2018. A journal version, containing all the results and proofs (arXiv:1902.05905) will appear in Logical Methods in Computer Science.
 Plus d'infos  


2020-02-18An algebraic approach to equivalence of MSO transductions of graphs of bounded treewidth
07:00-07:00
178
We prove MSO-transductions of graphs of bounded treewidth have decidable
equivalence modulo fractional isomorphism with real coefficients (not necessarily nonnegative).
The main goal of this talk is to present a new approach to equivalence problem of MSO-transductions of graphs of bounded treewidth.
This approach relies on associating to a graph a list of polynomials or generating functions
which can be updated by a polynomial function after join and forget operation of sourced graphs.

This is joint work with Mikolaj Bojanczyk.
 Plus d'infos  


2020-02-11The reverse mathematics of Hindman's theorem
07:00-07:00
178
Reverse mathematics consists of the study of the minimal axioms needed to prove a theorem. A phenomenon that appeared at the beginning of this study is that among the "natural" theorems, an enormous majority are equivalent to one out of five axiomatic systems: the Big Five. The exceptions to this are mainly mainly theorems from combinatorics, the most famous being the Ramsey theorem for pairs. This makes combinatorics especially interesting in the context of reverse mathematics.

Some theorems still escape classification, such as Hindman's theorem, which says that for any finite coloring, there is an infinite set whose set of finite sums of distinct elements is monochromatic. This theorem has several proofs, but the most elementary is in the system ACA_0^+ (the existence of the omega-jump), while it is only known to imply arithmetical comprehension.

We will start by presenting reverse mathematics and its use of calculability, before applying it to Hindman's theorem, presenting a sketch of the most elementary proof, and the latest advances on this subject.
 Plus d'infos  


2020-02-06Semantics and applications of PORGY - an interactive modelling framework based on strategic graph rewriting
11:00-12:00
178
In this talk I will describe the use of strategic port graph rewriting as a basis for the implementation of visual modelling tools. The goal is to facilitate the specification and analysis of complex systems. A system is represented by an initial graph and a collection of graph rewrite rules, together with a user-defined strategy to control the application of rules. The traditional operators found in strategy languages for term rewriting have been adapted to deal with the more general setting of graph rewriting, and some new constructs have been included in the strategy language to deal with graph traversal and management of rewriting positions in the graph. We give a formal semantics for the language, examples of application in the areas of biochemistry, social networks and database design, and a brief description of its implementation: the graph transformation and visualisation tool PORGY.
This is joint work with members of the PORGY team at Bordeaux and King’s College London.
 Plus d'infos  


2020-02-04 Reachability in fixed dimension vector addition systems with states
14:00-15:00
178
The reachability problem is a central decision problem for formal verification based on vector addition systems with states (VASS), which are equivalent to Petri nets and form one of the most studied and applied models of concurrency. Reachability for VASS is also inter-reducible with a plethora of problems from a number of areas of computer science. In spite of recent progress, the complexity of the reachability problem remains unsettled, and it is closely related to the lengths of shortest VASS runs that witness reachability.
We consider VASS of fixed dimension, and obtain three main results. For the first two, we assume that the integers in the input are given in unary, and that the control graph of the given VASS is flat (i.e., without nested cycles). We obtain a family of VASS in dimension 3 whose shortest reachability witnessing runs are exponential, and we show that the reachability problem is NP-hard in dimension 7. These results resolve negatively questions that had been posed by the works of Blondin et al. in LICS 2015 and Englert et al. in LICS 2016, and contribute a first construction that distinguishes 3-dimensional flat VASS from 2-dimensional VASS.
Our third result, by means of a novel family of products of integer fractions, shows that 4-dimensional VASS can have doubly exponentially long shortest reachability witnessing runs. The smallest dimension for which this was previously known is 14.

Joint work with Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Filip Mazowiecki. Paper available at https://arxiv.org/abs/2001.04327
 Plus d'infos  


2020-01-28A separation result on min-plus and max-plus automata
07:00-07:00
178
Work in collaboration with Thomas Colcombet.

The talk shall start with an overview of min-plus and max-plus automata. These weighted automata realize functions which map words onto real numbers. We shall see that it may be thorny to give a description of their asymptotic behaviour. In contrast, it is pretty easy to study the functions realized by unambiguous weighted automata (with at most one accepting run for each input). It was known that a function that can be both realized by a min-plus and a max-plus automaton can actually be realized by an unambiguous one. We show a generalization of this result: if a function realized by a min-plus automaton is larger than a function realized by a max-plus automaton, then there exists an effectively computable unambiguous automaton which realizes a function in between. This result also applies on weighted tree automata.
 Plus d'infos  


2020-01-21Computational content of circular proof systems
07:00-07:00
178
Cyclic proofs are a class of formal proof systems that allow some kind of circular reasoning. Unlike classical proofs, represented by finite trees with axioms as leaves, cyclic proofs are represented by trees containing infinite branches. The Curry-Howard correspondence allows us to see these cyclic proofs as programs. We investigate the computational content of a cyclic proof system based on Kleene algebra, where we see expressions as data types. Different proofs of the same sequent e |- f can be interpreted as different programs mapping every input of type e to an output of type f. We show that depending on the particular rules allowed in the system, the computational content of proofs matches different known complexity classes: regular languages, LogSpace, primitive recursive functions, system T. Various tools are used to pinpoint these different expressive powers, including a newly introduced class of automata (Jumping Multihead Automata), and results from the field of reverse mathematics.

This is joint work with Laureline Pinault, Damien Pous, and Anupam Das.
 Plus d'infos  


2020-01-14Lempel-Ziv: A "one-bit catastrophe" but not a tragedy
07:00-07:00
178
LZ'78 is a famous and very simple lossless data compression algorithm published by Abraham Lempel and Jacob Ziv in 1978. Although widely used in practise, we know little about its stability. The one-bit catastrophe question, introduced by Jack Lutz in the late 90s, asks whether an infinite word compressible by LZ'78 can become incompressible by adding a single bit in front of it. Our main result is to answer that question positively. We also give tight bounds on the maximal possible variation between the compression ratio of a finite word and its perturbation (when one bit is added in front of it), showing that to get a "catastrophe", the initial word needs already to be close to the threshold of incompressibility.

This is a joint work with Sylvain Perifel.
 Plus d'infos  


2020-01-07Mixing sure, almost sure, exist and probable objectives in MDPs
07:00-07:00
178
We consider algorithms to decide the existence of strategies in MDPs for Boolean combinations of objectives. These objectives are omega-regular properties that need to be enforced either surely (whatever happens), almost surely (with probability one), existentially (it can happen), or with non-zero probability. Such a combination of properties could be e.g. that an agent reaches a target with high probability while guaranteeing it will not crash. We provide algorithms to solve the general case of Boolean combinations and we also investigate relevant subcases. We provide algorithms to solve the general case of Boolean combinations and we also investigate relevant subcases. We also report on complexity lower-bounds for these problems.
 Plus d'infos  


2019-12-17Using tropical geometry to obtain condition numbers of stochastic mean payoff games
07:00-07:00
178
In this talk, we introduce a condition number of stochastic mean payoff games. To do so, we interpret these games as feasibility problems over tropically convex cones. In this setting, the condition number is defined as the maximal radius of a ball in Hilbert's projective metric that is included in the (primal or dual) feasible set. We show that this conditioning controls the number of value iterations needed to decide whether a mean payoff game is winning. In particular, we obtain a pseudopolynomial bound for the complexity of value iteration provided that the number of random positions is fixed. We also discuss the implications of these results for convex optimization problems over nonarchimedean fields and present possible directions for future research.
The talk is based on joint works with X. Allamigeon, S. Gaubert, and R. D. Katz.
 Plus d'infos  


2019-12-10Algebraic tools for state complexity
07:00-07:00
178
Computing the state complexity of regular operations is usually a messy business. Every new operation needs to be carefully considered and the associated computations need to be tweaked. We present an attempt to generalize this process on a large class of rational operations, and use this framework to present new results.
 Plus d'infos  


2019-12-03Semantics of Functional Probabilistic Programs
14:00-15:00
178
Probabilities are extensively used in Computer Science. Algorithms use probabilistic choices for solving problems that are untracktable deterministically or for improving efficiency. Recently, (Functional) Probabilistic Programming has been introduced for applications in Machine Learning and Artificial Intelligence. Probabilistic programs are used to describe statistical models and for developing probabilistic data analysis.

As decisions in our society are often based on statistical models, it has become crucial to develop formal methods for probabilistic computing. The aim is to systemetize the analysis and certification of probabilistic programs.

In this talk, I will first introduce functional probabilistic programing and the related problems. Then, I will present recent works in denotational semantics of probabilistic computing and their applications.
 Plus d'infos  


2019-11-26Parameter Synthesis in Markov Models: An Overview
07:00-07:00
178
Markov models comprise states with probabilistic transitions..
The analysis of these models is ubiquitous and studied in,
among others, reliability engineering, artificial intelligence, systems biology, and formal methods.
Naturally, their analysis crucially depends on the transition probabilities.
Often, these probabilities are approximations based on data or reflect configurable parts of a modelled system.
To represent the uncertainty about the probabilities, we study parametric Markov models,
in which the probabilities are symbolic expressions rather than concrete values.

More precisely, we consider parametric Markov decision processes (pMDPs) and parametric Markov chains (pMCs) as special case.
Substitution of the parameters yields classical, parameter-free Markov decision processes (MDPs) and Markov chains (MCs).
A pMDP thus induces uncountably many MDPs.
Each MDP may satisfy reachability and reward properties, such as the maximal probability that the system reaches an `offline' state is less than 0.01%.
Lifting these properties to pMDPs yields fundamental problems asking, e.g., Is there an induced MDP satisfying the property?
We give an overview over such problems on a conceptual level, discuss their complexity, and survey both older and recent methods.
 Plus d'infos  


2019-11-19Learning probabilistic context-free grammars
07:00-07:00
178
In this talk I will present a solution to the following problem: given a set of strings, learn the underlying probabilistic context-free grammar generating these strings.

The main difficulty is that we observe strings and not (for instance) derivation trees.
In general, strings are not enough to identify a unique grammar (as for instance the string abc can be generated in various ways). I will introduce some structural properties ensuring this identifiability, and show that the corresponding class of probabilistic context-free grammars can be efficiently learned.
 Plus d'infos  


2019-11-12Monadic monadic second order logic
07:00-07:00
178
Monadic second order logic (MSO) is usually studied over specific kinds of structures, be it finite words, infinite words, finite or infinite trees, total orders of various shapes, etc. A monad is a rather abstract notion of "a kind of structures" that covers these and many other examples. One can formulate an abstract definition of MSO for a generic monad. I will explain how this is done, and I will describe some conditions that a monad should satisfy to ensure a basic "sanity check": that every definable language is recognized by a finite algebra.

Familiarity with monads is not necessary, I will give a gentle introduction.
(joint work with Mikolaj Bojanczyk and Julian Salamanca)
 Plus d'infos  


2019-11-05An equational modeling of asynchronous concurrent programming
07:00-07:00
178
Asynchronous programing is a widely spread technique offering some simple concurrent programing primitives that are restricted enough so that the resulting concurrent programs are, to some extent, dead-lock free. In this talk, I shall present the notion of monadic references that allows for formally defining a model of asynchronous concurrent programming as an extension of the usual model of (say) sequential monad programing.

I shall first review the notion of monadic programing, as popularized these last twenty years in typed functional programming languages such as Haskell. Then I will define in a progressive way what is asynchronous programing, how it relates with sequential programing, along with two series of simple equations capturing first, the basic semantics of promises and second, their asynchronous nature.

Various theorems derive from such an approach, formally proving the intuition long gain by programmers that, simply said, asynchronous concurrent programing with promises is as at least as simple as sequential programing, but with additional smoothness and optimisations possibilities provided by light concurrency.

If time permits, we may eventually prove that promises of (monadic) streams of data can be defined as (monadic) streams of promises of data, offering thus safe and robust ways to duplicate (monadic) streams in pure typed functional data flow programs.
 Plus d'infos  


2019-10-22Computing Nested Fixpoints in Quasipolynomial Time
07:00-07:00
178

In this talk, we will see how the main idea behind Calude et al.'s breakthrough quasipolynomial time algorithm for solving parity games extends to the computation of nested fixpoints of arbitrary set-functions. This result can alternatively be phrased as a fixpoint theorem stating that the iterative computation of nested fixpoints by approximation stabilizes after a quasipolynomial number of iterations. Furthermore we show that the problem of computing nested fixpoints is contained in both NP and Co-NP. Time admitting, we will also see how Zielonka's algorithm for parity games can be used to compute nested fixpoints of arbitrary set-functions.

These results find application in solving generalized parity games as well as model checking and satisfiability checking for extensions of the mu-calculus (e.g. graded, probabilistic or alternating-time), and prospectively in the computation of fair bisimulations and type checking for inductive-coinductive types.

The main message of all this is that many results and algorithms for solving parity games naturally generalize to the computation of nested fixpoints, pointing to a close relation between the two problems.
 Plus d'infos  


2019-10-15Simple Priced Timed Games are not That Simple
07:00-07:00
178

Priced timed games are two-player zero-sum games played on priced
timed automata (whose locations and transitions are labeled by
weights modeling the price of spending time in a state and executing
an action, respectively). The goals of the players are to minimise
or maximise the price to reach a target location.
While one can compute the optimal values that the players can achieve
(and their associated optimal strategies) when the weights are all
positive, this problem with arbitrary integer weights remains open.
In this talk, I will explain what makes this case more difficult and
show how to solve the problem for a subclass of priced timed
games (the so-called simple priced timed games).
 Plus d'infos  


2019-10-08Tradeoff between size and degree in Polynomial Calculus Resolution
07:00-07:00
178
Introduced by Cleggs et al. (STOC'96) to capture Gröbner basis computations, Polynomial Calculus Resolution (PCR) is an algebraic proof system for certifying the unsatisfiability of CNF formulas. Impagliazzo et al. (CC'99) established that if an unsatisfiable k-CNF formula over n variables has a refutation of small size in PCR (that is, polynomial size), then this formula also has a refutation of small degree, i.e., O(sqrt(n log n)). A natural question is to know whether we can achieve both small size and small degree in the same refutation.

A situation similar in spirit arises in the more classical resolution proof system where degree is replaced by width and size by length. In this setting, Thapen (TOC '16) adressed the tradeoff question by providing a negative answer: the decrease in width necessarily comes at the expense of an exponential blow-up in length.

Extending ideas from Thapen, our main result is to prove that a strong size-degree tradeoff is also necessary in PCR.

Joint work with Jakob Nordström, Dmitry Sokolov, Joseph Swernofsky
 Plus d'infos  


2019-10-01Les algorithmes de Parcoursup
07:00-07:00
178
« Parcoursup » est la plateforme nationale d’admission en première année de l’enseignement supérieur, mise en place en 2018 suite au vote de la loi ORE, en remplacement d’APB (Admission Post-Bac). Cette plateforme assure la mise en relation des formations du supérieur (licences, BTS, IUT, écoles, prépas, etc…) avec les candidats à ces formations, près de 900.000 en 2019.

Les algorithmes de Parcoursup envoient automatiquement et quotidiennement des propositions aux candidats, sur la base des voeux formulés par les candidats et des classements réalisés par les formations.

Je présenterai plusieurs aspects de ces algorithmes, de leur conception à leur implémentation et leur vérification.

Ces travaux ont été réalisés dans le cadre de ma mission auprès du MESRI, en collaboration avec Claire Mathieu.
 Plus d'infos  


2019-09-24Arbres infinis réguliers et revêtements universels de graphes finis
14:00-15:00
178
The notion of graph covering, from which we get that of a universal covering (an infinite tree) is important in the theory of distributed computing.
This aspect will be first reviewed by Yves Métivier.

Universal coverings of finite graphs are regular infinite trees, but not all of them. They can be characterized as the strongly regular trees, i.e. those trees that yield finitely regular rooted trees up to isomorphism when taking any vertex as a root. A few words will be said about a beautiful and difficult theorem by Leighton.
These facts will be presented by B. Courcelle (and also at BWG 2019).
 Plus d'infos  


2019-09-10Two variable fragment of Term Modal logic
14:00-15:00
178

Multi-modal logics are commonly used to reason about systems of processes. Typically, we have formulas of the form Box_i alpha where "i" comes from a fixed finite set of agents or processes. In dynamic networks, the number of agents cannot be fixed a priori, and may even change from state to state. We are thus led to Term Modal Logic (TML) where variables range over agent names and we have quantification of such variables; the logic has formulas such as forall x (P(x) implies Box_x alpha). Thus TML is a first order logic in which we can talk of agent properties as predicates and also use modalities to talk about the moves by agents. As expected, this logic is highly undecidable. In this talk we consider the two variable fragment of TML and prove that it is decidable. This is in contrast to two-variable First order modal logic, which is undecidable.

This is a joint work with Prof. R. Ramanujam and will be presented at MFCS, 2019.
 Plus d'infos  


2019-07-09 Most permissive semantics of Boolean networks
11:00-12:00
178

Dynamics of Boolean networks (BNs) are usually computed according to a
fixed update mode (synchronous, asynchronous, etc.). However, update
modes can miss important behaviours actually realisable in more concrete
multilevel or quantitative models. We introduce the most permissive
semantics of BNs which guarantees a correct over-approximation of
behaviours of any multilevel refinement. Moreover, it turns out that
analysing the most permissive dynamics of BNs is much simpler than with
update modes: reachability is PTIME (instead of PSPACE-complete), and
identifying attractors is NP-complete (instead of PSPACE-complete).
Therefore, computing reachable attractors become tractable to very large
networks, without any assumption on their structure. We conclude on the
impact for the synthesis of BNs from reachability and stability constraints.
https://arxiv.org/abs/1808.10240
 Plus d'infos  


2019-07-02Block products for algebras over countable words
11:00-12:00
178
We look at words which are mappings from a countable linear ordering to a finite alphabet. Finite words, Omega words etc satisfy the above condition. In this talk, we study the languages (of words) definable by different logics. We consider monadic second order logic, first order logic, linear temporal logic etc.
These logics can be characterized by an algebra called o-algebra and its subclasses. We first present a block product principle. Building on this, we generalize the well-known algebraic characterizations of first-order logic (resp. first-order logic with two variables) in terms of strongly (resp. weakly) iterated block products. We also explicate the role of block products for linear temporal logic by formulating a novel algebraic characterization of a natural fragment.

 Plus d'infos  


2019-06-25Solving Simple Stochastic Games with few RandomNodes faster using Bland’s Rule
11:00-12:00
178
A simple stochastic game, SSG for short, is a two-player zero-sum game, a turn-based version of stochastic games. SSGs were introduced by Condon and provide a general framework that allows to study algorithmic complexity issues underlying reachability objectives. The best algorithm so far for solving SSGs is Ludwig’s randomized algorithm which works in expected 2^O(sqrt(n)) time. We first give a simpler iterative variant of this algorithm, using Bland’s rule from the simplex algorithm, which uses exponentially less random bits than Ludwig’s version. Then, we show how to adapt this method to the algorithm of Gimbert and Horn whose worst case complexity is O(k!), where k is the number of random nodes. Our algorithm has an expected running time of 2^O(k) , and works for general random nodes with arbitrary outdegree and probability distribution on outgoing arcs.
 Plus d'infos  


2019-06-18Generic and Complete Algorithms for Straight-Line String Constraints
11:00-12:00
178
Path-feasibility is an important problem in the symbolic execution of
string-manipulating programs. A symbolic path is given as a finite,
loop-free sequence of assertions and assignments and the task is to find
concrete instantiations of the symbolic variables that satisfy all
assertions along the path. If such instantiations are found, then the
path is feasible. Such a path may witness an error in the program being
analysed. Recent research has identified a number of string operations
that can be supported by path-feasibility algorithms. We contribute two
semantic conditions, which, if satisfied by the assertions and
assignments in the program, imply decidability of the path-feasibility
problem. This decidability is shown via a generic feasibility-checking
algorithm. We have implemented this algorithm in a tool OSTRICH, which
checks satisfiability of straight-line string constraints (paths). We
have compared this tool with other leading solvers over a wide range of
popular benchmarks. OSTRICH is competitive on well-supported benchmarks,
while also increasing the expressivity and extensibility of the
string-constraints supported.
 Plus d'infos  


2019-06-11The many facets of string transducers
11:00-12:00
178
The talk will be a survey on some recent results about string transducers.
It is based on an invited talk at STACS’19 and a survey co-authored with Gabriele
Puppis. It will also address a result to appear at ICALP’19, about the decidability
of the equivalence problem for finitely valued streaming string transducers.
 Plus d'infos  


2019-06-04LambdaY-calculus with priorities
11:00-12:00
178
We will start with another view on alternating automata over finite
ranked trees. We will see an automaton as powerset algebra with a
monotone operation for each letter of the alphabet. Every automaton
determines a finite powerset algebra with operations, and every finite
powerset algebra determines an automaton.

The advantage of powerset algebras is that they can be easily made to
interpret simply typed lambda terms, while it is not obvious how to
run an automaton on a lambda-term. The correspondence between automata
and finite powerset algebras shows that finite powerset algebras can
recognize exactly the properties of simply-typed lambda-terms
expressible by tree automata.

The goal of this talk is to present a similar correspondence
but for parity automata and simply-typed lambda-terms with
fixpoints, known as lambdaY-terms. For this we need to restrict
lambdaY-terms to lambdaY-terms with priorities. As a counterpart
of finite powerset algebras we obtain not all parity automata but
only visibly-parity automata.

The talk will not assume a familiarity with the lambda-calculus.
 Plus d'infos  


2019-05-28Parity, Buchi, Weak
11:00-12:00
178
This talk is about the trade-offs between different acceptance
conditions for omega-word automata.

I will present recent improvements that bring the blow-up up incurred during
the translation of alternating parity automata into Buchi (and weak)
automata into line with the current algorithms solving parity games. I
will finish by discussing the gap between the upper and lower bounds for
this problem, and what it tells us about where to go next.

The technical part of this talk is based on currently unpublished work
with Laure Daviaud and Marcin Jurdzinski on quasi-polynomially sized
Buchi automata that use universal trees to recognise winning strategies
in infinite parity games of fixed width.
 Plus d'infos  


2019-05-21Kleene Algebras
11:00-12:00
178

Kleene Algebra (KA) is a paradigm for reasoning about equivalence between programs. Its (sound and complete) axioms allow us to answer verification questions such as "does program A refine specification B?" or "is this transformation semantics-preserving?". As a matter of fact, queries such as these can be answered mechanically.

In recent years, extensions and refinements of KA have been proposed, each of which can be applied to reason about different kinds of programs in more detail. The question then arises: can we find sound and complete axioms for these variants? And can equivalence queries be similarly mechanised? While each flavour of KA has its own idiosyncrasies, it turns out that there are some common techniques that pop up when considering these questions.

We start out with a brief introduction to KA, and then consider the features of three variants (synchronous, concurrent and guarded). For each variant, we discuss results and ongoing efforts towards axiomatisation and decidability, and the techniques that have proven successful so far.

This talk includes joint work with Paul Brunet, Nate Foster, Justin Hsu, Dexter Kozen, Bas Luttik, Jurriaan Rot, Alexandra Silva, Steffen Smolka, Jana Wagemaker and Fabio Zanasi.
 Plus d'infos  


2019-05-14On the power of symmetric linear programs
11:00-12:00
178
We consider families of symmetric linear programs (LPs) that decide a property of graphs in the sense that, for each size of graph, there is an LP defining a polyhedral lift that separates the integer points corresponding to graphs with the property from those corresponding to graphs without the property. We show that this is equivalent, with at most polynomial blow-up in size, to families of symmetric Boolean circuits with threshold gates. In particular, when we consider polynomial-size LPs, the model is equivalent to definability in a non-uniform version of fixed-point logic with counting. This is joint work with Albert Atserias and Anuj Dawar.
 Plus d'infos  


2019-05-07Topological Sorting under Regular Constraints
11:00-12:00
178
In this talk, I will present a joint work with Antoine Amarilli, published at ICALP 18 about what we call the constrained topological sorting problem (CTS): given a regular language K and a directed acyclic graph G with labeled vertices, determine if G has a topological sort that forms a word in K.

This natural problem applies to several settings, e.g., scheduling with costs or verifying concurrent programs. I will present a complexity study to solve this problem with respect to some properties of the target regular language.
 Plus d'infos  


2019-04-30Linearity in Higher-Order Recursion Schemes
11:00-12:00
178
Higher-Order Model-Checking (HOMC) has recently emerged as an approach
to automated verification of higher-order programs, prompted by Ong's
2006 result that Monadic Second Order Logic (MSO) is decidable on
infinite trees generated by Higher-Order Recursion Schemes (HORS).
Implementations report encouraging results despite an awful theoretical
worst case complexity.

In principle, HOMC algorithms work by reduction to Ong's theorem. In
practice, this often involves CPS translations which are costly in terms
of complexity, and so as to get tight complexity people have instead
reproved variations of Ong's theorem for extensions of HORS (with data,
or call-by-value) and drastically restricted fragments of MSO.

In this talk, I will introduce Linear HORS (LHORS), an extension of HORS
with additional type constructors imported from Linear Logic. Data and
call-by-value evaluation admit a finer translation to LHORS exploiting
the idea of linearly-used continuations. Moreover LHORS enjoy a
decidable model-checking problem, whose complexity essentially ignores
linear types. In this way we recover and extend several developments
that were originally proved independently of Ong's theorem.

This is joint work with Andrzej Murawski and Charles Grellois, presented
at POPL'18.
 Plus d'infos  


2019-04-16Faster k-SAT algorithms using biased-PPSZ
11:00-12:00
178

The PPSZ algorithm, due to Paturi, Pudlak, Saks and Zane, is currently
the fastest known algorithm for the k-SAT problem, for every k>3. For
3-SAT, a tiny improvement over PPSZ was obtained by Hertli. We introduce
a biased version of the PPSZ algorithm using which we obtain an
improvement over PPSZ for every k>=3. For k=3 we also improve on Herli's
result and get a much more noticeable improvement over PPSZ, though
still relatively small. In particular, for Unique 3-SAT, we improve the
current bound from 1.308^n to 1.307^n.

Joint work with Thomas Dueholm Hansen, Haim Kaplan and Or Zamir
 Plus d'infos  


2019-04-09Selection, Divergence, and Dichotomy
11:00-12:00
178
The Schnorr-Stimm dichotomy theorem concerns finite-state gamblers that bet on infinite sequences of symbols taken from a finite alphabet. The theorem asserts that, for each such sequence S, the following two things are true. 1. If S is normal in the sense of Borel (meaning that any two strings of equal length appear with equal asymptotic frequency in S), then every finite-state gambler loses money at an exponential rate betting on S. 2. If S is not normal, then there is a finite-state gambler that wins money at an exponential rate betting on S.
In this paper we use the Kullback-Leibler divergence (also known as the relative entropy) to generalize the dichotomy theorem to arbitrary probability measures on the alphabet and to quantify the exponential rates of winning and losing on the two sides of the dichotomy.

 Plus d'infos  


2019-04-02Parameterized synthesis of sequential transducers from rational relations over finite words
11:00-12:00
178
The synthesis problem asks, given a specification that relates possible inputs to allowed outputs, whether there is a program realizing the specification, and if so, construct one.

We consider synthesis of sequential transducers with synchronization parameters from rational relations over finite words. A sequential transducer is basically a deterministic finite automaton that outputs a finite word on each transition. A word relation can be represented by a set of synchronizations, called synchronization language. A synchronization of a pair of words is a single word where each position is annotated over {1,2}, which indicates whether it came from the input or output component, e.g., the synchronization (1a 2a 2b 1b 2a) represents the pair (ab,aba). The decision problems that have been studied so far either ask for synthesis by a synchronous sequential or by an arbitrary sequential transducer. We ask whether a sequential transducer whose allowed input/output behavior is specified by a given synchronization language can be synthesized from a given rational relation. The given synchronization language is referred to as synchronization parameter.

Recently, main classes of rational relations have been characterized in terms of admissible synchronization languages, and we study the above problem for different combinations of classes of rational relations and classes of synchronization languages. The problem is undecidable in general, because it is known to be undecidable whether an arbitrary sequential transducer can be synthesized from a rational relation. For automatic relations (also called synchronized rational relations) it is known that it is decidable whether an arbitrary sequential transducer or a synchronous sequential transducer can be synthesized. Regarding our framework, the key contribution is that it is decidable whether a sequential transducer whose synchronization language lies within a given "automatic" synchronization language can be synthesized from an automatic relation.
 Plus d'infos  


2019-03-26Reachability for Two-Counter Machines with One Test and One Reset
11:00-12:00
178
We prove that the reachability relation of two-counter machines with one zero-test and one reset is Presburger-definable and effectively computable. Our proof is based on the introduction of two classes of Presburger-definable relations effectively stable by transitive closure. This approach generalizes and simplifies the existing different proofs and it solves an open problem introduced by Finkel and Sutre in 2000.

This is a joint work with Alain Finkel and Jérôme Leroux.
 Plus d'infos  


2019-03-19A theory of assertions for Dolev-Yao models
11:00-12:00
178
We undertake an abstract study of certification in security protocols, concentrating on the logical properties and derivability of certificates. Specifically, we extend the Dolev-Yao model with a new class of objects called ‘assertions’, along with an associated algebra for deriving new assertions from old ones. We also provide a case study via the FOO e-voting protocol, and provide algorithms for the derivability problem and the active intruder problem for this system.
 Plus d'infos  


2019-03-12The complexity of mean payoff games using universal graphs
11:00-12:00
178
We study the computational complexity of solving mean payoff games. This class of games can be seen as an extension of parity games, and they have similar complexity status: in both cases solving them is in NP and coNP and not known to be in P. In a breakthrough result Calude, Jain, Khoussainov, Li, and Stephan constructed in 2017 a quasipolynomial time algorithm for solving parity games, which was quickly followed by two other algorithms with the same complexity. Our objective is to investigate how these techniques can be extended to the study of mean payoff games. We construct two new algorithms for solving mean payoff games. Our first algorithm depends on the largest weight N (in absolute value) appearing in the graph and runs in sublinear time in N, improving over the previously known linear dependence in N . Our second algorithm runs in polynomial time for a fixed number k of weights.
 Plus d'infos  


2019-03-05Betweenness in order-theoretical trees
11:00-12:00
178
The ternary betweenness relation on a tree, B(x,y,z), indicates that y is on the unique path between x and z. This notion can be extended to order-theoretic trees defined as partial orders such that the set of nodes greater than any node is linearly ordered. In such generalized trees, the unique "path" between two nodes can have infinitely many nodes. We axiomatize in first-order or monadic second-order logic several betweenness relations in order-theoretical trees.
 Plus d'infos  


2019-02-12Logic and random graphs
11:00-12:00
178
We look at properties of graphs that can be expressed in first order (FO) logic. Given such a property A and a class G of random graphs, we are interested in the limiting probability that a graph in G satisfies A, when the number of vertices goes to infinity.
First we survey what is known for the classical model G(n,p), including zero-one laws and the celebrated theorem of Shelah and Spencer. Then we move to classes of graphs defined by a global condition, such as being acyclic or planar, under the uniform distribution. We survey recent results on zero-one laws, convergence laws, and non-convergence phenomena, both in FO and in the stronger monadic second order (MSO) logic. In particular, for graphs embeddable in a fixed surface other than the sphere, there is a striking difference between the results in FO and MSO logic.
 Plus d'infos  


2019-02-05The power of programs over monoids taken from some small varieties of finite monoids
11:00-12:00
178
The computational model of programs over monoids, introduced by Barrington and Thérien in the late 1980s, gives a way to generalise the notion of (classical) recognition through morphisms into monoids in such a way that almost all open questions about the internal structure of the complexity class NC^1 can be reformulated as understanding what languages (and, in fact, even regular languages) can be program-recognised by monoids taken from some given variety of finite monoids. Unfortunately, for the moment, this finite semigroup theoretical approach did not help to prove any new result about the internal structure of NC^1 and, even worse, any attempt to reprove well-known results about this internal structure (like the fact that the language of words over the binary alphabet containing a number of 1s not divisible by some fixed integer greater than 1 is not in AC^0) using techniques stemming from algebraic automata theory failed.
In this talk, I shall present the model of programs over monoids, explain how it relates to "small" circuit complexity classes and present some of the contributions I made during my Ph.D. thesis to the understanding of the computational power of programs over monoids, focusing on the well-known varieties of finite monoids DA and J (giving rise to "small" circuit complexity classes well within AC^0). I shall conclude with a word about ongoing work and future research directions.
 Plus d'infos  


2019-01-29Ontology-Mediated Query Answering with OWL 2 QL Ontologies: Combined Complexity and Succinctness of Rewritings
11:00-12:00
178
The problem of ontology-mediated query answering (OMQA) has gained significant interest in recent years. One popular ontology language for OMQA is OWL 2 QL, a W3C standardized language based upon the DL-Lite description logic. This language has the desirable property that OMQA can be reduced to database query evaluation by means of query rewriting. In this talk, I will consider two fundamental questions about OMQA with OWL 2 QL ontologies: 1) How does the worst-case complexity of OMQA vary depending on the structure of the ontology-mediated query (OMQ)? In particular, under what conditions can we guarantee tractable query answering? 2) Is it possible to devise query rewriting algorithms that produce polynomial-size rewritings? More generally, how does the succinctness of rewritings depend on OMQ structure and the chosen format of the rewritings?
After classifying OMQs according to the shape of their conjunctive queries (treewidth, the number of leaves) and the existential depth of their ontologies, we will determine, for each class, the combined complexity of OMQ answering, and whether all OMQs in the class have polynomial-size first-order, positive existential and nonrecursive datalog rewritings. The succinctness results are obtained using hypergraph programs, a new computational model for Boolean functions, which makes it possible to connect the size of OMQ rewritings and circuit complexity.
This talk is based upon a recent JACM paper co-authored with Stanislav Kikot, Roman Kontchakov, Vladimir Podolskii, and Michael Zakharyaschev.
 Plus d'infos  


2019-01-22On the Boundedness Problem for Higher-Order Pushdown Vector Addition Systems
11:00-12:00
178
Karp and Miller's algorithm is a well-known decision procedure that solves the termination and boundedness problems for vector addition systems with states (VASS), or equivalently Petri nets. This procedure was later extended to a general class of models, well-structured transition systems, and, more recently, to pushdown VASS. In this paper, we extend pushdown VASS to higher-order pushdown VASS (called HOPVASS), and we investigate whether an approach à la Karp and Miller can still be used to solve termination and boundedness.

We provide a decidable characterisation of runs that can be iterated arbitrarily many times, which is the main ingredient of Karp and Miller's approach. However, the resulting Karp and Miller procedure only gives a semi-algorithm for HOPVASS. In fact, we show that coverability, termination and boundedness are all undecidable for HOPVASS, even in the restricted subcase of one counter and an order 2 stack. On the bright side, we prove that this semi-algorithm is in fact an algorithm for higher-order pushdown automata. This is a joint work with Sylvain Salvati and Grégoire Sutre.
 Plus d'infos  


2019-01-15Beyond admissibility: Dominance between chains of strategies
11:00-12:00
178
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.
 Plus d'infos  


2019-01-08Unambiguous Register Automata
11:00-12:00
178
In the literature we find many computation models whose expressiveness goes beyond finite automata, however without attaining the full power of Turing machines. The common practice is to enrich finite automata with some internal memory (e.g. counters, clocks, stacks, etc.) that can be used to store, manipulate, and compare data from a potentially infinite domain. An intriguing model that results from this practice is the model of register automaton, which is essentially a finite automaton equipped with a finite number of registers. Register automata are used to recognize languages over infinite alphabets. The deterministic, unambiguous, and non-deterministic variants of these automata form a hierarchy of strictly increasing expressive power, where the bottom and top levels have, respectively, decidable and undecidable equivalence problems. Accordingly, the intermediate class of unambiguous register automata is an interesting object of study, since it is believed to be robust and algorithmically well-behaved.

In this talk I will present some preliminary results obtained with Thomas Colcombet and Michal Skrzypczak towards proving the following conjecture: unambiguous register automata have a decidable equivalence problem and form the largest subclass of non-deterministic register automata that is closed under complement.
 Plus d'infos  


2018-12-18Reasoning over Existential Rules with Acyclicity Notions
11:00-12:00
178
The chase is a sound and complete (albeit non-terminating) algorithm for conjunctive query answering over ontologies of existential rules. On the theoretical side, we develop sufficient conditions to guarantee its termination (i.e., acyclicity notions), and study several restrictions that furthermore ensure its polynomiality. On the practical side, we empirically study the generality of these conditions and we extend the Datalog engine VLog to develop an efficient implementation of the chase. Furthermore, we conduct an extensive evaluation, and show that VLog can compete with the state of the art, regarding runtime, scalability, and memory efficiency.
 Plus d'infos  


2018-12-11When are Emptiness and Containment Decidable for Probabilistic Automata?
11:00-12:00
178
The emptiness and containment problems for probabilistic automata are natural quantitative generalisations of the classical language emptiness and inclusion problems for Boolean automata. It is well known that both problems are undecidable. In this paper we provide a more refined view of these problems in terms of the degree of ambiguity of probabilistic automata. We show that a gap version of the emptiness problem (that is known be undecidable in general) becomes decidable for automata of polynomial ambiguity. We complement this positive result by showing that the emptiness problem remains undecidable even when restricted to automata of linear ambiguity. We then turn to finitely ambiguous automata. Here we show decidability of containment in case one of the automata is assumed to be unambiguous while the other one is allowed to be finitely ambiguous. Our proof of this last result relies on the decidability of the theory of real exponentiation, which has been shown, subject to Schanuel's Conjecture, by Macintyre and Wilkie.
 Plus d'infos  


2018-12-04Data generation for programme synthesis
11:00-12:00
178
Programming by example is the problem of synthesising a program from a small set of pairs input and output. Despite having found applications in several areas it is notoriously computationally expensive. Recent works have considered hybrid approaches combining ML and PL based techniques. These techniques require generating a training dataset, which leads to significant difficulties related to finding the most informative inputs to characterise a given programme.

In this paper we show that the data generation procedure has a significant impact on performance. The novelty of our approach relies on using an SMT solver to synthesize meaningful inputs with varied behaviour for a given program. By testing against several distributions, we show that our constraint-based approach improves on the generalizability of the models. Our results are consistent across two common learning architectures used in previous work.
 Plus d'infos  


2018-11-20Optimal bounds for single-source Kolmogorov extractors
11:00-12:00
178
The rate of randomness (or dimension) of a binary string x is the ratio C(x)/|x| where C(x) is the Kolmogorov complexity of x. While it is known that a single computable transformation cannot increase the rate of randomness of all strings, Fortnow et al. showed that for any 0
This is joint work with Barbara Csima and Matthew Harrison-Trainor
 Plus d'infos  


2018-11-13Complexity bounds for bisimulation equivalence in first-order grammars
11:00-12:00
178
Following Géraud Sénizergues' seminal results twenty years ago on the decidability of language equivalence of deterministic pushdown automata and of (weak) bisimilation equivalence of (epsilon-popping) pushshdown automata, several works have attempted to provide complexity bounds for these problems. For instance, some significant simplifications over the original proofs were provided by Colin Stirling and Petr Jancar, using in particular the formalism of first-order grammars instead of pushdown automata, and resulting in Tower upper bounds for the language equivalence problem in deterministic systems. But no complexity bounds were known for the bisimulation equivalence problem.

In this talk, I will cover some work in progress with Petr Jancar. Using a recent reformulation of the proofs for checking bisimulation equivalence as a black box, I will show how to provide Ackermannian upper bounds for the crucial step, which is the computation of a so-called `candidate basis'. This entails that the decision problem itself is Ackermann-complete, thanks to a lower bound proven by Petr Jancar a few years ago; this is the first known completeness result in this entire line of work.
 Plus d'infos  


2018-11-06The Reachability Problem for Petri Nets is Not Elementary
11:00-12:00
178
Petri nets, also known as vector addition systems, are a long established and widely used model of concurrent processes. The complexity of their reachability problem is one of the most prominent open questions in the theory of verification. That the reachability problem is decidable was established by Mayr in his seminal STOC 1981 work, and the currently best upper bound is non-primitive recursive cubic-Ackermannian of Leroux and Schmitz from LICS 2015. We show that the reachability problem is not elementary. Until this work, the best lower bound has been exponential space, due to Lipton in 1976.

Joint work with Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Filip Mazowiecki.
 Plus d'infos  


2018-10-23Foundations of Complex Event Processing
11:00-12:00
178
Complex event processing (CEP) emerges as a unified technology for efficiently processing data streams. Contrary to data streams management systems, CEP query languages model data streams as a continuous sequence of events and CEP queries define sets of events (complex events) that are of interest for the final user.

In this talk, I will present our recent proposal for giving formal foundations to complex event processing. First, I will introduce complex event logic (CEL), a logical language for extracting complex events, that captures the main features used by CEP systems in practise. Then I will show how to efficiently represent CEL queries through so-called complex event automata, which are symbolic transducers that produce complex events from data streams. Then I will explain how to evaluate complex event automata with constant delay algorithms and present some preliminaries experimental results that show how our approach is order of magnitudes faster than current CEP systems developed in academy and industry. Finally, I will discuss some open problems regarding the connection between automata models, transducers, and constant delay algorithms.
 Plus d'infos  


2018-10-09It Is Easy to Be Wise After the Event: Communicating Finite-State Machines Capture First-Order Logic with "Happened Before"
11:00-12:00
178
Message sequence charts (MSCs) naturally arise as executions of communicating finite-state machines (CFMs), in which finite-state processes exchange messages through unbounded FIFO channels. We study the first-order logic of MSCs, featuring Lamport's happened-before relation. We introduce a star-free version of propositional dynamic logic (PDL) with loop and converse. Our main results state that (i) every first-order sentence can be transformed into an equivalent star-free PDL sentence (and conversely), and (ii) every star-free PDL sentence can be translated into an equivalent CFM. This answers an open question and settles the exact relation between CFMs and fragments of monadic second-order logic. As a byproduct, we show that first-order logic over MSCs has the three-variable property.
This is joint work with Benedikt Bollig and Paul Gastin, presented at CONCUR’18.
 Plus d'infos  


2018-10-02Languages over countable linear orderings
11:00-12:00
178
We look at words which are mappings from a countable linear ordering to a finite alphabet. Finite words, Omega words etc satisfy the above condition. We will also look at other kind of words.
In this talk, we study the languages (of words) definable by different logics. We consider first order logic, weak monadic second order logic, two variable fragments and a host of other logics. We are interested in the relationship between these logics. Are these logics expressively different?

We will show that all these logics can be characterized by an algebraic structure called o-algebra and its subclasses. This helps us compare the respective expressive power of these logics. Moreover, since there is an effective translation to o-algebras from formulas, we have decidability for the satisfiability problem.
 Plus d'infos  


2018-09-25Closure properties of synchronized relations
11:00-12:00
178
A standard approach to define k-ary word relations over a finite alphabet A is through k-tape finite state automata that recognize regular languages L over {1, ... , k} x A, where (i,a) is interpreted as reading letter a from tape i. Accordingly, a word w in L denotes the tuple (u_1, ... , u_k) of words over A in which u_i is the projection of w onto i-labelled letters. While this formalism defines the well-studied class of Rational relations, enforcing restrictions on the reading regime from the tapes, which we call "synchronization", yields various sub-classes of relations. Such synchronization restrictions are imposed through regular properties on the projection of the language L onto {1, ... , k}. In this way, for each regular language C over the alphabet {1, ... , k}, one obtains a class Rel(C) of relations. Synchronous, Recognizable, and Length-preserving rational relations are all examples of classes that can be defined in this way.
We study basic properties of these classes of relations, in terms of closure under intersection, complement, concatenation, Kleene star and projection. In each case we characterize the classes with the property through a decidable property.
 Plus d'infos  


2018-07-03Ontology-mediated query answering for expressive description logics, or yet another family of (potentially) decidable fragments of first-order logic
11:00-12:00
178
Evaluating queries in the presence of background knowledge has been extensively studied in several communities. In database theory, it is known as query answering under integrity constraints: given a finite database instance and a set of constraints, determine answers to a query that are certain to hold over any extension of the given instance that satisfies the constraints. In the knowledge representation community, the database instance and the set of constraints are treated as a single object, called an ontology, but otherwise the problem remains the same, except that different kinds of constraints are interesting. While in database theory constraints are usually very simple, like functionality of relations, or inclusions between relations, in knowledge representation more expressive logics are used. I will focus on so called description logics, which are a family of extensions of modal logic. I will cover some basic techniques, a highly non-trivial result by Rudolph and Glimm (2010), as well as some recent results obtained with Tomek Gogacz (U Warsaw) and Yazmin Ibanez-Garcia (TU Wien).
 Plus d'infos  


2018-06-26On Jeandel-Rao aperiodic tilings
11:00-12:00
178
In 2015, Jeandel and Rao showed by exhaustive computer search that every Wang tile set of cardinality <=10 either admit a periodic tiling of the plane or admit no tiling of the plane at all. Moreover, they found a Wang tile set of cardinality 11 which admits tilings of the plane but never periodically. Their algorithm is based on the representation of Wang tilings as the execution of a transducer on biinfinite sequences. In this talk, we present an alternate definition of the aperiodic tilings of Jeandel-Rao as the coding of a $mathbb{Z}^2$-action on the torus. We conjecture that it is a complete characterization.
 Plus d'infos  


2018-06-19Semi-deterministic automata: How to obtain and complement them
11:00-12:00
178
Semi-deterministic Büchi automata (sDBA) are useful for example in model checking of probabilistic systems or in termination analysis. While in probabilistic model checking sDBA represent the set of behaviours of interest, in termination analysis they represent terminating behaviours of programs and are often complemented to perform a language difference. In my talk, I first introduce the class of semi-deterministic Büchi automata (sDBA). Then I will explain how can we convert nondeterministic Büchi automata (NBA) into sDBA, followed by a discussion on how to efficiently convert generalized Büchi automata into sDBA. After we learn how to build sDBA, I will introduce a complementation algorithm sDBA. The algorithm produces a complement automata with at most 4^n states while the best upper bound on complementation of NBA is O((0.76n)^n). Further, our algorithm produces automata with a very low degree of nondeterminism, indeed, the resulting automata are even unambiguous.
 Plus d'infos  


2018-06-12Undecidability of MSO+“ultimately periodic”
11:00-12:00
178
We prove that MSO on omega-words becomes undecidable if allowing to quantify over sets of positions that are ultimately periodic, i.e., sets X such that for some positive integer p, ultimately either both or none of positions x and x+p belong to X. We obtain it as a corollary of the undecidability of MSO on omega-words extended with the second-order predicate U1(X) which says that the distance between consecutive positions in a set X of naturals is unbounded. This is achieved by showing that adding U1 to MSO gives a logic with the same expressive power as MSO+U, a logic on omega-words with undecidable satisfiability.

This is joint work with Mikolaj Bojanczyk, Laure Daviaud, Vincent Penelle and Sreejith.
 Plus d'infos  


2018-06-05A pseudo-quasi-polynomial algorithm for mean-payoff parity games
11:00-12:00
178
In a mean-payoff parity game, one of the two players aims both to achieve a qualitative parity objective and to minimize a quantitative long-term average of payoffs (aka. mean payoff). The game is zerosum and hence the aim of the other player is to either foil the parity objective or to maximize the mean payoff.
I will present a pseudo-quasi-polynomial algorithm for solving mean-payoff parity games. All algorithms for the problem that have been developed for over a decade have a pseudo-polynomial and an exponential factors in their running times; in the running time of our algorithm the latter is replaced with a quasi-polynomial one.
 Plus d'infos  


2018-05-22Verification of Asynchronous Programs with Nested Locks
11:00-12:00
178
We consider asynchronous programs consisting of multiple recursive threads (modeled as pushdown systems) running in parallel. Each of the threads is equipped with a multi-set. The threads can create tasks and post them onto the multi-sets or read a task from their own. In addition, they can synchronize through a finite set of locks. We examine the decidability of the state reachability problem for this model. The problem is already known to be undecidable for a system consisting of two recursive threads (and no tasks) and we examine a decidable subclass.

In the first half of the talk we survey, quickly, the previous results for recursive programs communicating via locks and in the second half we will describe our results on the asynchronous program model.

Based on Joint work with M.F. Atig, A. Bouajjani and P. Saivasan.
 Plus d'infos  


2018-05-15Modelling replicated data stores with multiple correctness levels
11:00-12:00
178
Replicated data stores typically sacrifice strong consistency guarantees in favour of availability and partition tolerance. These data stores usually provide specific weaker consistency guarantees, such as eventual consistency, monotonic reads or causal consistency.

Recently, there have been proposals for data stores that support multiple consistency guarantees. An example is a speculative response based on a quick local check, followed by either a confirmation or an "apology" after a more detailed reconciliation of updates. A typical situation is an online purchase where the order is initially confirmed and later you are told the item is out of stock.

We describe a formal semantics for replicated data-stores with multiple correctness levels and explore decidability issues.

This is ongoing joint work with Ahmed Bouajjani, Constantin Enea, Gautham Shenoy R and S P Suresh.
 Plus d'infos  


2018-04-24The isomorphism problem for virtually free group
11:00-12:00
178
Since Muller and Schupp's result it is well-known that the finitely generated virtually free groups are precisely the context-free groups. The isomorphism problem for virtually free groups, has shown to be decidable by Kristic. In the special case that the input groups are either given as context-free grammars for their word problems or as so-called virtually free presentations, it is primitive recursive by the work of Sénizergues.
In this talk I will present an elementary time solution for these two special cases. The proof is based on analyzing the structure trees assigned to the Cayley graphs of the input groups. By Bass-Serre theory this yields graphs of groups which can be tested for isomorphism as in Kristic's algorithm.
The talk is based on joint work with Géraud Sénizergues and Volker Diekert.
 Plus d'infos  


2018-04-17Arithmetic circuits as automata, and applications
11:00-12:00
178
We give a syntactic correspondence between non-associative arithmetic circuits and acyclic weighted tree automata. We may then export results from automata theory to non-associative circuits and characterize the size of a minimal circuit for a given polynomial as the rank of a Hankel matrix. We will then show how this can be used to re-obtain Nisan's theorem on Algebraic Branching Programs as well as recent results on Unique Parse Tree circuits. Lastly, we will highlight a new way of obtaining lower bounds for general (associative) arithmetic circuits.
 Plus d'infos  


2018-04-10The State Complexity of Alternating Automata
11:00-12:00
178
We study the complexity of languages of finite words using automata theory. To go beyond the class of regular languages, we consider infinite automata and the notion of state complexity defined by Karp. We look at alternating automata as introduced by Chandra, Kozen and Stockmeyer: such machines run independent computations on the word and gather their answers through boolean combinations.
We devise a lower bound technique relying on boundedly generated lattices of languages, and give two applications of this technique. The first is a hierarchy theorem, stating that there are languages of arbitrarily high polynomial alternating state complexity, and the second is a linear lower bound on the alternating state complexity of the prime numbers written in binary. This second result strengthens a result of Hartmanis and Shank from 1968, which implies an exponentially worse lower bound for the same model.
To be presented at LICS'18.
 Plus d'infos  


2018-04-03On Rotating Q-Automata
11:00-12:00
178
I present results on rotating Q-automata, which are (memoryless) automata with weights in Q that can read the input tape from left to right several times. We show that the series realized by valid rotating Q-automata are Q-Hadamard series (which are the closure of Q-rational series by pointwise inverse), and that every Q-Hadamard series can be realized by such an automaton. We prove that, although validity of rotating Q-automata is undecidable, the equivalence problem is decidable on rotating Q-automata. Finally, we prove that every valid two-way Q -automaton admits an equivalent rotating Q-automaton. The conversion, which is effective, implies the decidability of equivalence of two-way Q-automata.
 Plus d'infos  


2018-03-27Limitations of treewidth for problems beyond NP.
11:00-12:00
178
***Joint seminar with Graphes et Optimisation***

In this seminar, we will take a closer look at the parameterized complexity of existsforallSAT, the prototypical complete problem of the class $Sigma^p_2$, the second level of the polynomial hierarchy. We will provide tight fine-grained bounds on the complexity of this problem with respect to the most important structural graph parameters. Specifically we will show that existsforallSAT cannot be solved in time $2^{2^{o(tw)}}$ under the Exponential Time Hypothesis. More strongly, we establish the same bound with respect to the formula’s primal vertex cover, a much more restrictive measure. Our reduction is a 'textbook' reduction that could be used in order to provide similar lower bounds for problems in the second level of the polynomial hierarchy.
 Plus d'infos  


2018-03-20Asymptotic Bounds on Termination Time in VASS
11:00-12:00
178
Vector Addition Systems with States (VASS) provide a well-known and fundamental model for the analysis of concurrent processes, parametrized systems, and are also used as abstract models of programs in resource bound analysis. We study the problem of obtaining asymptotic bounds on the termination time of a given VASS. In particular, we focus on the practically important case of obtaining polynomial bounds on termination time. First, I will present a characterization for VASS with linear asymptotic complexity. I will also show that if a complexity of a VASS is not linear, it is at least quadratic.
Second, I will talk about classification of VASS according to quantitative properties of their cycles. I will show that certain singularities in these properties are the key reason for their non-polynomial asymptotic complexity. In absence of singularities, I will show that the asymptotic complexity is always polynomial and of the form Theta(n^k), for some integer k <= d. I will present a polynomial-time algorithm computing the integer k. The results are based on insights into the geometry of VASS dynamics, which hold the potential for further applicability to VASS analysis.
 Plus d'infos  


2018-03-13Polynomial Vector Addition Systems With States
11:00-12:00
178
The reachability problem for vector addition systems is one of the most difficult and central problem in theoretical computer science. The problem is known to be decidable, but despite instance investigations during the last four decades, the exact complexity is still open. For some sub-classes, the complexity of the reachability problem is known. Structurally bounded vector addition systems, the class of vector addition systems with finite reachability sets from any initial configuration, is one of those classes. In fact, the reachability problem was shown to be polynomial-space complete for that class by Praveen and Lodaya in 2008. Surprisingly, extending this property to vector addition systems with states is open. In fact, there exist vector addition systems with states that are structurally bounded but with Ackermannian large sets of reachable configurations. It follows that the reachability problem for that class is between exponential space and Ackermannian. In this paper we introduce the class of polynomial vector addition systems with states, defined as the class of vector addition systems with states with size of reachable configurations bounded polynomially in the size of the initial ones. We prove that the reachability problem for polynomial vector addition systems is exponential-space complete. Additionally, we show that we can decide in polynomial time if a vector addition system with states is polynomial. This characterization introduces the notion of iteration scheme with potential applications to the reachability problem for general vector addition systems.
 Plus d'infos  


2018-03-06The hydra and the rooster
11:00-12:00
178
The Hydra game was introduced in 1982 by the mathematicians L. Kirby and J. Paris in their article: "Accessible Independence Results for Peano Arithmetic".
This article contains two theorems:

1. Whichever the strategy of Hercules and the Hydra, any battle eventually terminates with Hercules' victory.
2. The previous result cannot be proved in Peano Arithmetic.

We present a formal, self-contained (axiom-free) proof of a variant of both theorems, with the help of the Coq proof assistant.

Since Coq's logic is higher-order intuitionnistic logic, the reference to Peano Arithmetic is replaced with a study of a class of proofs of termination indexed by ordinal numbers less or equal than epsilon_0.

We present the main parts of this proof, as well as the main features of Coq that made its construction possible.
 Plus d'infos  


2018-02-27Resynchronizing Classes of Word Relations
11:00-12:00
178
A natural approach to defining binary word relations over a finite alphabet A is through two-tape finite state automata, which can be seen as regular languages L over the alphabet {1,2}xA, where (i,a) is interpreted as reading letter a from tape i. Thus, a word w of the language L denotes the pair (u_1,u_2) in A* x A* in which u_i is the projection of w onto i-labelled letters. While this formalism defines the well-studied class of Rational relations (a.k.a. non-deterministic finite state transducers), enforcing restrictions on the reading regime from the tapes, that we call synchronization, yields various sub-classes of relations. Such synchronization restrictions are imposed through regular properties on the projection of the language onto {1,2}. In this way, for each regular language C contained in {1,2}*, one obtains a class Rel(C) of relations, such as the classes of Regular, Recognizable, or length-preserving relations, as well as (infinitely) many other classes.

We study the problem of containment for synchronized classes of relations: given C,D sub-languages of {1,2}*, is Rel(C) contained in Rel(D)? We show a characterization in terms of C and D which gives a decidability procedure to test for class inclusion. This also yields a procedure to re-synchronize languages from {1,2}xA preserving the denoted relation whenever the inclusion holds.
 Plus d'infos  


2018-02-13 Complementing the languages of unambigous automata
11:00-12:00
178
Unambiguous non-deterministic finite automata have intermediate
expressive power and succinctness between deterministic and
non-deterministic automata.

It has been conjectured that every unambiguous non-deterministic one-way
finite automaton (1UFA) recognizing some language L can be converted
into a 1UFA recognizing the complement of the original language L with
polynomial increase in the number of states.

A counterexample to this conjecture using only the 1-letter alphabet
will be presented.
 Plus d'infos  


2018-02-06The Complexity of Decision Problems for Recognizing Morphisms
11:00-12:00
178
We discuss the complexity of decision problems on regular languages represented by morphisms to finite semigroups. There are two canonical ways of specifying the semigroup: giving its multiplication table or an implicit description as the subsemigroup of a transformation semigroup (generated by the images of the given morphism). For both representations, we will consider

* the membership problem,

* the emptiness/universality/inclusion/equivalence problems,

* the intersection non-emptiness problem,

and their restrictions to a certain classes of finite semigroups.
Complexity results and open problems will be presented.
 Plus d'infos  


2018-01-30Animation 3D et produit semi-direct
11:00-12:00
178
We define a simple and sound mathematical framework for describing temporal media programming language semantics based on the various concepts offered by semigroup theory. As a result a fairly general programming scheme can be defined in order to specify, compose and render both spatial media objects (e.g. 3D drawings) and timed media objects (e.g. Animation or Music). As an example, a simple monoid based semantics model of the turtle command language of Logo is detailed and extended throughout.

Joint work with Simon Archipoff
 Plus d'infos  


2018-01-23Pumping lemmas for weighted automata
11:00-12:00
178
We present three pumping lemmas for three classes of functions definable by fragments of weighted automata over the min-plus semiring and the semiring of natural numbers. As a corollary we show that the hierarchy of functions definable by unambiguous, finitely-ambiguous, polynomially-ambiguous weighted automata, and the full class of weighted automata is strict for the min-plus semiring.

This is joint work with Cristian Riveros to be presented at stacs 2018.
 Plus d'infos  


2018-01-09Simulabilité à mémoire finie de lois de probabilités continues
11:00-12:00
178
On s'intéresse à la question de la simulation exacte de lois de probabilités continues sur les réels, et plus précisément, à identifier quelles lois sont simulables exactement en n'utilisant qu'une mémoire finie - le modèle naturel étant une variante d'automates probabilistes, mais il est facile de voir que divers modèles sont équivalents (au moins au sens probabiliste de "presque sûrement").

Le premier résultat sur la question est une condition nécessaire dûe à Knuth et Yao, il y a plus de 40 ans: une loi à densité, et dont la densité est donnée par une fonction analytique, n'est pas simulable par automate si sa densité n'est pas en fait donnée par un polynôme. Je présenterai des résultats récents, qui permettent de caractériser les lois simulables parmi celles dont la densité est donnée par une fonction polynomiale par morceaux (de manière semi constructive dans le cas positif); et je discuterai de possibles extensions au cas multidimensionnel.
 Plus d'infos  


2017-12-12La coloration de graphe dans le modèle LOCAL - Partie II
11:00-12:00
178
Partie II:
- Coloration rapide des cycles
- Borne inférieure en log* sur la coloration des cycles (preuve de Linial)
- Une preuve alternative fondé sur le théorème de Ramsey
- Etat de l'art
 Plus d'infos  


2017-12-05La coloration de graphe dans le modèle LOCAL - Partie I
11:00-12:00
178
L'objectif de cette série d'exposés est de faire découvrir un résultat aussi élégant que surprenant du calcul distribué, à savoir la 3-coloration des n-cycles en temps log*(n). On démontrera l'optimalité de ce résultat ainsi que ces généralisations au cas des graphes arbitraires.

Partie I:
- Le modèle LOCAL
- Le problème de la coloration
- Coloration des 1-orientations en 6 couleurs
- De 6 à 3 couleurs
- Cas des graphes arbitraires
 Plus d'infos  


2017-11-28Succinct progress measures and solving parity games in quasi-polynomial time
11:00-12:00
178
The recent breakthrough paper by Calude et al. (a winner of STOC 2017 Best Paper Award) has given the first algorithm for solving parity games in quasi-polynomial time, where previously the best algorithms were mildly sub-exponential. We devise an alternative quasi-polynomial time algorithm based on progress measures, which allows us to reduce the space required from quasi-polynomial to nearly linear. Our key technical tools are a novel concept of ordered tree coding, and a succinct tree coding result that we prove using bounded adaptive multi-counters, both of which are interesting in their own right.

Apart from presenting our technical work on succinct progress measures, I will survey the relevance of parity games to the theory and practice of computer-aided verification and synthesis, their surprising impact on broader theoretical computer science, the history of results and techniques used for solving parity games, and the recent advances in the state of the art.

This is joint work with Marcin Jurdzinski.
 Plus d'infos  


2017-11-21Model Checking: the Interval Way
11:00-12:00
178
Model checking with interval temporal logics is emerging as a viable alternative to model checking with standard point-based temporal logics, such as LTL, CTL, CTL*, and the like. The behavior of the system is modelled by means of (finite) Kripke structures, as usual. However, while temporal logics which are interpreted "point-wise" describe how the system evolves state-by-state, and predicate properties of system states, those which are interpreted "interval-wise" express properties of computation stretches, spanning a sequence of states. A proposition letter is assumed to hold over a computation stretch (interval) if and only if it holds over each component state (homogeneity assumption). The most well-known interval temporal logic is Halpern and Shoham's modal logic of time intervals HS, which features one modality for each possible ordering relation between a pair of intervals, apart from equality. In the seminar, we provide an overview of the main results on model checking with HS and its fragments under the homogeneity assumption. In particular, we show that the problem turns out to be non-elementarily decidable and EXPSPACE-hard for full HS, but it is often computationally much better for its fragments. Then, we briefly compare the expressiveness of HS in model checking with that of LTL, CTL, CTL*. We conclude by discussing a recent generalization of the proposed MC framework that allows one to use regular expressions to define the behavior of proposition letters over intervals in terms of the component states.
 Plus d'infos  


2017-11-14Reunion d'equipe MF
11:00-12:00
178
 Plus d'infos  


2017-11-07Formal methods for capturing dynamics of biological networks
11:00-12:00
178
Computational models of biological networks aim at reporting the indirect influences between the different molecular entities acting within the cell (genes, RNA, proteins, ...). In this talk, I will give an overview of methods for the formal assessment of dynamics of biological networks by static analysis. After an introduction to Boolean networks and their relevance for modelling cell signalling and gene regulatory networks, I'll present an abstract interpretation of their trajectories based on a causal analysis. Then, I'll show how we can combine this abstraction with SAT approches to address systems biology challenges, such as model identification and cell reprogramming.
 Plus d'infos  


2017-10-31Rewriting Higher-order Stack Trees
11:00-12:00
178
Higher-order pushdown systems and ground tree rewriting systems can be seen as extensions of suffix word rewriting systems. Both classes generate infinite graphs with interesting logical properties. Indeed, the satisfaction of any formula written in monadic second order logic (respectively first order logic with reachability predicates) can be decided on such a graph.

The purpose of this talk is to propose a common extension to both higher-order stack operations and ground tree rewriting. We introduce a model of higher-order ground tree rewriting over trees labelled by higher-order stacks (henceforth called stack trees), which syntactically coincides with ordinary ground tree rewriting at order 1 and with the dynamics of higher-order pushdown automata over unary trees. The rewriting system is obtained through the definition of DAGs of operations.

Our contribution is twofold (apart from the definition of the model):
- define a automaton model over DAGs of operations, and show it is closed under iteration.
- showing that the model checking problem for first-order logic with reachability is decidable for the infinite graphs generated by stack tree rewriting systems. This last proof uses the technique of finite set interpretations presented by Colcombet and Loding.
 Plus d'infos  


2017-10-24Constructive completeness for the linear-time mu-calculus
11:00-12:00
178
Modal mu-calculus is one of the central logics for verification. In his seminal paper, Kozen proposed an axiomatization for this logic, which was proved to be complete, 13 years later, by Kaivola for the linear-time case and by Walukiewicz for the branching-time one. These proofs are based on complex, non-constructive arguments, yielding no reasonable algorithm to construct proofs for valid formulas. The problematic of constructiveness becomes central when we consider proofs as certificates, supporting the answers of verification tools. We provide a new completeness argument for the linear-time mu-calculus which is constructive, i.e. it builds a proof for every valid formula. To achieve this, we decompose this difficult problem into several easier ones, taking advantage of the correspondence between the mu-calculus and automata theory. More precisely, we lift the well-known automata transformations (non-determinization for instance) to the logical level. To solve each of these smaller problems, we perform first a proof-search in a circular proof system, then we transform the obtained circular proofs into proofs in Kozen's axiomatization. This yields a constructive proof for the full linear-time mu-calculus.
 Plus d'infos  


2017-10-17 Timed domains: an appetizer
11:00-12:00
178
we develop a general theory of timed domains and timed morphisms that aims at offering a versatile and sound mathematical framework for the study of timed denotational semantics of networks of timed programs. The proposed compositional semantic model accounts for the fact that every non trivial computation step necessarily takes some non zero time. This is achieved by defining timed domains as classical domains (directed complete posets) where time appears everywhere: every increase of knowledge necessarily refers to the passage of time. Timed morphisms are defined as functions between timed domains which uniformly act on the underlying time scales. The resulting category is a (bi)cartesian closed category with (mostly) internal henceforth timed least fixpoint operators. Moreover, by allowing (almost) arbitrary posets as time scales, the proposed frame- work also covers typical features of parallel or concurrency theory such as parallel, indenpendant or conflicting computations. In other words, timed domains and timed morphisms provide a fully featured mathematical framework for the study of computable spatio-temporal functions.
 Plus d'infos  


2017-10-10The complexity of graph query languages
11:00-12:00
178
A graph database is a directed graph where each edge is additionally labeled with a symbol from a finite alphabet. Several data models, such as the ones occurring in the Semantic Web or semi-structured data, can be naturally captured via graph databases. In this context, one is not only interested in traditional queries, such as conjunctive queries, but also in navigational queries that take the topology of the data into account.

In this talk, we consider one of the most prominent navigational query languages, namely, the class of conjunctive regular path queries (CRPQs). This class extends the class of conjunctive queries with the ability of checking the existence of a path between two nodes, whose label matches a given regular expression. As in the case of conjunctive queries, evaluating CRPQs is an NP-complete problem. We present some results about tractable restrictions of CRPQs, as well as several open problems.
 Plus d'infos  


2017-10-03Proof complexity of constraint satisfaction problems
11:00-12:00
178
Many natural computational problems, such as satisfiability and systems of equations, can be expressed in a unified way as constraint satisfaction problems (CSPs). In this talk I will show that the usual reductions preserving the complexity of the constraint satisfaction problem preserve also its proof complexity. As an application, I will present two gap theorems, which say that CSPs that admit small size refutations in some classical proof systems are exactly the constraint satisfaction problems which can be solved by Datalog.

This is joint work with Albert Atserias.
 Plus d'infos  


2017-09-26Which classes of origin graph are generated by transducers?
11:00-12:00
178
This talk is about transductions, which are binary relations on words. We are interested in various models computing transductions (ie, transducers), namely two-way automata with outputs, streaming string transducers and string-to-string MSO transductions. We observe that each of these formalisms provides more than just a set of pairs of words. Indeed, one can also reconstruct origin information, which says how positions of the output string originate from positions of the input string. On the other hand, it is also possible to provide any pair of words in a relation with an origin mapping, indicating an origin input position for each output position, in a similar way. This defines a general object called origin graph. We first show that the origin semantic is natural and corresponds to the intuition we have of the run of a transducer, and is stable from translation from one model to another. We then characterise the families of origin graphs which corresponds to the semantics of streaming string transducers.
This is joint work with Mikolaj Bojanczyk, Laure Daviaud and Bruno Guillon, and has been published to ICALP17.
 Plus d'infos  


2017-07-04SAT-based Bounded Model Checking for 3-Valued Abstractions - Part II
11:00-12:00
178
Continuation of his precedent talk.
 Plus d'infos  


2017-06-27SAT-based Bounded Model Checking for 3-Valued Abstractions
11:00-12:00
178
In this talk I will present joint work with Nils Timm (and students) from the University of Pretoria on how to make model-checking of concurrent systems more effective and more efficient. In the first part of the talk, which is based on our SBMF'16 paper, I show how bounded model-checking over a three-valued truth domain {T:true, F:false, U:unknown} can be translated into a classical Boolean satisfiability problem which can then be given to any classical SAT solver. In the second part of the talk, which is based on our recent FSEN'17 paper, I speak about efficiency-increasing heuristics which are based on the availability of structural knowledge about the original system to be model-checked. On the basis of such structural knowledge the SAT solver can be guided into 'promising' search paths, whereby the probability of unnecessarily exploring fruitless paths is considerably diminished. The SBMF'16 paper was acknowledged as the "2nd-best paper of the conference", and the FSEN'17 paper was nominated among the "top three papers of the conference".
 Plus d'infos  


2017-06-13Axiomatizations for downward XPath on Data Trees
11:00-12:00
178
We give sound and complete axiomatizations for XPath with data tests by "equality" or "inequality", and containing the single "child" axis. This data-aware logic predicts over data trees, which are tree-like structures whose every node contains a label from a finite alphabet and a data value from an infinite domain. The language allows us to compare data values of two nodes but cannot access the data values themselves (i.e., there is no comparison by constants).

Our axioms are in the style of equational logic, extending the axiomatization of data-oblivious XPath, by B. ten Cate, T. Litak and M. Marx. We axiomatize the full logic with tests by "equality" and "inequality", and also a simpler fragment with "equality" tests only. Our axiomatizations apply both to node expressions and path expressions. The proof of completeness relies on a novel normal form theorem for XPath with data tests.
 Plus d'infos  


2017-05-30An efficient algorithm to decide the periodicity of b-recognisable sets using MSDF convention
11:00-12:00
178
Given an integer base b>1, a set of integers is represented in base b by a language over {0,1,...,b-1}. The set is said b-recognisable if its representation is a regular language. It is known that eventually periodic sets are b-recognisable in every base b, and Cobham's theorem imply the converse: no other set is b-recognisable in every base b.

We are interested in deciding whether a b-recognisable set of integers (given as a finite automaton) is eventually periodic. Honkala showed in 1986 that this problem is decidable and recent developments give efficient decision algorithms. However, they only work when the integers are written with the least significant digit first.

In this work, we consider here the natural order of digits (Most Significant Digit First) and give a quasi-linear algorithm to solve the problem in this case.
 Plus d'infos  


2017-05-23A linear lower bound for incrementing a space-optimal integer representation in the bit-probe model
11:00-12:00
178
We present the first linear lower bound for the number of bits required to be accessed in the worst case to increment an integer in an arbitrary space-optimal binary representation. The best previously known lower bound was logarithmic. It is known that a logarithmic number of read bits in the worst case is enough to increment some of the integer representations that use one bit of redundancy, therefore we show an exponential gap between space-optimal and redundant counters.

Our proof is based on considering the increment procedure for a space optimal counter as a permutation and calculating its parity. For every space optimal counter, the permutation must be odd, and implementing an odd permutation requires reading at least half the bits in the worst case. The combination of these two observations explains why the worst-case space-optimal problem is substantially different from both average-case approach with constant expected number of reads and almost space optimal representations with logarithmic number of reads in the worst case.

https://arxiv.org/abs/1607.00242 ; ICALP 2017
 Plus d'infos  


2017-05-16Proving safety of concurrent programs
11:00-12:00
178
This talk will be based on the paper from POPL 2017:

Thread Modularity at Many Levels: a pearl of compositional verification
by
Jochen Hoenicke, Rupak Majumdar, and Andreas Podelski

In the paper the authors consider the problem of proving safety of (parametrized) concurrent programs. They do not propose new techniques but rather revisit some existing ones. I have found putting these techniques next to each other very interesting and thought provoking. Since the considered problem is a fundamental problem for verification, I think it is worth to see this work at the seminar.

This will not be a survey talk. Technically the talk will be very easy, as the results are straightforward. The goal is to present a view point on the problem that I have got from reading the paper.
 Plus d'infos  


2017-05-09WBTS: the new class of WSTS without WQO.
11:00-12:00
76
We present the ideal framework [FG09a,BFM14] which was recently used to obtain new deep results on Petri nets and extensions. If time, we will present the proof of the famous but unknown Erdös-Tarski theorem. We argue that the theory of ideals prompts a renewal of the theory of WSTS by providing a way to define a new class of monotonic systems, the so-called Well Behaved Transition Systems, which properly contains WSTS, and for which coverability is still decidable by a forward algorithm.
 Plus d'infos  


2017-04-25On Reversible Transducers
11:00-12:00
178
Deterministic two-way transducers define the robust class of regular functions which is, among other good properties, closed under composition.
However, the best known algorithms for composing two-way transducers cause a double exponential blow-up in the size of the inputs.
We introduce a class of transducers for which the composition has polynomial complexity. It is the class of reversible transducers, for which the computation steps can be reversed deterministically.
While in the one-way setting this class is not very expressive, any two-way transducer can be made reversible through a single exponential blow-up.
As a consequence, the composition of two-way transducers can be done with a single exponential blow-up in the number of states.

A uniformization of a relation is a function with the same domain and which is included in the original relation.
Our main result actually states that we can uniformize any non-deterministic two-way transducer by a reversible transducer with a single exponential blow-up, improving the known result by de Souza which has a quadruple exponential complexity.
As a side result, our construction also gives a quadratic transformation from copyless streaming string transducers to two-way transducers, improving the exponential previous bound.
 Plus d'infos  


2017-04-04Automata theory and game semantics of higher-order computation
11:00-12:00
178
I will give a survey of various classes of automata that have
been used to capture the game semantics of higher-order programs
and, consequently, obtain decidability results for contextual equivalence.
 Plus d'infos  


2017-03-28Time domain (for time denotational semantics)
11:00-12:00
178
Directed complete partial orders (cpos) are used in denotational semantics for describing the way each value is incrementally computed, passing from a completely unknown value to a completely known value. Then, continuous functions between cpos propagate increase of knowledge on their inputs to increase of knowledge on their outputs.
In this talk, we define the notion timed cpo by means of a cut function that tells what part of any value is known before any given instant. In the induced partial order, the increase of knowledge explicitly refers to the passage of time. It follows that continuous functions between timed cpos provide denotational semantics model candidates for timed IO-system acting over (higher-order) time evolving values, e.g. timed streams, but also bounded below values, partial inductive structures, timed functions, etc.
Definitions, examples and (closure) properties of these timed cpos and their continuous functions are provided throughout.
 Plus d'infos  


2017-03-21Learning probability measures
11:00-12:00
178
Suppose we have a probabilistic algorithm given as a black box and we have access to an output of this algorithm. There are two - related - questions one could ask. (1) Is it possible to make a plausible guess as to which algorithm is in the box? (2) Can we use the output of this algorithm as a random number generator by extracting `pure’ randomness from it? We will look at these questions from the point of view of computability and algorithmic learning theory. [Based on joint work with S. Figueira, B. Monin, and A. Shen]
 Plus d'infos  


2017-03-14On the decomposition of finite-valued streaming string transducers
11:00-12:00
178
I will present some preliminary results towards a proof of a decomposition theorem for streaming string transducers (SSTs). Roughly, the conjectured decomposition theorem states that every SST that associates at most k outputs to each input can be effectively decomposed as a finite union of functional SSTs. Such a result would imply, among other things, the decidability of the equivalence problem for the considered class of transducers as well as a correspondence with the classical two-way transducers. I will present a proof of this decomposition theorem in the special case of SSTs with 1 register. The proof heavily relies on a combinatorial result by Kortelainen concerning word equations with iterated factors.
 Plus d'infos  


2017-03-07Verifying properties of functional programs: from the deterministic to the probabilistic case
11:00-12:00
178
In functional programs, also called higher-order programs, functions may take functions themselves as arguments. As a result, their model-checking relies in most approaches on semantic or type-theoretic tools. In this talk, I will explain how an analysis based on linear logic of a model-checking result of 2009 by Kobayashi and Ong led Melliès and I to the construction of a model for model-checking. This model is such that, when interpreting a term with recursion representing the tree of traces of a functional program, its denotation determines whether it satisfies a MSO property of interest. A related and similar model was obtained independently by Salvati and Walukiewicz.

In the second part of the talk, I will discuss the verification of termination for functional programs with recursion and probabilistic choice. Dal Lago and I defined recently a type system which is such that typable programs terminate with probability 1. In other terms, their set of diverging executions is negligible. If time allows, I will sketch ideas towards an extension of the model-checking results of the deterministic case to quantitative logics and functional programs with recursion.
 Plus d'infos  


2017-02-28Digital Currencies
11:00-12:00
178
Electronic money is a quite old problem in cryptology (Chaum, 1982) but recent discoveries lead to the birth of a new type of digital currency such as Bitcoins or Ethereum. Most of the new crypto-currencies are based on the concept of Blockchain which is used to maintain a trusted consensus in a distributed manner thanks to cryptographic primitives.

This talk will summarize the main concepts and mechanisms used to ensure the security of Bitcoins and Blockchain.
 Plus d'infos  


2017-02-14Emptiness of nonzero automata is decidable
11:00-12:00
178
Zero automata are a probabilistic extension of parity automata on infinite trees.
Bojanczyk has shown recently that the satisfiability of a certain probabilistic variant of MSO, called TMSO+zero reduces to the emptiness problem for zero automata.

These automata perform random walks on the input (binary) tree: when the automaton is in a state q on a node labelled with a, it selects non-deterministically a transition (q,a,r_0,r_1) and moves with equal probability 1/2 either to the left node in state r_0 or to the right node in state r_1..

The acceptance condition of zero automata impose conditions not only on the parity of individual branches of the run but as well on some other properties of runs that should occur almost-surely or with positive probability.

We introduce a variant of zero automata called nonzero automata and we show that i) for every zero automaton there is an equivalent nonzero automaton of quadratic size ii) the emptiness problem of nonzero automata is decidable, with complexity {sc np}. These results imply that TMSO+zero has decidable satisfiability.

Joint work with Mikolaj Danger Bojanczyk and Edon Kelmendi
 Plus d'infos  


2017-01-24Faster algorithms for program analysis
11:00-12:00
178
The talk is based on joint work with Krishnendu Chatterjee, Amir Kafshdar Goharshady, Prateesh Goyal, and Andreas Pavlogiannis.

The talk is about solving graph problems (focusing on graph problems that are often reduced to in program analysis) faster when the graphs are composed of control flow graphs of methods in programs. Using that control flow graphs of methods typically have constant tree-width we consider when the program either (i) has a single method, (ii) has many methods, or (iii) concurrent threads, each on a single method. For cases (ii) and (iii), we consider the Algebraic Path Problem (APP), which is a very general problem, with many interesting special cases, such as (1) reachability and shortest path (with positive and negative weights), (2) the IDE/IDFS frameworks of program analysis and (3) most probable path. Since APP has already been optimally solved for single methods/constant tree-width graphs, up to factors of log^* n (n is the number of states), in (i), if time permits, we will consider other weighted graph problems that has been reduced to in program analysis (but which are not special cases of APP), specifically finding the cycle with the least mean of weights (the minimum mean-payoff problem) and for a given start node v, finding the minimum number c and a path from v where all prefix sums of the weights of the path are greater than -c (the minimum initial credit problem). In all cases, we give simple algorithms which are faster than the state-of-the-art in theory and practice.

The talk is based on my POPL papers from 2015 and 2016, and, if time permits, my CAV paper from 2015 (see e.g. my homepage at http://rasmus.ibsen-jensen.com for the papers). No prior specialised knowledge is necessary to follow the talk.
 Plus d'infos  


2017-01-10Why liveness for timed automata is hard, and what we can do about it
11:00-12:00
178
The liveness problem for timed automata asks if a given automaton has an infinite run visiting an accepting state infinitely often. In this talk, we will show that if P is not equal to NP, the liveness problem is "more difficult" than the reachability problem - more precisely, we will exhibit a family of automata for which reachability is in P whereas liveness is NP-hard. We will then present a new algorithm to solve the liveness problem, and compare it with existing solutions.

Joint work with F. Herbreteau, T.T. Tran and I. Walukiewicz.
 Plus d'infos  


2016-12-13Sound negotiations and static analysis
11:00-12:00
178
Negotiations are a graphical formalism for describing multiparty distributed cooperation, proposed by Desel and Esparza. Alternatively, they can be seen as a model of concurrency with synchronized choice as communication primitive. Well-designed negotiations must be sound, meaning that, whatever its current state, the negotiation can still be completed.

In a former paper, Esparza and Desel have shown that deciding soundness of arbitrary negotiations is PSPACE-complete, and in PTIME for deterministic negotiations. They also considered an intermediate subclass of non-deterministic negotiations, but left the complexity of the soundness problem open.

We first consider the soundness problem beyond deterministic negotiations: we show that soundness of acyclic, weakly non-deterministic negotiations is in PTIME, and that checking soundness is already NP-complete for slightly more general classes.
Then we show how to use our algorithmic results to provide polynomial algorithms for some analysis problems of workflow nets with data.

Joint work with J. Esparza, D. Kuperberg and I. Walukiewicz
 Plus d'infos  


2016-12-01Translating LTL to Probabilistic Automata
11:00-12:00
76
Starting with the seminal work of Sistla, Vardi, and Wolper (1985),
there has been a lot of interest in discovering efficient translations
of Linear Temporal Logic (LTL) formulae into small automata. The
reason for this is that logic to automata translations directly impact
the complexity of runtime monitoring, verification, and synthesis of
systems. While much of the work has focused on translations from LTL
to nondeterministic and deterministic automata, in this talk we will
present new constructions of probabilistic automata for LTL. We will
discuss the consequences of this translation to the asymptotic
complexity of problems in monitoring and verification of stochastic
systems.

Joint work with Dileep Kini
 Plus d'infos  


2016-11-29Deciding semantic finiteness of first-order grammars w.r.t. bisimulation equivalence
11:00-12:00
178
The plan is to explain the main ideas of the MFCS'16 paper http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=6464,
by figures (and without formalities).
The presented decidability proof for semantic finiteness (or "regularity") of first-order grammars (that encompass pushdown automata)
w.r.t. bisimulation equivalence relies on the decidability of bisimulation equivalence (which was first proven by Senizergues).
 Plus d'infos  


2016-11-22Subword Based Abstractions of Formal Languages
11:00-12:00
178
A successful idea in the area of verification is to consider finite-state abstractions of infinite-state systems.  A prominent example is the fact that many language classes satisfy a Parikh's theorem, i.e. for each language, there exists a finite automaton that accepts the same language up to the order of letters. Hence, provided that the abstraction preserves pertinent properties, this allows us to work with finite-state systems, which are much easier to handle.

While Parikh-style abstractions have been studied very intensely over the last decades, recent years have seen an increasing interest in abstractions based on the subword ordering. Examples include the set of (non necessarily contiguous) subwords of members of a language (the downward closure), or their superwords (the upward closure).  Whereas it is well-known that these closures are regular for any language, it is often not obvious how to compute them.  Another type of subword based abstractions are piecewise testable separators.  Here, a separators acts as an abstraction of a pair of languages.

This talk will present approaches to computing closures, deciding separability by piecewise testable languages, and a (perhaps surprising) connection between these problems. If time permits, complexity issues will be discussed as well.
 Plus d'infos  


2016-11-15Systems with Parametric Thread Creation
11:00-12:00
178
We consider multi-threaded systems which combine recursion, or even higher-order recursion, with dynamic thread creation. Communication between threads is via global variables as well as via local variables that are shared between a thread and its sub-threads. Reading and writing are atomic operations, while we do not allow locks or operations of the type compare-and-set. The resulting systems are still too expressive to be decidable. As an abstraction, we therefore replace thread creation with parametric thread creation and show for the resulting systems, that the reachability problem is decidable.

This is joint work with Anca Muscholl and Helmut Seidl.
 Plus d'infos  


2016-11-08Parameterized verification of networks of many identical processes
11:00-12:00
178
I'll give an overview of my pd thesis result on parameterized verification of networks composed of many identical processes for which the number of processes is the parameter.
I'll present the decidability of the parameterized reachability problem in selective networks, where the messages only reach a subset of the components. This result is obtained thanks to a reduction to a new model of distributed two-player games for which we prove decidability in coNP of the game problem. Finally, I will present local strategies that enforce all processes to resolve the non-determinism only according to their own local knowledge. Under this assumption of local strategy, we were able to show that the parameterized reachability and synchronization problems are NP-complete.
 Plus d'infos  


2016-10-25Semantics models for timed programing languages
11:00-12:00
178
In this talk, I consider temporally causal functions of timed streams, i.e. functions that produce output values at a given instant that only depends on the input values that have been received till that instant.
Defining partial timed streams that form a directed complete partial order (DCPO), I will show how causal functions are nicely captured as limits of continuous and synchronous functions over these DCPO offering thus a denotational model of causal timed functions. Relaxing synchronous hypothesis to pre-synchronous hypothesis, I will show how every causal function admits a lattice of possible denotations such that:
- the least element can be understood as the latest semantics of that function: output values are computed when they need to be outputted,
- the greatest element can be understood as a the earliest semantics of that function: output values are computed as soon as all the input values they depend have been received.
- other elements in between can be understood as the various possible computation schedules that can still be followed in order to run the causal function.
The categorical properties of these continuous functions will then be detailed, offering various relevant operators for programing with these functions.
Last, I will show that a notion of causal function residual is available so that a minimal (possibly continuous) IO-automaton can be associated to every causal functions, providing thus a clear operation (latest) semantics. Open perspectives or questions will conclude this presentation.
 Plus d'infos  


2016-10-18Humanoid robotics and motion abstractions
11:00-12:00
178
Humans typically do not realize how much intelligence is required to perform usual motions.
One of the reasons why we are so good at motion control seems to be that we can abstract continuous inputs and outputs and their relationships with great flexibility, and perhaps reason almost symbolically on these abstractions.
This observation leads to the temptation to tackle humanoid robot motion problems with discrete abstractions and formal methods.
 Plus d'infos  


2016-10-11Walking the Boundary Between Tractability and Intractability
11:00-12:00
178
I will give an overview of some of my past and expected future research. I will focus on complexity classification theorems — which classify (or attempt to classify) all problems in some problem family of interest — and their interactions with other areas of theoretical computer science. In particular, I will discuss work on the template-restricted constraint satisfaction problem and variants thereof; and, work on model checking first-order logic with respect to different classes of sentences.
 Plus d'infos  


2016-10-04Evaluations de requêtes au moyen d'automates programmés (Query evaluations by fly-automata)
11:00-12:00
178
Les formules de la logique du second-ordre monadique définissent des ensembles de p-uplets d'ensembles
sur lesquels on peut faire du comptage et des recherches de cardinalité.
On considère dans cet exposé des combinaisons de comptages et de cardinalités.
On utilise pour cela deux types de déterminisation des automates.

Exposé en français. Les transparents sont en anglais.
 Plus d'infos  


2016-07-12Non commutative booléen algebras
11:00-12:00
76
I shall explain what the title of the talk means and hint at connections with multiple valued logic.
 Plus d'infos  


2016-07-05Double-exponential and triple-exponential bounds for choosability problems parameterized by treewidth
11:00-12:00
178
Choosability, introduced by Erdos, Rubin, and Taylor [Congr. Number. 1979], is a well-studied concept in graph theory: we say that a graph is $c$-choosable if for any assignment of a list of $c$ colors to each vertex, there is a proper coloring where each vertex uses a color from its list.

We study the complexity of deciding choosability on graphs of bounded treewidth. It follows from earlier work that 3-choosability can be decided in time $2^{2^{O(w)}}·n^{O(1)}$ on graphs of treewidth $w$. We complement this result by a matching lower bound giving evidence that double-exponential dependence on treewidth may be necessary for the problem: we show that an algorithm with running time $2^{2^{o(w)}}·n^{O(1)}$ would violate the Exponential-Time Hypothesis (ETH).

We consider also the optimization problem where the task is to delete the minimum number of vertices to make the graph 4-choosable and demonstrate that dependence on treewidth becomes triple-exponential for this problem: it can be solved in time $2^{2^{2^{O(w)}}}·n^{O(1)}$ on graphs of treewidth $w$, but an algorithm with running time $2^{2^{2^{o(w)}}}·n^{O(1)}$ would violate ETH.

The significance of the results is that these problems are apparently the first fairly natural graph-theoretic problems that require double-exponential or triple-exponential dependence on treewidth.

Joint work with Dániel Marx.
 Plus d'infos  


2016-06-28Nesting Depth of Operators in Graph DatabaseQueries: Expressiveness vs. Evaluation Complexity
11:00-12:00
178
Expressiveness and efficient algorithms for query evaluation are conflicting goals while designing languages for querying graph structured data. To better handle dynamically changing data, recent work has been done on designing query languages that can compare values stored in the graph database, without hard coding the values in the query. The main idea is to allow variables in the query and bind the variables to values when evaluating the query. For query languages that bind variables only once, query evaluation is usually NP-complete. There are query languages that allow binding inside the scope of Kleene star operators, which can themselves be in the scope of bindings and so on. Uncontrolled nesting of binding and iteration within one another results in query evaluation being PSPACE-complete. In this talk, we present a way to syntactically control the nesting depth of iterated bindings, and study how this affects the expressiveness and complexity of query evaluation.

This is joint work with B. Sreevathsan.

**Séminaire en salle 178**
 Plus d'infos  


2016-06-07Data Communicating Processes with Unreliable Channels
11:00-12:00
salle 178
We extend the classical model of lossy channel systems by considering systems that operate on a finite set of variables ranging over an infinite data domain. Furthermore, each message inside a channel is equipped with a data item representing its value. Although we restrict the model by allowing the variables to be only tested for (dis-)equality, we show that the state reachability problem is undecidable. In light of this negative result, we consider bounded-phase reachability, where the processes are restricted to performing either send or receive operations during each phase. We show decidability of state reachability in this case by computing a symbolic encoding of the set of system configurations that are reachable from a given configuration.

This a joint work with Parosh Abdulla and Mohammed Faouzi Atig.
 Plus d'infos  


2016-05-31The Complexity of All-switches Strategy Improvement
11:00-12:00
76
We study all-switches strategy improvement algorithms for parity, mean-payoff, discounted-payoff, and simple stochastic games. While these algorithms are now known to take exponential time in the worst case, we follow a recent line of work on the simplex method, and study them from a computational complexity point of view. We show that it is PSPACE-complete to decide the following problems: (1) given an edge e, will all-switches strategy improvement ever switch e? (2) given an edge e, is e in the optimal strategy found by all-switches strategy improvement?
 Plus d'infos  


2016-05-18Regular Abstractions of One Counter Languages
11:00-12:00
salle 75
We study the complexity of the following problems:
Given a one counter automaton A
1) construct an NFA that accepts the upward closure of the language of A (w.r.t. subword ordering)
2) construct an NFA that accepts the downward closure of the language of A
3) construct an NFA that accepts a language whose Parikh-image is the Parikh-image of the language of A.

Joint work with M.F. Atig (Uppsala), D. Chistikov (Oxford), P. Hofman (Cachan), P. Saivasan (Kaiserlautern) and G. Zetzsche (Cachan).
 Plus d'infos  


2016-05-10Deciding Maxmin Reachability in Half-Blind Stochastic Games
11:00-12:00
76
Two-player, turn-based, stochastic games with reachability conditions are considered, where the maximizer has no information (he is blind) and is restricted to deterministic startegies whereas the minimizer is perfectly informed. We ask the question of whether the game has maxmin 1 in other words we ask whether for all epsilon>0 there exists a deterministic strategy for the (blind) maximizer such that against all the strategies of the minimizer, it is possible to reach the set of final states with probability larger than 1-epsilon. This problem is undecidable in general, but we define a class of games, called leaktight half-blind games where the problem becomes decidable. We also show that mixed strategies in general are stronger for both players and that optimal strategies for the minimizer might require infinite-memory.
 Plus d'infos  


2016-05-03Semantic acyclicity of conjunctive queries
11:00-12:00
76
The evaluation problem for Conjunctive Queries (CQ) is known to be NP-complete in combined complexity and W[1]-complete in parameterized complexity. However, acyclic CQs and more generally CQs of bounded tree-width can be evaluated in polynomial time in combined complexity and they are fixed-parameter tractable.

We study the problem of whether a CQ can be rewritten into an equivalent CQ of bounded tree-width, in the presence of unary functional dependencies. We show that this problem is decidable in doubly exponential time, or in exponential time for a restricted class of queries. When it exists, the algorithm also yields a witness query.

This is a work that will appear in LICS this summer.
 Plus d'infos  


2016-04-19Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete
11:00-12:00
76
Blondin et al. showed at LICS 2015 that two-dimensional vector addition systems with states have reachability witnesses of length exponential in the number of states and polynomial in the norm of vectors. The resulting guess-and-verify algorithm is optimal (PSPACE), but only if the input vectors are given in binary. We answer positively the main question left open by their work, namely establish that reachability witnesses of pseudo-polynomial length always exist. Hence, when the input vectors are given in unary, the improved guess-and-verify algorithm requires only logarithmic space.

Joint work with Matthias Englert and Patrick Totzke, available from: http://arxiv.org/abs/1602.00477
 Plus d'infos  


2016-04-14The Logic of Counting Query Answers: A Study via Existential Positive Queries
11:00-12:00
Salle 76
We consider the computational complexity of the problem of counting the number of answers to a logical formula on a finite structure.

We present two contributions.

First, in the setting of parameterized complexity, we present a classification theorem on classes of existential positive queries. In particular, we prove that (relative to the problem at hand) any class of existential positive formulas is interreducible with a class of primitive positive formulas. In the setting of bounded arity, this allows us to derive a trichotomy theorem indicating the complexity of any class of existential positive formulas, as we previously proved a trichotomy theorem on classes of primitive positive formulas. This new trichotomy theorem generalizes and unifies a number of existing classification results in the literature, including classifications on model checking primitive positive formulas, model checking existential positive formulas, and counting homomorphisms.

Our second contribution is to introduce and study an extension of first-order logic in which algorithms for the counting problem at hand can be naturally and conveniently expressed. In particular, we introduce a logic which we call #-logic where the evaluation of a so-called #-sentence on a structure yields an integer, as opposed to just a propositional value (true or false) as in usual first-order logic. We discuss the width of a formula as a natural complexity measure and show that this measure is meaningful in #-logic and that there is an algorithm that minimizes width in the "existential positive fragment" of #-logic.

This is joint work with Stefan Mengel (CNRS).
 Plus d'infos  


2016-04-12One Hierarchy Spawns Another: Graph Deconstructions and the Complexity Classification of Conjunctive Queries
11:00-12:00
76
We study the classical problem of conjunctive query evaluation, here restricted according to the set of permissible queries. In this work, this problem is formulated as the relational homomorphism problem over a set of structures A, wherein each instance must be a pair of structures such that the first structure is an element of A. This problem generalizes the graph homomorphism problem of deciding, given a pair of graphs, whether or not there is a homomorphism from the first to the second.

We present a comprehensive complexity classification of these problems, which strongly links graph-theoretic properties of A to the complexity of the corresponding homomorphism problem.

- In particular, we define a binary relation on graph classes and completely describe the resulting hierarchy given by this relation; this description involves defining a new graph-theoretic measure called stack depth which may be of independent interest.
The binary relation is defined in terms of a notion which we call graph deconstruction and which is a variant of the well-known notion of tree decomposition. The hierarchy that results is reminiscent of that identified by Blumensath and Courcelle (LMCS 2010).

- We then use this graph hierarchy to infer a complexity hierarchy of homomorphism problems which is comprehensive up to a computationally very weak notion of reduction, namely, a parameterized form of quantifier-free reductions. We obtain a significantly refined complexity classification of left-hand side restricted homomorphism problems, as well as a unifying, modular, and conceptually clean treatment of existing complexity classifications, such as the classifications by Grohe-Schwentick-Segoufin (STOC 2001) and Grohe (FOCS 2003, JACM 2007).


In this talk, we will also briefly discuss parameterized complexity classes that we introduced/studied which capture some of the complexity degrees identified by our classification.

This talk is based on joint work with Moritz M"uller that appeared in PODS ’13 and CSL-LICS ’14.
 Plus d'infos  


2016-04-05Towards an algebraic theory of rational word functions
11:00-12:00
76
In formal language theory, several different models characterize regular languages, such as finite automata, congruences of finite index, or monadic second-order logic (MSO). Moreover, several fragments of MSO have effective characterizations based on algebraic properties. When we consider transducers instead of automata, such characterizations are much more challenging, because many of the properties of regular languages do not generalize to regular word functions. In this paper we consider word functions that are definable by one-way transducers (rational functions). We show that the canonical bimachine of Reutenauer and Schützenberger preserves certain algebraic properties of rational functions, similar to the case of word languages. In particular, we give an effective characterization of functions that can be defined by an aperiodic one-way transducer.
 Plus d'infos  


2016-03-29Programmation réactive par tuilage
11:00-12:00
76
Ou comment faire de la programmation événementielle, temps réel et concurrente,
sans évènements, sans produit concurrent et donc sans deadlock..

Travail en cours avec Simon Archipoff
 Plus d'infos  


2016-03-22For graphs of bounded tree width, recognisability equals definability in MSO.
14:15-16:00
75
We prove a conjecture of Bruno Courcelle, which states that a graph property is definable in MSO with modular counting predicates on graphs of constant treewidth if, and only if it is recognizable in the sense that constant-width tree decompositions of graphs satisfying the property can be recognized by tree automata. In our proof, we show that for every k there is an mso transduction which computes tree decompositions for graphs of tree-width at most k. One of the ingredients is the Factorisation Forest Theorem of Imre Simon.
 Plus d'infos  


2016-03-08The Complexity of Coverability in nu-Petri Nets
11:00-12:00
76
We show that the coverability problem in nu-Petri nets is complete for 'double Ackermann' time, thus closing an open complexity gap between an Ackermann lower bound and a hyper-Ackermann upper bound. The coverability problem captures the verification of safety properties in this nominal extension of Petri nets with name management and fresh name creation. Our completeness result establishes nu-Petri nets as a model of intermediate power among the formalisms of nets enriched with data, and relies on new algorithmic insights brought by the use of well-quasi-order ideals.

Joint work with Ranko Lazic, preprint available from https://hal.inria.fr/hal-01265302.
 Plus d'infos  


2016-03-01Reasoning about distributed systems: WYSIWYG
11:00-12:00
76
There are two schools of thought on reasoning about distributed systems: one following interleaving based semantics, and one following partial-order/graph based semantics. We will compare these two approaches and argues in favour of the latter. An introductory treatment of tree automata techniques (via split-width) to reason about distributed systems is also provided.
 Plus d'infos  


2016-02-16Sensing cost for automata and synthesis
11:00-12:00
76
I will present a complexity measure named sensing cost, designed for automata and transducters. It measures the average amount of information from the environment that must be read by the system at each time instant, in a random environment. It is then natural to look for minimally sensing automata for a given language, or minimally-sensing transducers as solutions of synthesis problems. I will present results along these lines, as well as open problems that remain to be tackled.

This is joint work with Shaull Almagor and Orna Kupferman.
 Plus d'infos  


2016-02-09A Generalised Twinning Property for Minimisation of Cost Register Automata.
11:00-12:00
76
Weighted automata extend finite-state automata by associating with transitions weights from a semiring S, defining functions from words to S. Recently, cost register automata have been introduced as an alternative model to describe any function realised by a weighted automaton by means of a deterministic machine.

Unambiguous weighted automata over a group G can equivalently be described by cost register automata whose registers take their values in G, and are updated by operations of the form x:=y.c, with c in G, and x,y registers.
This class is denoted by CRA(G).

In this talk, I will introduce a twinning property and a bounded variation property parametrised by an integer k, such that the corresponding notions introduced originally by Choffrut for finite-state transducers are obtained for k=1. Our main result links these notions with the register complexity of CRA(G).
More precisely, we prove that given an unambiguous weighted automaton W over an infinitary group G realizing some function f, the three following properties are equivalent:
i) W satisfies the twinning property of order k,
ii) f satisfies the k-bounded variation property,
iii) f can be described by a CRA(G) with at most k registers.

Actually, this result is proved in a more general setting, considering machines over the semiring of finite sets of elements from G and is extended to prove a similar result for finite-valued finite-state transducers.

Finally, the effectiveness of the constructions leads to decidability/complexity results about the register complexity (i.e. what is the minimal number of registers needed to compute a given function) of cost register automata.

This is a joint work with Pierre-Alain Reynier and Jean-Marc Talbot.
 Plus d'infos  


2016-02-02A Class of Zielonka Automata with a Decidable Controller Synthesis Problem
11:00-12:00
76
The decidability of the distributed version of the Ramadge and Wonham control problem, where both the plant and the controllers are modelled as Zielonka automata is a challenging open problem.

There exists three classes of plants for which the existence of a correct controller has been shown decidable in the distributed setting: when the dependency graph of actions is series-parallel, when the processes are connectedly communicating and when the dependency graph of processes is a tree.

We generalize these three results by showing that a larger class of plants, called broadcast plants, has a decidable controller synthesis problem. We give new examples of plants for which controller synthesis is decidable.
 Plus d'infos  


2016-01-12The language complexity of solutions of equations in free semigroups and free groups
11:00-12:00
76
We show that, given a word equation over a finitely generated free group (or semigroup), the set of all solutions in reduced words forms an EDT0L language. In particular, it is an indexed language in the sense of Aho. This is joint work with Murray Elder and Volker Diekert.
 Plus d'infos  




Liste des événements répétitifs du groupe Séminaire Méthodes Formelles




Retour
Retour à l'index