Les lundis, à partir de 14h - UPEC CMC - Salle P2-131

20 juin 2022

tba

Cüneyt Güzelis

tba

23 mai 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.

16 mai 2022

Absorbing patterns in BST-like expression-trees

Pablo Rotondo (LIGM)

Dans cet exposé, nous nous interrogeons sur l’effet de réductions sémantiques simples
sur des expressions produites par le modèle aléatoire des arbres de recherche binaire (dits BST-like).

Ces arbres unaire-binaire sont souvent utilisés dans les benchmarks des outils de vérification,
car leur distribution est très facile à implémenter. Dans un premier temps, nous introduisons ce que nous entendons par expressions,
et nous nous plaçons dans le cas où il y a un motif absorbant pour un opérateur donné,
qui permet de simplifier les expressions tout en préservant leur sémantique.

Nous étudions alors la taille moyenne après avoir simplifié au maximum une expression aléatoire de taille n.
Nous démontrons qu’il y a 5 régimes différents, selon deux “thresholds” pour la probabilité de l’opérateur absorbant,
allant du cas où il y a aucune simplification jusqu’à une réduction presque totale.

Travail en commun avec Florent Koechlin.

9 mai 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.

14 mars 2022

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

Yann Strozecki (UVSQ, laboratoire DAVID)

Les jeux stochastiques simples sont des jeux à deux joueurs, avec du hasard et à information parfaite. Deux joueurs déplacent à tour de rôle un jeton sur un graphe dans le but d’atteindre chacun un puits différent. L’objectif est de trouver le couple de stratégies optimales.

Trouver ce couple est relativement difficile : on ne connaît aucun algorithme polynomial ou quasi polynomial, contrairement aux jeux de parité, même si le problème n’est pas NP-complet (sous hypothèse de complexité).

Les algorithmes de résolution se rangent principalement dans trois catégories : programmation quadratique, propagation de valeur, et amélioration de stratégies.

On présente dans cet exposé un méta-algorithme qui généralise tous les algorithmes d’améliorations de stratégies connus. Cela nous permet de redémontrer facilement la correction de ces algorithmes, de supprimer certaines hypothèses ainsi que de donner de meilleures bornes de complexité.

7 mars 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.

14 février 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.