Personal tools
You are here: Home Events LFCS Seminars-Folder Model-checking of Ordered Multi-pushdown Automata

Model-checking of Ordered Multi-pushdown Automata

Title: Model-checking of Ordered Multi-pushdown Automata Speaker: Mohamed Faouzi Atig, University of Uppsala (Sweden) Venue: IF 4.31-4.33. Wednesday, November 27, 4:30 pm.

When Nov 27, 2013
from 04:30 PM to 05:30 PM
Where IF 4.31-4.33
Contact Name Rik Sarkar
Add event to calendar vCal




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 omega-regular property. As an immediate consequence, we obtain an 2ETIME upper bound for the model-checking problem of omega-regular properties for ordered multi-pushdown automata (matching its lower-bound).



Document Actions