VASS (Vector Addition Systems with States), which are equivalent to Petri nets, are automata equipped with natural variables that can be decremented or incremented. VASS are a powerful model which has been intensively studied in the last decades. Many verification techniques have been developed to analyse them and the frontier between the decidable and undecidable problems related to VASS begins to be well known. One interesting point is that the model-checking of linear temporal logics (like LTL or linear mu-calculus) is decidable for this model but this is not anymore the case when considering branching time temporal logics. However some restrictions can be imposed on the logics and on the studied system in order to regain decidability. In this talk, we will present these results concerning the model-checking of VASS and the techniques leading to the decidability results. We will then show how these techniques and results can be used to analyse some extensions of VASS with probabilities, namely probabilistic VASS and VASS Markov Decision Processes.

The notion of rank of divisor on graph was introduced by Baker and Norine in 2007 in showing the link with the similar notion on Riemann surface. Moreover, the authors have developed a theorem for divisors on graph analogue to the classical Riemann-Roch theorem. Since then, many works have studied for computing the rank of divisors on graph. A very important is the new theorem on the NP-hardness complexity of the Problem of computing the rank of divisor on general graph. The proof of this result was based on the proof of the NP-hardness of the Problem of finding the minimum recurrent configurations of Chip Firing Game on directed graphs (by Perrot and Pham). In this talk, we will present some (linear) algorithms for computing the rank of divisors on some classes of graphs.

Soit G_n un graphe aléatoire uniforme à n sommets, choisi dans votre classe de graphes favorite (graphes planaires, graphes sans triangles,graphes 7-coloriables, etc…). Quelle est la probabilité que G_n soit connexe? Sans hypothèse sur la classe on ne peut, bien sûr, rien dire sur cette question. Mais si la classe de graphe est *ajoutable*, àsavoir stable par l'ajout d'arêtes entre composantes connexes, McDiarmid-Steger-Welsh (2005) ont conjecturé que P(G_n connexe) est au moins exp(-1/2)=0.60… asymptotiquement. Cette borne est optimale (car elle est atteinte pour la classe des forêts) et aussi assez étonnante (car de nombreuses classes sont ajoutables, y compris des classes très bizarres sur lesquelles on penserait ne rien pouvoir dire). Je parleraide notre démonstration de cette conjecture. Je commencerai par expliquer la très jolie et simple technique dedouble-comptage due à McSW et qui permet de démontrer la borne exp(-1). Puis j'essaierai de donner les idées principales de notre technique nouvelle, le «double-comptage local». Cette technique débouche sur un problème d'optimisation non convexe dont les fonctionnelles sont par miracle des séries génératrices d'arbres enracinés pondérés par des fonctionnelles supermultiplicatives. L'adaptation d'outils de combinatoire classique (le théorème de disymétrie!) permet de résoudre le problème. Travail commun avec Guillem Perarnau (Birmingham)

Sylvain Lombardy (LaBRI)– Démonstration du logiciel Vaucuson-R