CEGAR for compositional analysis of qualitative properties in Markov decision processes
From MaRDI portal
Publication:746785
Recommendations
- Compositional reasoning for Markov decision processes (extended abstract)
- Qualitative Logics and Equivalences for Probabilistic Systems
- Multi-objective Model Checking of Markov Decision Processes
- Multi-Objective Model Checking of Markov Decision Processes
- Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives
Cites work
- scientific article; zbMATH DE number 1670775 (Why is no real title available?)
- scientific article; zbMATH DE number 3148886 (Why is no real title available?)
- scientific article; zbMATH DE number 3926220 (Why is no real title available?)
- scientific article; zbMATH DE number 176729 (Why is no real title available?)
- scientific article; zbMATH DE number 1306878 (Why is no real title available?)
- scientific article; zbMATH DE number 1134975 (Why is no real title available?)
- scientific article; zbMATH DE number 2038762 (Why is no real title available?)
- scientific article; zbMATH DE number 1863173 (Why is no real title available?)
- scientific article; zbMATH DE number 1884411 (Why is no real title available?)
- scientific article; zbMATH DE number 2090703 (Why is no real title available?)
- scientific article; zbMATH DE number 794262 (Why is no real title available?)
- scientific article; zbMATH DE number 910719 (Why is no real title available?)
- scientific article; zbMATH DE number 5585443 (Why is no real title available?)
- scientific article; zbMATH DE number 2209335 (Why is no real title available?)
- A counterexample-guided abstraction-refinement framework for Markov decision processes
- A logic for reasoning about time and reliability
- A survey of partial-observation stochastic parity games
- Algorithms for Omega-Regular Games with Imperfect Information
- Alternating-time temporal logic
- An \(O(n^2)\) time algorithm for alternating Büchi games
- Assume-guarantee verification for probabilistic systems
- Automata, Languages and Programming
- Automata, logics, and infinite games. A guide to current research
- Code aware resource management
- Computer Aided Verification
- Computer Science Logic
- Concurrent reachability games
- Decidable problems for probabilistic automata on infinite words
- Efficient and dynamic algorithms for alternating Büchi games and maximal end-component decomposition
- Faster algorithms for alternating refinement relations
- Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification
- Fun with fireWire: A comparative study of formal verification methods applied to the IEEE 1394 root contention protocol
- Games with a Weak Adversary
- Infinite games on finitely coloured graphs with applications to automata on infinite trees
- Interface simulation distances
- Learning to divide and conquer: applying the \(L^*\) algorithm to automate assume-guarantee reasoning
- Model checking of probabilistic and nondeterministic systems
- Multi-Objective Model Checking of Markov Decision Processes
- Myths about the mutual exclusion problem
- Number of quantifiers is better than number of tape cells
- On Decision Problems for Probabilistic Büchi Automata
- On the menbership problem for functional and multivalued dependencies in relational databases
- POMDPs under probabilistic semantics
- Partial-observation stochastic games: how to win when belief fails
- Probabilistic CEGAR
- Qualitative Logics and Equivalences for Probabilistic Systems
- Qualitative analysis of concurrent mean-payoff games
- Qualitative analysis of partially-observable Markov decision processes
- Qualitative concurrent parity games
- Qualitative concurrent parity games: bounded rationality
- Qualitative determinacy and decidability of stochastic games with signals
- Quantitative stochastic parity games
- Randomness for free
- Solving partial-information stochastic parity games
- Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives
- Symmetry breaking in distributed networks
- The Value 1 Problem Under Finite-memory Strategies for Concurrent Mean-payoff Games
- The complexity of partial-observation stochastic parity games with finite-memory strategies
- The complexity of probabilistic verification
- The complexity of quantitative concurrent parity games
- The complexity of stochastic Müller games
- Thread-modular abstraction refinement.
- Tighter Bounds for the Determinisation of Büchi Automata
- Verification of the randomized consensus algorithm of Aspnes and Herlihy: a case study
- What is decidable about partially observable Markov decision processes with omega-regular objectives
Cited in
(6)- Verification of general Markov decision processes by approximate similarity relations and policy refinement
- Verification of general Markov decision processes by approximate similarity relations and policy refinement
- Of cores: a partial-exploration framework for Markov decision processes
- Qualitative Logics and Equivalences for Probabilistic Systems
- Compositional reasoning for Markov decision processes (extended abstract)
- Of cores: a partial-exploration framework for Markov decision processes
This page was built for publication: CEGAR for compositional analysis of qualitative properties in Markov decision processes
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q746785)
