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完全，并提供了若干自然限制条件，使得该问题可在多项式时间内求解。