Model checking CTL properties of pushdown systems

DOI10.1007/3-540-44450-5_10MaRDI QIDQ4472439zbMATH OpenFDO

Authors Igor Walukiewicz

Publication date 4 August 2004

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/1974/19740127.htm

Mathematics Subject Classification ID

Logic in computer science (03B70) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Verification, Model Checking, and Abstract Interpretation
• Complexity results on branching-time pushdown model checking
• Model checking of pushdown systems for projection temporal logic
• Efficient CTL model-checking for pushdown systems
• scientific article; zbMATH DE number 1232241

Cited in

(35)

• The complexity of bisimilarity-checking for one-counter processes.
• Checking simple properties of transition systems defined by Thue specifications
• Analyzing probabilistic pushdown automata
• Hyperplane separation technique for multidimensional mean-payoff games
• Complexity results on branching-time pushdown model checking
• Model checking of pushdown systems for projection temporal logic
• Fixpoint logics over hierarchical structures
• Temporal property verification as a program analysis task
• Characterizing EF and EX tree logics
• A general approach to comparing infinite-state systems with their finite-state specifications
• Using assumptions to distribute CTL model checking
• Using assumptions to distribute alternation free {\(\mu\)}-calculus model checking
• Global model checking of ordered multi-pushdown systems
• scientific article; zbMATH DE number 6719346 (Why is no real title available?)
• Model Checking CTL is Almost Always Inherently Sequential
• Efficient CTL model-checking for pushdown systems
• Model checking EGF on basic parallel processes
• Model checking procedural programs
• Model checking concurrent programs
• An automata-theoretic approach to infinite-state systems
• Model Checking FO(R) over One-Counter Processes and beyond
• 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 2090156 (Why is no real title available?)
• Efficient CTL verification via Horn constraints solving
• Model-Checking HyperLTL for Pushdown Systems
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• Weak bisimilarity between finite-state systems and BPA or normed BPP is decidable in polynomial time
• Church synthesis on register automata over linearly ordered data domains
• Module checking of pushdown multi-agent systems
• Synchronized CTL over one-counter automata
• Church synthesis on register automata over linearly ordered data domains
• On the complexity of checking semantic equivalences between pushdown processes and finite-state processes

This page was built for publication: Model checking CTL properties of pushdown systems

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