Certificates for probabilistic pushdown automata via optimistic value iteration

DOI10.1007/978-3-031-30820-8_24zbMATH Open1547.68384MaRDI QIDQ6536144

Tobias Winkler, J.-P. Katoen

Publication date: 5 April 2024

zbMATH Keywords

probabilistic model checkingprobabilistic pushdown automatacertified algorithmsprobabilistic recursive programs

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Certifying algorithms
• Runtime analysis of probabilistic programs with unbounded recursion
• Latticed \(k\)-induction with an application to probabilistic programs
• An introduction to randomized algorithms
• Ensuring the reliability of your model checker: interval iteration for Markov decision processes
• Optimistic value iteration
• Analyzing probabilistic pushdown automata
• Model-based machine learning
• Computing the Least Fixed Point of Positive Polynomial Systems
• COMPUTING LEAST FIXED POINTS OF PROBABILISTIC SYSTEMS OF POLYNOMIALS
• Upper Bounds for Newton’s Method on Monotone Polynomial Systems, and P-Time Model Checking of Probabilistic One-Counter Automata
• Reachability in MDPs: Refining Convergence of Value Iteration
• Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations
• Reasoning about Recursive Probabilistic Programs
• Convergence Thresholds of Newton's Method for Monotone Polynomial Equations
• Farkas Certificates and Minimal Witnesses for Probabilistic Reachability Constraints
• Verified Certification of Reachability Checking for Timed Automata
• JGraphT—A Java Library for Graph Data Structures and Algorithms
• Model Checking Probabilistic Pushdown Automata
• STACS 2005
• Sound value iteration
• Model Checking Temporal Properties of Recursive Probabilistic Programs
• Optimistic and topological value iteration for simple stochastic games
• Minimal Witnesses for Probabilistic Timed Automata
• Correct probabilistic model checking with floating-point arithmetic

This page was built for publication: Certificates for probabilistic pushdown automata via optimistic value iteration

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6536144)