Efficient CTL model-checking for pushdown systems

DOI10.1016/j.tcs.2014.07.001zbMath1360.68599OpenAlexW2020438328MaRDI QIDQ402129

Fu Song, Tayssir Touili

Publication date: 27 August 2014

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

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

zbMATH Keywords

model-checkingCTLCTL with regular valuationspushdown system

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

A Branching Time Variant of CaRet ⋮ Not all bugs are created equal, but robust reachability can tell the difference ⋮ Analyzing pushdown systems with stack manipulation

Uses Software

• PuMoC

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A saturation method for the modal \(\mu \)-calculus over pushdown systems
• 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
• A lattice-theoretical fixpoint theorem and its applications
• 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
• Reachability analysis of pushdown automata: Application to model-checking