CEGAR for compositional analysis of qualitative properties in Markov decision processes
From MaRDI portal
Publication:746785
DOI10.1007/S10703-015-0235-2zbMATH Open1322.68137OpenAlexW1165962627MaRDI QIDQ746785FDOQ746785
Authors: Krishnendu Chatterjee, Martin Chmelík, Przemysław Daca 
Publication date: 20 October 2015
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10703-015-0235-2
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
Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Applications of game theory (91A80) Specification and verification (program logics, model checking, etc.) (68Q60) Markov and semi-Markov decision processes (90C40)
Cites Work
- Title not available (Why is that?)
- Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives
- Efficient and dynamic algorithms for alternating Büchi games and maximal end-component decomposition
- Alternating-time temporal logic
- The complexity of probabilistic verification
- Title not available (Why is that?)
- Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification
- An \(O(n^2)\) time algorithm for alternating Büchi games
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Computer Aided Verification
- Learning to divide and conquer: applying the \(L^*\) algorithm to automate assume-guarantee reasoning
- Myths about the mutual exclusion problem
- A logic for reasoning about time and reliability
- Automata, logics, and infinite games. A guide to current research
- POMDPs under probabilistic semantics
- Model checking of probabilistic and nondeterministic systems
- What is decidable about partially observable Markov decision processes with omega-regular objectives
- Randomness for free
- Qualitative analysis of partially-observable Markov decision processes
- Algorithms for Omega-Regular Games with Imperfect Information
- Title not available (Why is that?)
- Verification of the randomized consensus algorithm of Aspnes and Herlihy: a case study
- Games with a Weak Adversary
- The complexity of partial-observation stochastic parity games with finite-memory strategies
- On Decision Problems for Probabilistic Büchi Automata
- Concurrent reachability games
- Title not available (Why is that?)
- A survey of partial-observation stochastic parity games
- Quantitative stochastic parity games
- Automata, Languages and Programming
- Thread-modular abstraction refinement.
- Infinite games on finitely coloured graphs with applications to automata on infinite trees
- Tighter Bounds for the Determinisation of Büchi Automata
- Multi-Objective Model Checking of Markov Decision Processes
- Solving partial-information stochastic parity games
- Assume-guarantee verification for probabilistic systems
- Title not available (Why is that?)
- Probabilistic CEGAR
- A counterexample-guided abstraction-refinement framework for Markov decision processes
- Symmetry breaking in distributed networks
- Number of quantifiers is better than number of tape cells
- The complexity of quantitative concurrent parity games
- On the menbership problem for functional and multivalued dependencies in relational databases
- The complexity of stochastic Müller games
- Title not available (Why is that?)
- Computer Science Logic
- Title not available (Why is that?)
- Title not available (Why is that?)
- Interface simulation distances
- Title not available (Why is that?)
- Decidable problems for probabilistic automata on infinite words
- Faster algorithms for alternating refinement relations
- Partial-observation stochastic games: how to win when belief fails
- Fun with fireWire: A comparative study of formal verification methods applied to the IEEE 1394 root contention protocol
- Code aware resource management
- Qualitative analysis of concurrent mean-payoff games
- Qualitative concurrent parity games
- Qualitative concurrent parity games: bounded rationality
- Qualitative Logics and Equivalences for Probabilistic Systems
- Qualitative determinacy and decidability of stochastic games with signals
- The Value 1 Problem Under Finite-memory Strategies for Concurrent Mean-payoff Games
Cited In (4)
- Qualitative Logics and Equivalences for Probabilistic Systems
- 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
- Compositional reasoning for Markov decision processes (extended abstract)
Uses Software
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)
