On parametrized verification of asynchronous, shared-memory pushdown systems

2016/06/28 by Fortin, Marie, Muscholl, Anca, Walukiewicz, Igor
#FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.1606.08707

Abstract

We consider the model of parametrized asynchronous shared-memory pushdown systems, as introduced in [Hague'11]. In a series of recent papers it has been shown that reachability in this model is PSPACE-complete [Esparza, Ganty, Majumdar'13] and that liveness is decidable in NEXPTIME [Durand-Gasselin, Esparza, Ganty, Majumdar'15]. We show here that the liveness problem is PSPACE-complete. We also introduce the universal reachability problem. We show that it is decidable, and coNEXPTIME-complete. Finally, using these results, we prove that the verifying regular properties of traces of executions, satisfying some stuttering condition, is also decidable in NEXPTIME for this model.

Related

• Model Checking Parameterized Asynchronous Shared-Memory Systems
• Checking Presence Reachability Properties on Parameterized Shared-Memory Systems
• Safety verification of asynchronous pushdown systems with shaped stacks
• Model-checking parametric lock-sharing systems against regular constraints
• Reachability analysis of multithreaded software with asynchronous communication