Ahmed Bouajjani (University of Paris 7), Reasoning about dynamic networks of counter systems

We introduce new models for multithreaded programs with dynamic creation of communicating processes, each of these processes being able to manipulate a finite number of (local) integer/real variables. These models are based on constrained multiset rewrite systems (Petri nets). We define a logic (an extension of Presburger arithmetics) allowing to specify and to reason about (potentially infinite) sets of configurations of such models. We investigate the decidability of the proposed logic and propose an expressive fragment which is decidable and close under post and pre image computations. We show the application of the proposed framework in the verification of parametrized/dynamic networks of processes with integer/real variables. This is a joint work with Yan Jurski and Mihaela Sighireanu.