Efficient CTL Model-Checking for Pushdown Systems

DOI10.1007/978-3-642-23217-6_29zbMath1343.68156OpenAlexW8705220MaRDI QIDQ3090847

Tayssir Touili, Fu Song

Publication date: 2 September 2011

Published in: CONCUR 2011 – Concurrency Theory (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-23217-6_29

Mathematics Subject Classification ID

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

Related Items (6)

Model Checking Procedural Programs ⋮ Ordered multi-stack visibly pushdown automata ⋮ Branching Temporal Logic of Calls and Returns for Pushdown Systems ⋮ Analyzing pushdown systems with stack manipulation ⋮ Unnamed Item ⋮ Model checking dynamic pushdown networks

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Pushdown module checking
• Note on winning positions on pushdown games with \(\omega\)-regular conditions
• Deciding emptiness for stack automata on infinite trees
• Model checking LTL with regular valuations for pushdown systems
• Complexity results on branching-time pushdown model checking
• Efficient Algorithms for Alternating Pushdown Systems with an Application to the Computation of Certificate Chains
• An Automata-Theoretic Approach to Infinite-State Systems
• Model checking the full modal mu-calculus for infinite sequential processes
• Computer Aided Verification
• Pushdown Module Checking

This page was built for publication: Efficient CTL Model-Checking for Pushdown Systems