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

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.

7 février 2022

Mesure uniforme et modèle probabiliste pour des systèmes concurrents sous la sémantique d’ordres partiels

Samy Abbes (IRIF, Université de Paris)

Attention : SALLE MSE 018
(la salle du conseil est occupée).

Considérons un système concurrent à événements discrets. Ses exécutions sont naturellement données comme des ordres partiels, et non pas comme des chaînes d’événements. Du point de vue probabiliste, le lien avec les systèmes probabilistes classiques (chaînes de Markov, automates probabilistes par exemple) n’est pas immédiat. Il est pourtant nécessaire d’avoir une théorie probabiliste bien fondée si on s’intéresse à la génération aléatoire de trajectoires dans les systèmes concurrents, notamment dans un but de vérification probabiliste.

Ces motivations me poussent à étudier dans un premier temps la notion de mesure de Bernoulli pour les monoïdes de traces, dont un cas particulier est la mesure uniforme. Il s’agit de généraliser le “jeté de dés répété infiniment” au cadre d’un monoïde dont certaines lettres commutent, à la place d’un monoïde libre. Dans un deuxième temps, on étend cette notion au cadre de systèmes concurrents plus réalistes, tels que les réseaux de Petri. On montrera dans l’exposé le lien entre la combinatoire des monoïdes de traces, qui remonte aux travaux de Cartier et Foata (1969) et de Viennot (1986), et la construction récente de mesures de probabilités en collaboration avec J. Mairesse (2015).

24 janvier 2022

Compositionality for Herbrand witnesses

Aurore Alcolei (LACL)

Herbrand theorem is a cornerstone result for giving a computational meaning to first order classical formulas. The validity of a formula is equivalent to having a finite procedure able to choose witnesses to satisfy the formula in any model. Those witnesses are generally called Herbrand witnesses.

Hebrand witnesses can be extracted from proof sequents but unlike them they cannot be composed. This opens the way for investigations: what kind of missing ingredient should be added to the witnesses in order to make them composable? Can we avoid the sequent calculus bureaucracy while doing so?

In this talk I will propose a semantic answer to these questions: I will show how Herbrand witnesses can be viewed as term-strategies in an extended model of causal games, hence inheriting the composition procedure already embedded in this model.

13 décembre 2021

Addressing Machines for Higher-Order Computations

Giulio Manzonetto ( Laboratoire d'Informatique de Paris Nord (LIPN))

Turing machines and register machines have been used for
decades in theoretical computer science as abstract models of
computation. However, they are not well-suited for modelling
higher-order computations, because accessing the address of a machine
is not a built-in operation, hence functional machines cannot be
easily passed through their reference. We study a class of abstract
machines that we call “addressing machines” since they are only able
to manipulate memory addresses of other machines. The operations
performed by these machines are very elementary: load an address in a
register, apply a machine to another one via their addresses, and call
the address of another machine. We endow addressing machines with an
operational semantics based on leftmost reduction and study their
behaviour. We show that they can be used, for instance, to construct
models of the pure, untyped lambda-calculus. Subsequently, we extend
the syntax of their programs by adding instructions for executing
arithmetic operations on natural numbers, and introduce a reflection
principle allowing certain machines to access their own address and
perform recursive calls. We show that the resulting extended
addressing machines naturally model a weak call-by-name PCF with
explicit substitutions. Finally, we show that they are also well
suited for representing regular PCF programs (closed terms) computing
natural numbers.

6 décembre 2021

Avancées récentes sur les algèbres de Kleene concurrentes

Paul Brunet (LACL)

Les algèbres de Kleene concurrentes (CKA) fournissent un cadre algébrique pour raisonner sur les programmes concurrents. Au cours de ces dernières années, nous avons étudié différentes manières d’enrichir ce modèle afin de capturer une classe plus large de problèmes de vérification.

Dans cet exposé, je présenterai tout d’abord les bases de CKA, avec ses présentations axiomatiques et combinatoires, et les résultats de décidabilité correspondants. Je ferais ensuite un bref panorama de certaines extensions du modèle, en considérant des aspects tels que le flot de contrôle, la cohérence des accès mémoire, et l’exclusion mutuelle.

Ce travail est le fruit de collaborations avec Tobias Kappé, Jana Wagemaker, Simon Docherty, Fabio Zanasi, Jurriaan Rot, Alexandra Silva, David Pym, Damien Pous, et Georg Struth.

29 novembre 2021

Invariance pour l’ordre et logique à deux variables.

Julien Grange (LACL)

On s’intéressera au pouvoir d’expression d’une extension particulière de la logique du premier ordre portant sur deux variables (FO^2).

On enrichira nos structures d’un ordre linéaire sur leurs sommets, en s’imposant toutefois la limitation suivante: une formule peut s’appuyer sur cette relation d’ordre uniquement si son évaluation est indépendante de cet ordre.
Cette notion d’invariance pour l’ordre est très naturelle en complexité descriptive, et son application à FO^2 l’est d’autant plus que la propriété d’invariance est décidable dans ce contexte.

Il apparaît clairement que l’ajout de cet ordre invariant accroît le pouvoir d’expression de FO^2, en autorisant le comptage.

On proposera ici une borne supérieure à son pouvoir d’expression sur les classes de structures de degré borné.

22 novembre 2021

QCSP monsters and the future of the Chen Conjecture

Barnaby Martin (Durham University, Algorithms and Complexity Group (ACiD) )

We elaborate the complexity of the Quantified Constraint Satisfaction Problem, QCSP(A), where A is a finite idempotent algebra. Such a problem is either in NP or is co-NP-hard, and the borderline is given precisely according to whether A enjoys the polynomially-generated powers (PGP) property. This completes the complexity classification problem for QCSPs modulo that co-NP-hard cases might have complexity rising up to Pspace-complete. Our result requires infinite languages, but in this realm represents the proof of a slightly weaker form of a conjecture for QCSP complexity made by Hubie Chen in 2012. The result relies heavily on the algebraic dichotomy between PGP and exponentially-generated powers (EGP), proved by Dmitriy Zhuk in 2015, married carefully to previous work of Chen. Finally, we discuss some recent work with Zhuk in which the aforementioned Chen Conjecture is actually shown to be false. Indeed, the complexity landscape for QCSP(B), where B is a finite constraint language, is much richer than was previously thought.

15 novembre 2021

Pareto analysis and approximation in stochastic and timed systems

Mahsa Shirmohammadi (IRIF)

This is a survey talk on the Pareto and $\epsilon$-Gap Pareto analysis in Markov decision processes, stochastic games and weighted time automata.

The talk will lightly introduce the problems and the challenges one encounters while studying them in the stochastic and time systems; the talk will also pinpoint a couple of related open problems in the above-mentioned models.

8 novembre 2021

Conjunctive grammars, cellular automata and logic

Théo Grente (LACL)

Conjunctive grammars are an extension of context free grammars with a conjunction operation. Their expressive power (even on a unary alphabet) is largely unknown.

When restricting time, space or even communication, cellular automata (CA) can act as languages recognizer defining complexity classes.

The goal of this talk is to prove the inclusion of conjunctive languages in one of CA complexity classes.

The proof uses a programming method which relies on exact characterizations of interesting CA complexity classes by sub-logics of ESO (existential second-order logic) with Horn formulas as their first-order part. By using this method, we just have to define conjunctive grammars in our logic to obtain an inclusion result.

18 octobre 2021

Simulating Digital Computations with Analog Machines

Olivier Bournez (Lix)

We will compare the power of analog machines (such as the General Purpose Analog Computer), based for example on analog electronics, to the power of digital machines (such as Turing machines). This will involve a discussion on how one can compute with ordinary differential equations.