Paper Info
Title
Parameterized verification of asynchronous shared-memory systems
Abstract
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.
Year
DOI
Venue
2013
10.1145/2842603
Journal of the ACM (JACM)
Keywords
DocType
Volume
parameterized verification,language-theoretic construction,turing machine,leader process,asynchronous shared-memory system,independent interest,finite-state machine,identical contributor,bounded-value register,safety verification problem,pushdown machine,combinatorial characterization
Conference
63
Issue
ISSN
Citations 
1
0004-5411
15
PageRank 
References 
Authors
0.62
27
3
Name
Order
Citations
PageRank
Javier Esparza177060.33
Pierre Ganty224220.29
Rupak Majumdar33401220.08