Model-checking linear-time properties of parametrized asynchronous shared-memory pushdown systems

International audienceA 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