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

Büchi automataMarkov chainsmodel checkingprobabilistic systemspushdown systemsrecursive systemsstochastic context-free grammarstemporal logic

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) 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)

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)

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

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)