Entropy Objectives in Markov Decision Processes
For researchers in formal methods and control, this provides a first method for entropy objectives in MDPs, though the approach is preliminary and incremental.
The paper tackles the problem of synthesizing control policies to enforce entropy-based concentration properties on state distributions in Markov Decision Processes. It proves the problem is hard, then presents a sound and conditionally complete method using convex duality and invariant synthesis, with empirical validation.
We consider the problem of synthesizing control policies that enforce a concentration property on the state distributions of a stochastic system. We present a formalization of this problem in terms of synthesizing strategies for maintaining an entropy-based objective in Markov Decision Processes (MDPs). We first show that even relaxed versions of this problem are complexity-theoretically hard. We then present a sound and (conditionally) relatively complete method to verify and synthesize strategies for such entropy objectives. The main challenge is the non-linear nature of such objectives, and our approach addresses this by exploiting and combining ideas from convex duality and invariant synthesis. We also investigate the role of memory and randomization in ensuring entropy objectives. Finally, we implement our ideas to evaluate our approach empirically on a few illustrative benchmarks.