On parametrized verification of asynchronous, shared-memory pushdown systems

We consider here parametrized asynchronous shared-memory pushdown systems, as introduced by Hague. In a series of recent papers it has been shown that reachability in this model is PSPACE-complete [Hague’11], [Esparza, Ganty, Majumdar’13] and that liveness is decidable in NEXPTIME [Durand-Gasselin, Esparza, Ganty, Majumdar’15]. We show that the liveness problem is PSPACE-complete. We also consider the universal reachability problem, and show that it is decidable, moreover coNEXPTIME-complete. These results imply that verification of regular properties of traces, satisfying some stuttering condition, is also decidable in NEXPTIME.

Authors

• joint work with Anca Muscholl
• Igor Walukiewicz

Keywords

No keywords are indexed for this paper.