Model-Checking of Ordered Multi-Pushdown Automata

We address the verification problem of ordered multi-pushdown automata: Amulti-stack extension of pushdown automata that comes with a constraint onstack transitions such that a pop can only be performed on the first non-emptystack. First, we show that the emptiness problem for ordered multi-pushdownautomata is in 2ETIME. Then, we prove that, for an ordered multi-pushdownautomata, the set of all predecessors of a regular set of configurations is aneffectively constructible regular set. We exploit this result to solve theglobal model-checking which consists in computing the set of all configurationsof 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 themodel-checking problem of w-regular properties for ordered multi-pushdownautomata (matching its lower-bound).Comment: 31 page