Model checking LTL with regular valuations for pushdown systems

DOI10.1016/S0890-5401(03)00139-1zbMath1078.68081OpenAlexW2114132089MaRDI QIDQ1887158

Javier Esparza, Antonín Kučera, Stefan Schwoon

Publication date: 23 November 2004

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0890-5401(03)00139-1

zbMATH Keywords

Model checkingPushdown automataLinear-time logic

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (29)

Reactive synthesis from visibly register pushdown automata ⋮ A Branching Time Variant of CaRet ⋮ Model-checking structured context-free languages ⋮ Complexity results on branching-time pushdown model checking ⋮ Model Checking Procedural Programs ⋮ A generic framework for checking semantic equivalences between pushdown automata and finite-state automata ⋮ Branching-time model-checking of probabilistic pushdown automata ⋮ Verification of programs with exceptions through operator precedence automata ⋮ Efficient CTL model-checking for pushdown systems ⋮ Branching Temporal Logic of Calls and Returns for Pushdown Systems ⋮ Operator precedence temporal logic and model checking ⋮ Reachability in recursive Markov decision processes ⋮ Multi-matching nested relations ⋮ Reachability relations of timed pushdown automata ⋮ The word problem for visibly pushdown languages described by grammars ⋮ Verification of well-formed communicating recursive state machines ⋮ Complexity results for prefix grammars ⋮ Pushdown module checking ⋮ Branching-Time Model-Checking of Probabilistic Pushdown Automata ⋮ An Automata-based Approach for CTL⋆ With Constraints ⋮ Temporal logics with language parameters ⋮ Qualitative reachability in stochastic BPA games ⋮ On the complexity of checking semantic equivalences between pushdown processes and finite-state processes ⋮ Unnamed Item ⋮ PDL with intersection and converse: satisfiability and infinite-state model checking ⋮ Efficient CTL Model-Checking for Pushdown Systems ⋮ CaRet With Forgettable Past ⋮ Model Checking FO(R) over One-Counter Processes and beyond ⋮ Model checking dynamic pushdown networks

Uses Software

• Bebop

Cites Work

• Automata-theoretic techniques for modal logics of programs
• Modalities for model checking: Branching time logic strikes back
• Model checking the full modal mu-calculus for infinite sequential processes
• Reachability analysis of pushdown automata: Application to model-checking
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Model checking LTL with regular valuations for pushdown systems