Branching-time model-checking of probabilistic pushdown automata

DOI10.1016/j.jcss.2013.07.001zbMath1311.68084OpenAlexW2088970711MaRDI QIDQ394999

Vojtěch Forejt, Václav Brožek, Tomáš Brázdil, Antonín Kučera

Publication date: 28 January 2014

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jcss.2013.07.001

zbMATH Keywords

model-checkingpushdown automataprobabilistic systemsbranching-time logics

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

Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems ⋮ Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Reachability in recursive Markov decision processes
• A logic for reasoning about time and reliability
• Model checking LTL with regular valuations for pushdown systems
• Analyzing probabilistic pushdown automata
• Complexity results on branching-time pushdown model checking
• STACS 2005. 22nd annual symposium on theoretical aspects of computer science, Stuttgart, Germany, February 24--26, 2005. Proceedings.
• Model Checking of Recursive Probabilistic Systems
• Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations
• Alternation
• Branching-Time Model-Checking of Probabilistic Pushdown Automata
• Model Checking Probabilistic Pushdown Automata
• Qualitative Reachability in Stochastic BPA Games
• Discounted Properties of Probabilistic Pushdown Automata
• Tools and Algorithms for the Construction and Analysis of Systems
• STACS 2005
• Automata, Languages and Programming