Modelchecking of Ordered Multipushdown Automata
Title: Modelchecking of Ordered Multipushdown Automata Speaker: Mohamed Faouzi Atig, University of Uppsala (Sweden) Venue: IF 4.314.33. Wednesday, November 27, 4:30 pm.
What 


When 
Nov 27, 2013 from 04:30 PM to 05:30 PM 
Where  IF 4.314.33 
Contact Name  Rik Sarkar 
Add event to calendar 
vCal iCal 
Title:
MODELCHECKING OF ORDERED MULTIPUSHDOWN AUTOMATA
Abstract:
We address the verification problem of ordered multipushdown automata: A multistack extension of pushdown automata that comes with a constraint on stack transitions such that a pop can only be performed on the first nonempty stack. First, we show that the emptiness problem for ordered multipushdown automata is in 2ETIME. Then, we prove that, for an ordered multipushdown 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 modelchecking which consists in computing the set of all configurations of an ordered multipushdown automaton that satisfy a given omegaregular property. As an immediate consequence, we obtain an 2ETIME upper bound for the modelchecking problem of omegaregular properties for ordered multipushdown automata (matching its lowerbound).