Analyzing probabilistic pushdown automata

DOI10.1007/s10703-012-0166-0zbMath1291.68226OpenAlexW2083374362MaRDI QIDQ2248071

Stefan Kiefer, Antonín Kučera, Tomáš Brázdil, Javier Esparza

Publication date: 30 June 2014

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://is.muni.cz/repo/1076453

zbMATH Keywords

Markov chainsmodel checkingpushdown automata

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items

Model Checking Probabilistic Systems, Ratio and Weight Quantiles, Branching-time model-checking of probabilistic pushdown automata, Model Checking Temporal Properties of Recursive Probabilistic Programs, Unnamed Item, Unnamed Item, Preface to the special issue on probabilistic model checking, Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems, Computing expected runtimes for constant probability programs, Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Reachability in recursive Markov decision processes
• Complexity of deciding Tarski algebra
• A logic for reasoning about time and reliability
• A lattice-theoretical fixpoint theorem and its applications
• One-Counter Stochastic Games
• Runtime Analysis of Probabilistic Programs with Unbounded Recursion
• Approximating the Termination Value of One-Counter MDPs and Stochastic Games
• COMPUTING LEAST FIXED POINTS OF PROBABILISTIC SYSTEMS OF POLYNOMIALS
• A First Look at Rigorous Probability Theory
• Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations
• On the Complexity of Numerical Analysis
• Probability with Martingales
• Branching-Time Model-Checking of Probabilistic Pushdown Automata
• CONCUR 2004 - Concurrency Theory
• Polynomial time algorithms for multi-type branching processesand stochastic context-free grammars
• Discounted Properties of Probabilistic Pushdown Automata
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• STACS 2005
• STACS 2005
• Verification, Model Checking, and Abstract Interpretation
• Reachability analysis of pushdown automata: Application to model-checking