@article{Atig:ordered:2012,
    Abstract = {We address the verification problem of ordered multi-pushdown automata: A multi-stack extension of pushdown automata that comes with a constraint on stack transitions such that a pop can only be performed on the first non-empty stack. First, we show that the emptiness problem for ordered multi-pushdown automata is in 2ETIME. Then, we prove that, for an ordered multi-pushdown automata, the set of all predecessors of a regular set of configurations is an effectively constructible regular set. We exploit this result to solve the global model-checking which consists in computing the set of all configurations of an ordered multi-pushdown automaton that satisfy a given w-regular property (expressible in linear-time temporal logics or the linear-time \mu-calculus). As an immediate consequence, we obtain an 2ETIME upper bound for the model-checking problem of w-regular properties for ordered multi-pushdown automata (matching its lower-bound).},
    Author = {Atig, Mohamed F.},
    EPrint = {1209.1916},
    File = {Model-Checking of Ordered Multi-Pushdown Automata - Atig (0) (0) - a - a - b.pdf},
    Journal = {Log. Methods Comput. Sci.},
    Keywords = {multi-pushdown automata},
    Month = {09},
    Number = {3},
    Title = {Model-Checking of Ordered Multi-Pushdown Automata},
    URL = {http://arxiv.org/abs/1209.1916},
    Volume = {8},
    Year = {2012},
    bdsk-url-1 = {http://www.lmcs-online.org/ojs/viewarticle.php?id=924},
    bdsk-url-2 = {http://arxiv.org/abs/1209.1916},
    bdsk-url-3 = {http://dx.doi.org/10.2168/LMCS-8(3:20)2012},
    date-added = {2012-11-19 20:22:12 +0000},
    date-modified = {2015-02-15 21:31:22 +0000},
    ee = {http://dx.doi.org/10.2168/LMCS-8(3:20)2012},
    doi = {10.2168/LMCS-8(3:20)2012}
}

@article{Atig:ordered:2012, Abstract = {We address the verification problem of ordered multi-pushdown automata: A multi-stack extension of pushdown automata that comes with a constraint on stack transitions such that a pop can only be performed on the first non-empty stack. First, we show that the emptiness problem for ordered multi-pushdown automata is in 2ETIME. Then, we prove that, for an ordered multi-pushdown automata, the set of all predecessors of a regular set of configurations is an effectively constructible regular set. We exploit this result to solve the global model-checking which consists in computing the set of all configurations of an ordered multi-pushdown automaton that satisfy a given w-regular property (expressible in linear-time temporal logics or the linear-time \mu-calculus). As an immediate consequence, we obtain an 2ETIME upper bound for the model-checking problem of w-regular properties for ordered multi-pushdown automata (matching its lower-bound).}, Author = {Atig, Mohamed F.}, EPrint = {1209.1916}, File = {Model-Checking of Ordered Multi-Pushdown Automata - Atig (0) (0) - a - a - b.pdf}, Journal = {Log. Methods Comput. Sci.}, Keywords = {multi-pushdown automata}, Month = {09}, Number = {3}, Title = {Model-Checking of Ordered Multi-Pushdown Automata}, URL = {http://arxiv.org/abs/1209.1916}, Volume = {8}, Year = {2012}, bdsk-url-1 = {http://www.lmcs-online.org/ojs/viewarticle.php?id=924}, bdsk-url-2 = {http://arxiv.org/abs/1209.1916}, bdsk-url-3 = {http://dx.doi.org/10.2168/LMCS-8(3:20)2012}, date-added = {2012-11-19 20:22:12 +0000}, date-modified = {2015-02-15 21:31:22 +0000}, ee = {http://dx.doi.org/10.2168/LMCS-8(3:20)2012}, doi = {10.2168/LMCS-8(3:20)2012} }