On parametrized verification of asynchronous, shared-memory pushdown systems.
arXiv: Formal Languages and Automata Theory(2016)
摘要
We consider the model of parametrized asynchronous shared-memory pushdown systems, as introduced in [Hagueu002711]. In a series of recent papers it has been shown that reachability in this model is PSPACE-complete [Esparza, Ganty, Majumdaru002713] and that liveness is decidable in NEXPTIME [Durand-Gasselin, Esparza, Ganty, Majumdaru002715]. 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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络