Model-Checking Linear-Time Properties Of Parametrized Asynchronous Shared-Memory Pushdown Systems
COMPUTER AIDED VERIFICATION (CAV 2017), PT II(2017)
摘要
A parametrized verification problem asks if a parallel composition of a leader process with some number of copies of a contributor process can exhibit a behavior satisfying a given property. We focus on the case of pushdown processes communicating via shared memory. 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 verification of general regular properties of traces of executions, satisfying some stuttering condition, is NEXPTIME-complete for this model. We also study two interesting subcases of this problem: we show that liveness is actually PSPACE-complete, and that safety is already NEXPTIME-complete.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络