The complexity of model checking multi-stack systems

DOI10.1007/s00224-016-9700-6zbMath1372.68164OpenAlexW2508346251MaRDI QIDQ2398213

Benedikt Bollig, Roy Mennicke, Dietrich Kuske

Publication date: 15 August 2017

Published in: Theory of Computing Systems (Search for Journal in Brave)

Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.1022.6185

zbMATH Keywords

model checkingtemporal logicsmulti-stack systemsmultiply nested words

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Temporal logic (03B44)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• An optimal construction of Hanf sentences
• Temporal logics for concurrent recursive programs: satisfiability and model checking
• Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces
• On monadic NP vs monadic co-NP
• MSO Decidability of Multi-Pushdown Systems via Split-Width
• Model-Checking of Ordered Multi-Pushdown Automata
• A Temporal Logic for Multi-threaded Programs
• Model Checking Concurrent Recursive Programs Using Temporal Logics
• Scope-bounded multistack pushdown systems: fixed-point, sequentialization, and tree-width
• Reachability of Multistack Pushdown Systems with Scope-Bounded Matching Relations
• Adding nesting structure to words
• Verifying Communicating Multi-pushdown Systems via Split-Width
• Emptiness of Multi-pushdown Automata Is 2ETIME-Complete
• An Infinite Automaton Characterization of Double Exponential Time
• First-Order and Temporal Logics for Nested Words
• The Complexity of Translating Logic to Finite Automata
• Linear-Time Model-Checking for Multithreaded Programs under Scope-Bounding
• The Complexity of Model Checking Multi-stack Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• The tree width of auxiliary storage
• Context-Bounded Analysis of Concurrent Queue Systems
• MULTI-PUSH-DOWN LANGUAGES AND GRAMMARS
• Tools and Algorithms for the Construction and Analysis of Systems
• Reachability Analysis of Communicating Pushdown Systems
• CONCUR 2005 – Concurrency Theory