Branching-Time Model-Checking of Probabilistic Pushdown Automata

DOI10.1016/j.entcs.2009.05.031zbMath1347.68220OpenAlexW2011353919MaRDI QIDQ5179051

Václav Brožek, Vojtěch Forejt, Tomáš Brázdil

Publication date: 19 March 2015

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

Full work available at URL: https://doi.org/10.1016/j.entcs.2009.05.031

zbMATH Keywords

Markov chainsmodel checkingtemporal logicsprobabilistic pushdown automata

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Formal languages and automata (68Q45) Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.) (60J20) Specification and verification (program logics, model checking, etc.) (68Q60) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Temporal logic (03B44)

Related Items (3)

Branching-time model-checking of probabilistic pushdown automata ⋮ Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives ⋮ Analyzing probabilistic pushdown automata

Cites Work

• Unnamed Item
• Unnamed Item
• CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus
• A logic for reasoning about time and reliability
• Model checking LTL with regular valuations for pushdown systems
• Alternation
• Temporal logics for the specification of performance and reliability
• Tools and Algorithms for the Construction and Analysis of Systems
• STACS 2005
• STACS 2005
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Branching-Time Model-Checking of Probabilistic Pushdown Automata