Invited Speakers

Jérôme Leroux (Bordeaux) Ideal Decompositions : Applications to Petri Net Extensions. Abstract. We present extensions of Petri nets that are well-structured and therefore allow generic decision procedures for several verification problems. By inspecting the data structures of classical algorithms for Petri nets, we show that they can be interpreted as ideals for well quasi ordered sets. This new interpretation of classical data structures paves the way to extend algorithms to various Petri net extensions. In this presentation we mainly focus on the framework of ideal decompositions for well-quasi-ordered sets with Petri nets extensions as running examples. Sylvain Schmitz (Cachan) On the Complexity of VAS Reachability. Abstract. The decidability of the reachability problem in vector addition systems is a landmark result in theoretical computer science, with applications in an array of fields ranging from program verification to data logics. I will present the main arguments of the first known complexity upper bound for this problem, obtained together with Leroux by analysing the decomposition algorithms invented by Mayr and successively refined by Kosaraju and Lambert.