Branching-time model-checking of probabilistic pushdown automata
From MaRDI portal
Publication:394999
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
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