📝 SummarXiv

Abstract

We investigate the problem of optimal control synthesis for Markov Decision Processes (MDPs), addressing both qualitative and quantitative objectives. Specifically, we require the system to satisfy a qualitative task specified by a Linear Temporal Logic (LTL) formula with probability one. Additionally, to quantify the system's performance, we introduce the concept of efficiency, defined as the ratio between rewards and costs. This measure is more general than the standard long-run average reward metric, as it seeks to maximize the reward obtained per unit cost. Our objective is to synthesize a control policy that not only ensures the LTL task is satisfied but also maximizes efficiency. We present an effective approach for synthesizing a stationary control policy that achieves $\epsilon$-optimality by integrating state classifications of MDPs with perturbation analysis in a novel manner. Our results extend existing work on efficiency-optimal control synthesis for MDPs by incorporating qualitative LTL tasks. Case studies in robot task planning are provided to illustrate the proposed algorithm.