uu.seUppsala University Publications
Change search
ReferencesLink to record
Permanent link

Direct link
Model-Checking of Ordered Multi-Pushdown Automata
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
2012 (English)In: Logical Methods in Computer Science, ISSN 1860-5974, Vol. 8, no 3, 20- p.Article in journal (Refereed) Published
Abstract [en]

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

Place, publisher, year, edition, pages
2012. Vol. 8, no 3, 20- p.
Keyword [en]
Multi-pushdown Automata, Program Verification, LTL model-Checking
National Category
Engineering and Technology
URN: urn:nbn:se:uu:diva-184665DOI: 10.2168/LMCS-8(3:20)2012ISI: 000309447200020OAI: oai:DiVA.org:uu-184665DiVA: diva2:567119
Available from: 2012-11-12 Created: 2012-11-12 Last updated: 2012-11-12Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Search in DiVA

By author/editor
Atig, Mohamed Faouzi
By organisation
Computer Systems
In the same journal
Logical Methods in Computer Science
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 202 hits
ReferencesLink to record
Permanent link

Direct link