Complexity results on branching-time pushdown model checking

DOI10.1016/j.tcs.2007.03.049zbMath1121.68073OpenAlexW2087431796MaRDI QIDQ2373715

Laura Bozzelli

Publication date: 16 July 2007

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2007.03.049

zbMATH Keywords

model checkinginfinite-state systemspushdown systemsregular propositional temporal logics

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items

A Branching Time Variant of CaRet ⋮ Branching-time model-checking of probabilistic pushdown automata ⋮ Efficient CTL model-checking for pushdown systems ⋮ Improved model checking of hierarchical systems ⋮ Model checking properties on reduced trace systems ⋮ Temporal logics with language parameters ⋮ Efficient CTL Model-Checking for Pushdown Systems

Cites Work

• Using branching time temporal logic to synthesize synchronization skeletons
• The theory of ends, pushdown automata, and second-order logic
• Alternating automata on infinite trees
• Model checking LTL with regular valuations for pushdown systems
• Computer aided verification. 8th international conference, CAV '96, New Brunswick, NJ, USA, July 31 -- August 3, 1996. Proceedings
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• “Sometimes” and “not never” revisited
• The complexity of propositional linear temporal logics
• Alternation
• Computer Aided Verification
• An automata-theoretic approach to branching-time model checking
• Reachability analysis of pushdown automata: Application to model-checking
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item