Synthesis of Discounted-Reward Optimal Policies for Markov Decision\n Processes Under Linear Temporal Logic Specifications

2020/11/01 by Krishna C. Kalagarla, Rahul Jain, Kalagarla, Krishna C. +3
Computer Science · #Formal Methods in Verification #Advanced Software Engineering Methodologies #AI-based Problem Solving and Planning

paper · pdf · doi:10.48550/arxiv.2011.00632

Abstract

We present a method to find an optimal policy with respect to a reward\nfunction for a discounted Markov decision process under general linear temporal\nlogic (LTL) specifications. Previous work has either focused on maximizing a\ncumulative reward objective under finite-duration tasks, specified by\nsyntactically co-safe LTL, or maximizing an average reward for persistent\n(e.g., surveillance) tasks. This paper extends and generalizes these results by\nintroducing a pair of occupancy measures to express the LTL satisfaction\nobjective and the expected discounted reward objective, respectively. These\noccupancy measures are then connected to a single policy via a novel reduction\nresulting in a mixed integer linear program whose solution provides an optimal\npolicy. Our formulation can also be extended to include additional constraints\nwith respect to secondary reward functions. We illustrate the effectiveness of\nour approach in the context of robotic motion planning for complex missions\nunder uncertainty and performance objectives.\n

Related

• Optimal Control of Markov Decision Processes for Efficiency with Linear Temporal Logic Tasks
• Policy Synthesis and Reinforcement Learning for Discounted LTL
• MDP Optimal Control under Temporal Logic Constraints
• Control Synthesis from Linear Temporal Logic Specifications using\n Model-Free Reinforcement Learning
• Synthesis from Satisficing and Temporal Goals