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

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.

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.

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.

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

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.

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.

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.

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.

La classes des fonctions régulières est une classe robuste définie de façon équivalente par les transducteurs bidirectionnels, les transductions MSO ou encore les Streaming String Transducers. Récemment, il a été proposé des combinateurs réguliers afin de définir des expressions régulières pouvant décrire cette classe.

Dans cet exposé, je présenterai la classe des transducteurs bidirectionnels ainsi que ces combinateurs réguliers, puis une extension de ce résultat à la sous-classe des fonctions apériodiques, étendant le célèbre résultat d’équivalence entre expressions sans-étoiles et automates apériodiques de Schützenberger.

Les résultats présentés ici proviennent de travaux récents en collaboration avec Paul Gastin (LSV, Université Paris-Saclay) et Shankara Narayanan Krishna (IIT Bombay) et sont disponible à cette adresse.