Algorithmic verification of recursive probabilistic state machines

DOI10.1007/978-3-540-31980-1_17MaRDI QIDQ5703763zbMATH OpenOpenAlexFDO

Authors Kousha Etessami, Mihalis Yannakakis

Publication date 10 November 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b107194

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Model checking of recursive probabilistic systems
• Recursive Markov decision processes and recursive stochastic games
• Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations
• Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations
• Automata, Probability, and Recursion

Cited in

(20)

• A note on the attractor-property of infinite-state Markov chains
• Formally verified algorithms for upper-bounding state space diameters
• Analyzing probabilistic pushdown automata
• Deciding probabilistic bisimilarity over infinite-state probabilistic systems
• Model checking of recursive probabilistic systems
• On probabilistic parallel programs with process creation and synchronisation
• Runtime analysis of probabilistic programs with unbounded recursion
• Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations
• Automata, Probability, and Recursion
• Branching-time model-checking of probabilistic pushdown automata
• Branching-time model-checking of probabilistic pushdown automata
• Verifying -regular properties of Markov chains
• On the Complexity of Ltl Model-Checking of Recursive State Machines
• Verifying probabilistic procedural programs
• Efficient analysis of probabilistic programs with an unbounded counter
• Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations
• Reachability in Recursive Markov Decision Processes
• Probabilistic verification beyond context-freeness
• Runtime analysis of probabilistic programs with unbounded recursion
• Verification of well-formed communicating recursive state machines

This page was built for publication: Algorithmic verification of recursive probabilistic state machines

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