3 citations · 9 across the 10 of their papers we have counts for
16 papers
Learning Algorithms for Verification of Markov Decision Processes
Tomáš Brázdil, Krishnendu Chatterjee, Martin Chmelik +6
We present a general framework for applying learning algorithms and heuristical guidance to the verification of Markov decision processes (MDPs). The primary goal of our techniques…
Sensor Synthesis for POMDPs with Reachability Objectives
Krishnendu Chatterjee, Martin Chmelik, Ufuk Topcu
Partially observable Markov decision processes (POMDPs) are widely used in probabilistic planning problems in which an agent interacts with an environment using noisy and imprecise…
Stochastic Shortest Path with Energy Constraints in POMDPs
Tomáš Brázdil, Krishnendu Chatterjee, Martin Chmelík +2
We consider partially observable Markov decision processes (POMDPs) with a set of target states and positive integer costs associated with every transition. The traditional optimiz…
A Symbolic SAT-based Algorithm for Almost-sure Reachability with Small Strategies in POMDPs
Krishnendu Chatterjee, Martin Chmelik, Jessica Davies
POMDPs are standard models for probabilistic planning problems, where an agent interacts with an uncertain environment. We study the problem of almost-sure reachability, where give…
Counterexample Explanation by Learning Small Strategies in Markov Decision Processes
Tomáš Brázdil, Krishnendu Chatterjee, Martin Chmelík +2
While for deterministic systems, a counterexample to a property can simply be an error trace, counterexamples in probabilistic systems are necessarily more complex. For instance, a…
Optimal Cost Almost-sure Reachability in POMDPs
Krishnendu Chatterjee, Martin Chmelík, Raghav Gupta +1
We consider partially observable Markov decision processes (POMDPs) with a set of target states and every transition is associated with an integer cost. The optimization objective…
Temporal Logic Control for Stochastic Linear Systems using Abstraction Refinement of Probabilistic Games
Maria Svorenova, Jan Kretinsky, Martin Chmelik +3
We consider the problem of computing the set of initial states of a dynamical system such that there exists a control strategy to ensure that the trajectories satisfy a temporal lo…
Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications
Krishnendu Chatterjee, Martin Chmelík, Raghav Gupta +1
We consider partially observable Markov decision processes (POMDPs), that are a standard framework for robotics applications to model uncertainties present in the real world, with…
POMDPs under Probabilistic Semantics
Krishnendu Chatterjee, Martin Chmelik
We consider partially observable Markov decision processes (POMDPs) with limit-average payoff, where a reward value in the interval [0,1] is associated to every transition, and the…
CEGAR for Qualitative Analysis of Probabilistic Systems
Krishnendu Chatterjee, Martin Chmelik, Przemyslaw Daca
We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems. We focus on qualitative properties for MDPs that can express that desired behavio…
Verification of Markov Decision Processes using Learning Algorithms
Tomáš Brázdil, Krishnendu Chatterjee, Martin Chmelík +5
We present a general framework for applying machine-learning algorithms to the verification of Markov decision processes (MDPs). The primary goal of these techniques is to improve…
What is Decidable about Partially Observable Markov Decision Processes with ω-Regular Objectives
Krishnendu Chatterjee, Martin Chmelik, Mathieu Tracol
We consider partially observable Markov decision processes (POMDPs) with ω-regular conditions specified as parity objectives. The class of ω-regular languages extends regular langu…
POMDPs under Probabilistic Semantics
Krishnendu Chatterjee, Martin Chmelík
We consider partially observable Markov decision processes (POMDPs) with limit-average payoff, where a reward value in the interval [0,1] is associated to every transition, and the…
Interface Simulation Distances
Pavol Černý, Martin Chmelík, Thomas A. Henzinger +1
The classical (boolean) notion of refinement for behavioral interfaces of system components is the alternating refinement preorder. In this paper, we define a distance for interfac…
Controllable-choice Message Sequence Graphs
Martin Chmelík, Vojtěch Řehák
We focus on the realizability problem of Message Sequence Graphs (MSG), i.e. the problem whether a given MSG specification is correctly distributable among parallel components comm…
Equivalence of Games with Probabilistic Uncertainty and Partial-observation Games
Krishnendu Chatterjee, Martin Chmelik, Rupak Majumdar
We introduce games with probabilistic uncertainty, a natural model for controller synthesis in which the controller observes the state of the system through imprecise sensors that…