@inproceedings{10.1007/978-3-319-63390-9_9,
    Abstract = {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.},
    Address = {Cham},
    Author = {Fortin, Marie and Muscholl, Anca and Walukiewicz, Igor},
    BookTitle = {Computer Aided Verification},
    Editor = {Majumdar, Rupak and Kun{\v{c}}ak, Viktor},
    File = {igw-cav17 (0) (0) - a - a - m.pdf},
    ISBN = {978-3-319-63390-9},
    Pages = {155--175},
    Publisher = {Springer International Publishing},
    Title = {Model-Checking Linear-Time Properties of Parametrized Asynchronous Shared-Memory Pushdown Systems},
    Year = {2017},
    date-added = {2019-03-30 14:10:10 +0100},
    date-modified = {2019-03-30 14:10:10 +0100},
    doi = {10.1007/978-3-319-63390-9_9}
}

@inproceedings{10.1007/978-3-319-63390-9_9, Abstract = {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.}, Address = {Cham}, Author = {Fortin, Marie and Muscholl, Anca and Walukiewicz, Igor}, BookTitle = {Computer Aided Verification}, Editor = {Majumdar, Rupak and Kun{\v{c}}ak, Viktor}, File = {igw-cav17 (0) (0) - a - a - m.pdf}, ISBN = {978-3-319-63390-9}, Pages = {155--175}, Publisher = {Springer International Publishing}, Title = {Model-Checking Linear-Time Properties of Parametrized Asynchronous Shared-Memory Pushdown Systems}, Year = {2017}, date-added = {2019-03-30 14:10:10 +0100}, date-modified = {2019-03-30 14:10:10 +0100}, doi = {10.1007/978-3-319-63390-9_9} }