Model checking of recursive probabilistic systems

DOI10.1145/2159531.2159534MaRDI QIDQ2946660zbMATH OpenOpenAlexFDO

Authors Kousha Etessami, Mihalis Yannakakis

Publication date 17 September 2015

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2159531.2159534

zbMATH Keywords

Markov chainsmodel checkingpushdown systemstemporal logicstochastic context-free grammarsprobabilistic systemsrecursive systemsBüchi automata

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Analysis of algorithms and problem complexity (68Q25) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Tools and Algorithms for the Construction and Analysis of Systems
• Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations
• STACS 2005
• Automata, Languages and Programming
• Automata, Probability, and Recursion

Cited in

(22)

• Branching-time model-checking of probabilistic pushdown automata
• The finite satisfiability problem for PCTL is undecidable
• On the Complexity of Ltl Model-Checking of Recursive State Machines
• Counterexamples in Probabilistic Model Checking
• Be lazy and don't care: faster CTL model checking for recursive state machines
• On the termination problem for probabilistic higher-order recursive programs
• Model checking probabilistic systems
• Probabilistic Guarded P Systems, A New Formal Modelling Framework
• The satisfiability problem for a quantitative fragment of PCTL
• Language equivalence of probabilistic pushdown automata
• The finite satisfiability problem for PCTL is undecidable
• A polynomial time algorithm for computing extinction probabilities of multitype branching processes
• Recursive Markov decision processes and recursive stochastic games
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification
• Model Checking Probabilistic Pushdown Automata
• Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations
• STACS 2005
• The satisfiability problem for a quantitative fragment of PCTL
• Automata, Probability, and Recursion
• Deciding fast termination for probabilistic VASS with nondeterminism
• Probabilistic black-box reachability checking (extended version)

This page was built for publication: Model checking of recursive probabilistic systems

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