tba

### June 20, 2022

*tba*

**Cüneyt Güzelis**

Skip to content
# Seminars 2021-22

Contact : seminar@lacl.fr
# On monday, at 2pm - UPEC CMC - Room P2-131

### June 20, 2022

*tba*

**Cüneyt Güzelis**

### May 23, 2022

*Geometric amortization of enumeration algorithms*

**Florent Capelli**
(INRIA Lille équipe LINKS)

### May 16, 2022

*Absorbing patterns in BST-like expression-trees*

**Pablo Rotondo**
(LIGM)

### May 9, 2022

*Fairness and promptness in Muller formulas*

**Léo Tible**
(LACL)

### April 11, 2022

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

**Benoit Barbot**
(LACL)

### March 28, 2022

*Progress report on hardness of approximate graph colouring*

**Jakub Opršal**
(Oxford)

### March 21, 2022

*Visibly pushdown languages in AC*^{0}

**Nathan Grosshans**
(Universität Kassel)

### March 14, 2022

*Une méthode générique d’amélioration de stratégie pour les jeux stochastiques simples.*

**Yann Strozecki**
(UVSQ, laboratoire DAVID)

### March 7, 2022

*Counter games with boundedness winning conditions*

**Edwin Hamel**
(Université libre de Bruxelles)

### February 14, 2022

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

**Damien Busatto-Gaston**
(Université libre de Bruxelles)

tba

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.

TBA

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.

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

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.

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 NC^{1}, 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 NC^{1} 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 AC^{0}, the subclass of NC^{1} 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 AC^{0} 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 AC^{0} by Krebs, Lange and Ludwig. However, the characterisation of the VPLs in AC^{0} still remains open.

In this talk, I shall present a conjectural characterisation of the VPLs in AC^{0} 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 TC
^{0}-hard; - those that are in AC
^{0}; - those that correspond to a well-identified class of “intermediate languages” that we believe to be neither in AC
^{0}nor TC^{0}-hard.

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.

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.