Model checking probabilistic systems against pushdown specifications

DOI10.1016/j.ipl.2012.01.006zbMath1243.68214OpenAlexW2067613458MaRDI QIDQ436316

Christel Baier, Manuela Berg, Clemens Dubslaff

Publication date: 20 July 2012

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ipl.2012.01.006

zbMATH Keywords

Markov chainsformal methodspushdown systemsprobabilistic model checkingcontext-free specifications

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items

Model Checking Temporal Properties of Recursive Probabilistic Programs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• \(\omega\)-computations on deterministic pushdown machines
• Verification of probabilistic systems with faulty communication
• Visibly pushdown languages
• On ω-sets associated with context-free languages
• The complexity of probabilistic verification
• A NEW TYPE OF PUSHDOWN AUTOMATA ON INFINITE TREES
• Tools and Algorithms for the Construction and Analysis of Systems
• Model Checking Probabilistic Pushdown Automata
• Decisive Markov Chains
• STACS 2005
• STACS 2005