Reasoning about Dynamic Networks of Infinite-State Processes with Global Synchronization

We propose a generic framework for reasoning about dynamic networks of infinite state processes such as counter processes, timed processes, or pushdown processes, with complex synchronization mechanisms, including global synchronization (i.e., broadcast communication). We define models for such networks, called CTN, based on Petri nets with transfer operations. Tokens (representing occurrences of processes) have attached colors over infinite domains (representing data values, clocks, stacks, etc.). We also define a (second-order) logic called CTSL allowing to express constraints on locations of tokens in the nets and on their colors. We prove that the $\exists^* \forall^*$ fragment of CTSL is decidable whenever the underlying logic for expressing constraints on colors is decidable. Moreover, we show that the same fragment is closed under post and pre image computations. These results can be used in verification such as in invariance checking. We show that our framework can be applied for reasoning about multithreaded programs with procedure calls and dynamic creation of process with global synchronization, and on dynamic programs with real-time constraints