We consider the verification of distributed systems composed of an arbitrary number of asynchronous processes. Processes are identical finite-state machines that communicate by reading from and writing to a shared memory. Beyond the standard model with finitely many registers, we tackle round-based shared-memory systems with fresh registers at each round. In the latter model, both the number of processes and the number of registers are unbounded, making verification particularly challenging. The properties studied are generic presence reachability objectives, which subsume classical questions such as safety or synchronization by expressing the presence or absence of processes in some states. In the more general round-based setting, we establish that the parameterized verification of presence reachability properties is PSPACE-complete. Moreover, for the roundless model with finitely many registers, we prove that the complexity drops down to NP-complete and we provide several natural restrictions that make the problem solvable in polynomial time.

翻译：我们考虑由任意数量异步进程组成的分布式系统的验证问题。这些进程是相同的有限状态机，通过读写共享内存进行通信。除了具有有限数量寄存器的标准模型外，我们还研究了每轮使用新寄存器的轮次式共享内存系统。在后一种模型中，进程数量和寄存器数量均无界，这使验证变得尤为困难。所研究的属性是一般化的存在可达性目标，通过表达进程在某些状态中的存在或缺失，涵盖了诸如安全性或同步性等经典问题。在更通用的轮次式设定下，我们证明存在可达性属性的参数化验证是PSPACE完全的。此外，对于具有有限数量寄存器的非轮次模型，我们证明其复杂度降至NP完全，并提供了若干能使问题在多项式时间内可解的自然约束条件。