On parametrized verification of asynchronous, shared-memory pushdown systems
Formal Languages and Automata Theory
2016-07-19 v2 Logic in Computer Science
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.
Cite
@article{arxiv.1606.08707,
title = {On parametrized verification of asynchronous, shared-memory pushdown systems},
author = {Marie Fortin and Anca Muscholl and Igor Walukiewicz},
journal= {arXiv preprint arXiv:1606.08707},
year = {2016}
}
Comments
43 pages