Global model checking of ordered multi-pushdown systems

DOI10.4230/LIPICS.FSTTCS.2010.216MaRDI QIDQ2908851zbMATH OpenOpenAlexFDO

Authors Mohamed Faouzi Atig

Publication date 29 August 2012

Full work available at URL https://arxiv.org/abs/1209.1916, http://subs.emis.de/LIPIcs/frontdoor_ce27.html

zbMATH Keywords

concurrent programsglobal model-checkingpushdown systems

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

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

Recommendations

• Model-checking of ordered multi-pushdown automata
• Model-checking bounded multi-pushdown systems
• Computer Aided Verification
• scientific article; zbMATH DE number 2080197
• Unconventional Computation
• On Global Model Checking Trees Generated by Higher-Order Recursion Schemes
• Model-checking on ordered structures
• The complexity of model checking (collapsible) higher-order pushdown systems

Cited in

(13)

• On store languages and applications
• Model-checking of ordered multi-pushdown automata
• Emptiness of ordered multi-pushdown automata is 2ETIME-complete
• Temporal logics for concurrent recursive programs: satisfiability and model checking
• Model-checking bounded multi-pushdown systems
• Data multi-pushdown automata
• On the Complexity of Bounded Context Switching.
• Adjacent ordered multi-pushdown systems
• Ordered tree-pushdown systems
• Adjacent ordered multi-pushdown systems
• Reasoning about reversal-bounded counter machines
• On the complexity of multi-pushdown games
• Store languages of Turing machines and counter machines

This page was built for publication: Global model checking of ordered multi-pushdown systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2908851)