CEGAR for compositional analysis of qualitative properties in Markov decision processes
From MaRDI portal
Publication:746785
DOI10.1007/s10703-015-0235-2zbMath1322.68137OpenAlexW1165962627MaRDI QIDQ746785
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
Applications of game theory (91A80) Markov and semi-Markov decision processes (90C40) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The complexity of stochastic Müller games
- Symmetry breaking in distributed networks
- Learning to divide and conquer: applying the \(L^*\) algorithm to automate assume-guarantee reasoning
- Myths about the mutual exclusion problem
- Number of quantifiers is better than number of tape cells
- Infinite games on finitely coloured graphs with applications to automata on infinite trees
- A logic for reasoning about time and reliability
- Fun with fireWire: A comparative study of formal verification methods applied to the IEEE 1394 root contention protocol
- Automata, logics, and infinite games. A guide to current research
- Code aware resource management
- Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives
- A survey of partial-observation stochastic parity games
- POMDPs under probabilistic semantics
- Qualitative analysis of concurrent mean-payoff games
- Concurrent reachability games
- A counterexample-guided abstraction-refinement framework for markov decision processes
- Qualitative concurrent parity games
- Model checking of probabilistic and nondeterministic systems
- What is Decidable about Partially Observable Markov Decision Processes with omega-Regular Objectives.
- Partial-Observation Stochastic Games: How to Win When Belief Fails
- Decidable Problems for Probabilistic Automata on Infinite Words
- Efficient and Dynamic Algorithms for Alternating Büchi Games and Maximal End-Component Decomposition
- Qualitative Concurrent Parity Games: Bounded Rationality
- Alternating-time temporal logic
- Probabilistic CEGAR
- Assume-Guarantee Verification for Probabilistic Systems
- The complexity of quantitative concurrent parity games
- Randomness for Free
- Qualitative Analysis of Partially-Observable Markov Decision Processes
- Algorithms for Omega-Regular Games with Imperfect Information
- Tighter Bounds for the Determinisation of Büchi Automata
- Multi-Objective Model Checking of Markov Decision Processes
- Qualitative Logics and Equivalences for Probabilistic Systems
- On the menbership problem for functional and multivalued dependencies in relational databases
- The complexity of probabilistic verification
- Qualitative Determinacy and Decidability of Stochastic Games with Signals
- Faster Algorithms for Alternating Refinement Relations
- Verification of the randomized consensus algorithm of Aspnes and Herlihy: a case study
- Games with a Weak Adversary
- Solving Partial-Information Stochastic Parity Games
- Computer Science Logic
- 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
- On Decision Problems for Probabilistic Büchi Automata
- Computer Aided Verification
- Automata, Languages and Programming
- Computer Aided Verification
This page was built for publication: CEGAR for compositional analysis of qualitative properties in Markov decision processes
