Complexity results on branching-time pushdown model checking

DOI10.1016/J.TCS.2007.03.049MaRDI QIDQ2373715zbMATH OpenOpenAlexFDO

Authors 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

infinite-state systemsmodel checkingpushdown systemsregular propositional temporal logics

Mathematics Subject Classification ID

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

Recommendations

• Verification, Model Checking, and Abstract Interpretation
• scientific article; zbMATH DE number 2080197
• Branching-time model-checking of probabilistic pushdown automata
• Model checking of pushdown systems for projection temporal logic
• scientific article; zbMATH DE number 1670780

Cites work

• Alternating automata on infinite trees
• Alternation
• An automata-theoretic approach to branching-time model checking
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Computer Aided Verification
• Computer aided verification. 8th international conference, CAV '96, New Brunswick, NJ, USA, July 31 -- August 3, 1996. Proceedings
• scientific article; zbMATH DE number 1670780 (Why is no real title available?)
• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 1223729 (Why is no real title available?)
• scientific article; zbMATH DE number 1232241 (Why is no real title available?)
• scientific article; zbMATH DE number 1980931 (Why is no real title available?)
• scientific article; zbMATH DE number 2080197 (Why is no real title available?)
• scientific article; zbMATH DE number 1759605 (Why is no real title available?)
• scientific article; zbMATH DE number 2102748 (Why is no real title available?)
• scientific article; zbMATH DE number 794257 (Why is no real title available?)
• Model checking LTL with regular valuations for pushdown systems
• Reachability analysis of pushdown automata: Application to model-checking
• The complexity of propositional linear temporal logics
• The theory of ends, pushdown automata, and second-order logic
• Using branching time temporal logic to synthesize synchronization skeletons
• “Sometimes” and “not never” revisited

Cited in

(12)

• A direct branching algorithm for checking the equivalence of two deterministic pushdown transducers, one of which is real-time strict
• Model checking properties on reduced trace systems
• Efficient CTL model-checking for pushdown systems
• Branching-time model-checking of probabilistic pushdown automata
• Efficient CTL model-checking for pushdown systems
• Improved model checking of hierarchical systems
• scientific article; zbMATH DE number 2080197 (Why is no real title available?)
• Branching-time model-checking of probabilistic pushdown automata
• A Branching Time Variant of CaRet
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• Temporal logics with language parameters

This page was built for publication: Complexity results on branching-time pushdown model checking

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