Author name cluster

Martin Chmelík

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

6 papers

1 author row

AAAI Conference 2016 Conference Paper

A Symbolic SAT-Based Algorithm for Almost-Sure Reachability with Small Strategies in POMDPs

Krishnendu Chatterjee
Martin Chmelík
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 given a set of target states, the question is to decide whether there is a policy to ensure that the target set is reached with probability 1 (almost-surely). While in general the problem is EXPTIMEcomplete, in many practical cases policies with a small amount of memory sufﬁce. Moreover, the existing solution to the problem is explicit, which ﬁrst requires to construct explicitly an exponential reduction to a belief-support MDP. In this work, we ﬁrst study the existence of observation-stationary strategies, which is NP-complete, and then small-memory strategies. We present a symbolic algorithm by an efﬁcient encoding to SAT and using a SAT solver for the problem. We report experimental results demonstrating the scalability of our symbolic (SAT-based) approach.

PDF Details

AIJ Journal 2016 Journal Article

Optimal cost almost-sure reachability in POMDPs

Krishnendu Chatterjee
Martin Chmelík
Raghav Gupta
Ayush Kanodia

We consider partially observable Markov decision processes (POMDPs) with a set of target states and an integer cost associated with every transition. The optimization objective we study asks to minimize the expected total cost of reaching a state in the target set, while ensuring that the target set is reached almost surely (with probability 1). We show that for integer costs approximating the optimal cost is undecidable. For positive costs, our results are as follows: (i) we establish matching lower and upper bounds for the optimal cost, both double exponential in the POMDP state space size; (ii) we show that the problem of approximating the optimal cost is decidable and present approximation algorithms developing on the existing algorithms for POMDPs with finite-horizon objectives. While the worst-case running time of our algorithm is double exponential, we also present efficient stopping criteria for the algorithm and show experimentally that it performs well in many examples of interest.

Details DOI

AAMAS Conference 2016 Conference Paper

Stochastic Shortest Path with Energy Constraints in Pomdps (Extended Abstract)

Tomáš Brázdil
Krishnendu Chatterjee
Martin Chmelík
Anchit Gupta
Petr Novotný

We extend the traditional framework of POMDPs to model resource consumption inducing a hard constraint on the behaviour of the model. Resource levels increase and decrease with transitions, and the hard constraint requires that the level remains positive in all steps. We present an algorithm for solving POMDPs with resource levels, developing on existing POMDP solvers. Our second contribution is related to policy representation. For larger POMDPs the policies computed by existing solvers are too large to be understandable, an issue particularly pronounced in POMDPs with resource levels. We present a procedure based on machine learning techniques that extracts important decisions of a policy and outputs its readable representation.

PDF

AIJ Journal 2015 Journal Article

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 with every transition, and the payoff of an infinite path is the long-run average of the rewards. We consider two types of path constraints: (i) a quantitative constraint defines the set of paths where the payoff is at least a given threshold λ 1 ∈ ( 0, 1 ]; and (ii) a qualitative constraint which is a special case of the quantitative constraint with λ 1 = 1. We consider the computation of the almost-sure winning set, where the controller needs to ensure that the path constraint is satisfied with probability 1. Our main results for qualitative path constraints are as follows: (i) the problem of deciding the existence of a finite-memory controller is EXPTIME-complete; and (ii) the problem of deciding the existence of an infinite-memory controller is undecidable. For quantitative path constraints we show that the problem of deciding the existence of a finite-memory controller is undecidable. We also present a prototype implementation of our EXPTIME algorithm and experimental results on several examples.

Details DOI

TCS Journal 2014 Journal Article

Interface simulation distances

Pavol Černý
Martin Chmelík
Thomas A. Henzinger
Arjun Radhakrishna

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 interfaces, called interface simulation distance. It makes the alternating refinement preorder quantitative by, intuitively, tolerating errors (while counting them) in the alternating simulation game. We show that the interface simulation distance satisfies the triangle inequality, that the distance between two interfaces does not increase under parallel composition with a third interface, that the distance between two interfaces can be bounded from above and below by distances between abstractions of the two interfaces, and how to synthesize an interface from incompatible requirements. We illustrate the framework, and the properties of the distances under composition of interfaces, with two case studies.

Details DOI

GandALF Workshop 2012 Workshop Paper

Interface Simulation Distances

Pavol Černý
Martin Chmelík
Thomas A. Henzinger
Arjun Radhakrishna

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 interfaces, called interface simulation distance. It makes the alternating refinement preorder quantitative by, intuitively, tolerating errors (while counting them) in the alternating simulation game. We show that the interface simulation distance satisfies the triangle inequality, that the distance between two interfaces does not increase under parallel composition with a third interface, and that the distance between two interfaces can be bounded from above and below by distances between abstractions of the two interfaces. We illustrate the framework, and the properties of the distances under composition of interfaces, with two case studies.

PDF Details DOI