TY - GEN
T1 - Parameterized verification of asynchronous shared-memory systems
AU - Esparza, Javier
AU - Ganty, Pierre
AU - Majumdar, Rupak
PY - 2013
Y1 - 2013
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84881191812&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-39799-8_8
DO - 10.1007/978-3-642-39799-8_8
M3 - Conference contribution
AN - SCOPUS:84881191812
SN - 9783642397981
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 124
EP - 140
BT - Computer Aided Verification - 25th International Conference, CAV 2013, Proceedings
T2 - 25th International Conference on Computer Aided Verification, CAV 2013
Y2 - 13 July 2013 through 19 July 2013
ER -