Optimal Constrained sc-LTL Planning in MDPs via Switching Policies

This paper studies optimal policy synthesis for Markov decision processes with objectives and safety constraints expressed in co-safe linear temporal logic (sc-LTL). Because sc-LTL specifications make the problem non-Markovian, the authors reduce it to constrained reachability on an extended model. They show that switching policies assembled from stationary policies for the individual sc-LTL specifications are sufficient for optimality. This leads to a tractable linear program for computing the policy. A grid-world case study reports an optimal trade-off between the objective and safety constraint, supporting the proposed method’s optimality and tractability.