# Parameterized Verification of Asynchronous Shared-Memory Systems

arXiv: https://arxiv.org/abs/1304.1185 · HTML: https://mlsanity.com/paper/1304.1185/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 3 Apr 2013.

## Built on by (most cited first, 1 of 1)

- [Safe Reinforcement Learning via Probabilistic Logic Shields](https://mlsanity.com/paper/2303.03226/) (2023)

## Abstract (arXiv)

We characterize the complexity of the safety verification problem for parameterized systems consisting of a leader process and arbitrarily many anonymous and identical contributors. Processes communicate through a shared, bounded-value register. While each operation on the register is atomic, there is no synchronization primitive to execute a sequence of operations atomically. We analyze the complexity of the safety verification problem when processes are modeled by finite-state machines, pushdown machines, and Turing machines. The problem is coNP-complete when all processes are finite-state machines, and is PSPACE-complete when they are pushdown machines. The complexity remains coNP-complete when each Turing machine is allowed boundedly many interactions with the register. Our proofs use combinatorial characterizations of computations in the model, and in case of pushdown-systems, some language-theoretic constructions of independent interest.