Atig, Mohamed Faouzi - Model-Checking of Ordered Multi-Pushdown Automata

lmcs:871 - Logical Methods in Computer Science, September 20, 2012, Volume 8, Issue 3
Model-Checking of Ordered Multi-Pushdown Automata

Authors: Atig, Mohamed Faouzi

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).

DOI : 10.2168/LMCS-8(3:20)2012
Volume: Volume 8, Issue 3
Published on: September 20, 2012
Submitted on: May 2, 2011
Keywords: Computer Science - Logic in Computer Science,Computer Science - Formal Languages and Automata Theory,D.2.4, D.3.1, F.4.3, I.2.2


Consultation statistics

This page has been seen 163 times.
This article's PDF has been downloaded 202 times.