On monday, at 2pm - UPEC CMC - Room P2-131

June 20, 2022

tba

Cüneyt Güzelis

tba

May 23, 2022

Geometric amortization of enumeration algorithms

Florent Capelli (INRIA Lille équipe LINKS)

Enumeration algorithms are algorithms whose goal is to
output the set of all solutions to a given problem. There exists
different measures for the quality of such algorithm, whose relevance
depends on what the user wants to do with the solutions set.

If the goal of the user is to explore a subset of solutions or to
transform the solutions as they are outputted with a stream-like
algorithm, a relevant measure of the complexity in this case is the
delay, that is, the maximal time between the output of two distinct
solutions. Following this line of thoughts, significant efforts have
been made by the community to design polynomial delay algorithms, that
is, algorithms whose delay between the output of two new solutions is
polynomial in the size of the input.

While this measure is interesting, it is not always completely
necessary to have a bound on the delay and it is enough to ask for a
guarantee that running the algorithm for O(t poly(n)) will produce at
least t solutions. While algorithms having this property can be
transformed into polynomial delay algorithm, the naive transformation
may result in a blow up in the space used by the enumerator.

In this talk, we will present a new technique that allow to transform
such algorithms into polynomial delay algorithm with only a polynomial
overhead on the space.

May 9, 2022

Fairness and promptness in Muller formulas

Léo Tible (LACL)

In this paper we consider two different views of the model checking problems for the Linear Temporal Logic (LTL).

  • On the one hand, we consider the universal model checking problem for LTL, where one asks that for a given system and a given formula that all the runs of the system satisfy the formula.
  • On the other hand, fair model checking problem for LTL asks that for a given system and a given formula almost-all the runs of the system satisfy the formula.

It was shown that these two problems have the same theoretical complexity i.e. PSPACE
complete. The question arises whether one can find a fragment of LTL for which the complexity of these two problems differ. One such fragment was identified in a previous work, namely the Muller fragment.

We address a similar comparison for the prompt fragment of LTL (pLTL). pLTL extends LTL
with an additional operator, i.e. the prompt-eventually. This operator ensures the existence of a bound such that liveness properties are satisfied within this bound.

We show that the corresponding Muller fragment for pLTL does not enjoy the same algorithmic
properties with respect to the comparison considered. We also identify a new expressive fragment for which the fair model checking is faster than the universal one.

April 11, 2022

Boltzmann sampling for fun and profit : Comment utiliser des séries formelles pour corriger des copies !

Benoit Barbot (LACL)

The long title : a modest proposal for preventing teacher to think too hard when evaluating student’s programmatic feast.

Therein the speaker, the honourable Benoît Barbot shall enlighten us on the theory and practice of Boltzmann sampling, before reporting on the masterful application in automated evaluation of student’s programming skills in functional programming.

The title is a reference to the excellent essay of Dr J. Swift.
https://en.wikipedia.org/wiki/A_Modest_Proposal

March 28, 2022

Progress report on hardness of approximate graph colouring

Jakub Opršal (Oxford)

As almost everybody knows, deciding whether a given graph is colourable using 3 colours is an NP-hard problem which means that finding a 3-colouring of a graph that is promised to be 3-colourable cannot be achieved in polynomial time, unless P = NP.

But how hard is to find a colouring of such a graph using 4, 5, 6, or more colours?

Surprisingly little is known to that account — it has only recently (in 2019) been shown that finding a 5-colouring of a given 3-colourable graph is NP-hard, while the best known polynomial algorithm, due to Kawarabayashi and Thorup, uses a little less than $O(n^{1/5})$ colours where $n$ is the number of vertices of the input graph.

We will present several recent advancements on this problem, and their relevance to a wider scope of promise constraint satisfaction.

The promise constraint satisfaction problem is a natural generalisation of both the above promise version of graph colouring and the constraint satisfaction problem (CSP). This generalised, promise variant gained a substantial attention in recent years due to generalisation of algebraic techniques behind the theory of CSP, that lead to the famous CSP dichotomy, to the promise setting.

March 21, 2022

Visibly pushdown languages in AC0

Nathan Grosshans (Universität Kassel)

One important research endeavour at the intersection of circuit complexity theory, algebraic automata theory and logic is the classification of regular languages according to their localisation within the internal structure of NC1, the class of languages decided by Boolean circuits of polynomial size, logarithmic depth and with gates of constant fan-in. In some sense, the search for such a classification concentrates most of the open questions we have about the relationship between NC1 and its well-studied subclasses.

While many questions are still open, one of the greatest successes of this research endeavour has been the characterisation of the regular languages in AC0, the subclass of NC1 corresponding to Boolean circuits of polynomial length, constant depth and with gates of unbounded fan-in. This characterisation takes the form of a triple languages-algebra-logic correspondence: a regular language is in AC0 if, and only if, its syntactic morphism is quasi-aperiodic if, and only if, it is definable in first-order logic over words with linear order and modular predicates.

It is natural to try to extend such results to classes of formal languages greater than the class of regular languages. A well studied and robust such class is given by visibly pushdown languages (VPLs): languages recognised by pushdown automata where the stack-height-behaviour only depends on the letters read from the input. Over the previous decade, a series of works concentrated on the fine complexity of VPLs, with several achievements: one of those was a characterisation of the class of visibly counter languages (basically VPLs recognised by visibly pushdown automata with only one stack symbol) in AC0 by Krebs, Lange and Ludwig. However, the characterisation of the VPLs in AC0 still remains open.

In this talk, I shall present a conjectural characterisation of the VPLs in AC0 obtained with Stefan Göller at the Universität Kassel. It is inspired by the conjectural characterisation given by Ludwig in his Ph.D. thesis as a generalisation of the characterisation for visibly counter languages, but that is actually false. In fact, we give a more precise general conjectural characterisation that builds upon recognisability by morphisms into Ext-algebras, an extension of recognisability by monoid-morphisms proposed by Czarnetzki, Krebs and Lange to suit the case of VPLs. This characterisation classifies the VPLs into three categories according to precise conditions on the Ext-algebra-morphisms that recognise them:

  • those that are TC0-hard;
  • those that are in AC0;
  • those that correspond to a well-identified class of “intermediate languages” that we believe to be neither in AC0 nor TC0-hard.

March 7, 2022

Counter games with boundedness winning conditions

Edwin Hamel (Université libre de Bruxelles)

Parity games are well-known infinite two-player games played on finitely colored graphs. We define an extension of parity games, called counter games, where each player can at every move, increment or reset a finite number of counters.

We examine several types of winning conditions that are linked to the boundedness of the counters of the game, and to parity conditions. For every type of winning conditions examined, we give algorithmic complexity results, and results on the size of the memory needed to win. For example, we show that deciding whether Eve can force one of the counters to be bounded can be done in polynomial time, and that, if Eve wins, then Eve has a memoryless winning strategy.

The results in this talk are joint work with Emmanuel Filiot.

February 14, 2022

On the strategy synthesis problem in MDPs: probabilistic CTL and rolling windows.

Damien Busatto-Gaston (Université libre de Bruxelles)

In this talk I will present ongoing work on Markov decision processes.

Given an MDP and a formula phi, the strategy synthesis problem asks if there exists a strategy for the MDP such that the resulting Markov chain satisfies phi.
This challenging problem is known to be undecidable for the probabilistic temporal logic PCTL.

We study a class of formulae that can be seen as a fragment of PCTL where a local, bounded horizon property is enforced globally. Moreover, we allow for linear expressions
in the probabilistic inequalities.

We show that this class of formulae is at the frontier of decidability, depending on the type of strategies considered. In particular, strategy synthesis becomes decidable when strategies are either deterministic or memoryless, while the general problem remains undecidable.

We compare with results on the entire PCTL logic and consider applications to the PCTL satisfiability problem.