Source-linked AI summary
A Learning Based Approach to Control Synthesis of Markov Decision Processes for Linear Temporal Logic Specifications
Dorsa Sadigh, Eric S. Kim, Samuel Coogan, S. Shankar Sastry, Sanjit A. Seshia
TL;DR
The paper addresses control synthesis for MDPs with rich LTL specifications, including practical settings with partially specified transition probabilities. It combines a Rabin-weighted product MDP with reinforcement learning and proves probability-one satisfaction when such a policy exists, while obtaining reasonable strategies in cases where it does not.
Problem
The paper studies how to synthesize MDP control policies satisfying rich LTL properties, including settings with unspecified transition probabilities.
Method
The method applies modified active temporal-difference reinforcement learning to a product MDP whose persistent variables include transition frequencies, state utilities, and an optimal policy.
Results
The method is guaranteed to find a probability-one satisfying policy when one exists and produced reasonable strategies in grid-world and traffic-network case studies.
Takeaways & Limitations
The approach supports LTL control synthesis without requiring transition probabilities to be known a priori and empirically handles cases lacking a probability-one satisfying policy.
Takeaways & Limitations
The paper leaves theoretical guarantees open for cases where the LTL specification cannot be satisfied with probability one, including whether suitable reward weightings maximize satisfaction probability.
Abstract
from arXiv · showhide
We propose to synthesize a control policy for a Markov decision process (MDP) such that the resulting traces of the MDP satisfy a linear temporal logic (LTL) property. We construct a product MDP that incorporates a deterministic Rabin automaton generated from the desired LTL property. The reward function of the product MDP is defined from the acceptance condition of the Rabin automaton. This construction allows us to apply techniques from learning theory to the problem of synthesis for LTL specifications even when the transition probabilities are not known a priori. We prove that our method is guaranteed to find a controller that satisfies the LTL property with probability one if such a policy exists, and we suggest empirically with a case study in traffic control that our method produces reasonable control strategies even when the LTL property cannot be satisfied with probability one.
I. INTRODUCTION
The paper targets LTL control synthesis for MDPs, including settings with partially specified transition probabilities. It combines a Rabin-automaton product construction with learning-based optimization and reports guarantees plus case studies.
- LTL expresses rich MDP control objectives including stability, surveillance, response, safety, and liveness.
- The approach constructs a product MDP pairing original-system states with deterministic Rabin automaton states for the desired specification.
- A reward function derived from the Rabin acceptance condition supports expected-utility optimization over the product MDP.
- Reinforcement learning optimizes the Rabin-weighted product MDP and can operate when transition probabilities are not known a priori.
- The method is guaranteed to find a probability-one satisfying controller when one exists, while case studies examine grid-world and traffic-network control.
II. PRELIMINARIES
The preliminaries define LTL operators and Rabin automata, then introduce labeled MDPs as the probabilistic systems to be controlled. A DRA accepts exactly the words satisfying a given LTL formula.
- LTL formulas use atomic propositions, Boolean operators, and temporal operators to specify system behavior.
- G, F, X, and U express truth at all future moments, some future moment, the next moment, and until another formula becomes true.
- Surveillance and stability can be represented by the LTL patterns GFφ and FGφ, respectively.
- A deterministic Rabin automaton consists of states, an input alphabet, a transition function, an initial state, and a Rabin acceptance condition.
- For any LTL formula φ, a DRA can be constructed that accepts exactly the words over atomic propositions satisfying φ.
- A labeled MDP specifies finite states, available actions, transition probabilities, an initial state, atomic propositions, and a state-labeling function.
A. Problem Formulation
The problem formulation composes a labeled MDP with a DRA for the LTL specification, producing a Rabin-weighted product MDP. Policies maximize discounted utility under acceptance-pair rewards, yielding a probability-one satisfying policy when such a policy exists.
- Problem objective: The synthesis objective is to find a policy whose MDP traces satisfy an LTL formula φ with probability one.
- Product construction: The product MDP augments each MDP state with a DRA state, while retaining the original MDP actions.
- Policies: A stationary product-MDP policy maps every product state to an action and corresponds to a finite-memory policy for the original MDP.
- Reward design: Rewards assign positive weight to Gi, negative weight to Bi, and zero weight to neutral states, biasing policies toward the Rabin acceptance condition.
- Optimization: The algorithm optimizes expected discounted utility for each Rabin acceptance pair and analyzes the resulting policies for probability-one satisfaction.
- Guarantee: If a probability-one satisfying policy exists, suitable discount and negative-reward parameters ensure that utility optimization finds such a policy.
- Learning setting: When transition probabilities are unknown, optimization must simultaneously learn system dynamics and expected utility.
B. Synthesis through Reinforcement Learning
The approach translates LTL synthesis into expected-reward maximization on a Rabin-weighted product MDP, enabling reinforcement learning when transition probabilities are unknown. The modified temporal-difference algorithm exploits shared transition structure and uses resets to support convergence in the case studies.
- Standard reinforcement-learning techniques can find satisfying control policies after LTL synthesis is translated into expected reward maximization.
- The method learns transition probabilities and optimizes product-MDP utility using a modified active temporal-difference algorithm updated after each observed transition.Persistent variables include transition frequencies, state utilities, and the optimal policy.
- Each product-MDP state shares transition structure with states having the same labeled MDP state, so one observation updates estimates across an equivalence class.The equivalence classes are formed from an MDP state paired with all Rabin states.
- Rabin-state resets occur after safety violations or heuristically when liveness is not being achieved, ensuring a correct control action for every state.The authors observed convergence to a satisfying policy in both case studies with this reset technique.
- The resulting policy can be constructed online while learning unknown transition probabilities, but general online MDP learning lacks hard optimal-policy convergence guarantees because of exploration versus exploitation.
A. Control of an agent in a grid world
In a 5 × 5 probabilistic grid world, the method controls an agent required to visit regions A and B infinitely often while avoiding region C. Although no policy satisfies the specification on every run, one satisfies it with probability 1.
- The grid-world task requires infinitely often visiting regions A and B while avoiding region C.
- No policy satisfies the specification for all runs, because every action could possibly result in no movement.
- A policy nevertheless exists that satisfies the specification with probability 1, placing this example within the theorem’s guaranteed case.
B. Control of a Traffic Network with Two Intersections
The traffic case study models two signalized intersections as a discrete probabilistic MDP and synthesizes policies for queue, supply, and minimum-green-time objectives. Reinforcement learning improves an approximate controller so it empirically often satisfies the LTL specification under true traffic dynamics.
- The traffic network has two signalized intersections, with each signal choosing between actuating its associated east-west or north-south link every 15 seconds.
- Queues are modeled through downstream space, saturation limits, and turn ratios that distribute forwarded vehicles among downstream links.
- Continuous queue capacities are discretized into finite subintervals, producing a probabilistic MDP whose state also records the last control action.The example contains 320 total discrete states.
- The control objective requires links 1 and 2 eventually to remain below 30 vehicles, links 3 and 4 to fall below 10 vehicles infinitely often, and a three-step signal constraint.The minimum-green-time condition requires signal 2 to remain red for at least three consecutive time steps after switching from green to red.
- A naive policy fails because x2 remains above 30 vehicles, while an approximate-model controller greatly improves performance but still fails to satisfy the specification.
- Reinforcement learning modifies the approximate controller using true traffic dynamics, yielding a controller that empirically often satisfies the specification.The paper does not expect satisfaction for all traces or disturbance inputs when such a controller may not exist.
V. CONCLUSION
The paper presents an LTL-based MDP control-synthesis method with case studies in grid-world and traffic control. It proves probability-one satisfaction when such a controller exists, while leaving guarantees for the non-probability-one case as future work.
- The proposed method synthesizes MDP control policies whose traces satisfy an LTL control objective.
- The method is guaranteed to return a controller satisfying the LTL formula with probability one if such a controller exists.
- Two case studies apply the method to a virtual grid-world agent and a traffic signal controller for a small network with two intersections.
- Future work must establish theoretical guarantees when the LTL specification cannot be satisfied with probability one.
A. Proof of Theorem 1
The proof shows that, with suitable discount and reward parameters, an optimal policy for the product MDP must satisfy the Rabin acceptance condition and therefore the LTL specification with probability one.
- Conclusion: Because the two case conditions can be satisfied simultaneously, no optimal policy can violate the acceptance condition; an optimal policy must visit Gi infinitely often and Bi only finitely often.The construction selects γ and wB to satisfy the combined inequalities, yielding satisfaction with probability one.
- Case analysis: The proof partitions policies that fail the specification into two cases based on recurrent classes and the resulting visits to accepting or rejecting Rabin sets.Case 1 concerns recurrent classes that exclude Gi; Case 2 concerns recurrent classes containing a state in Bi.
- Case 1: For policies violating Case 1, recurrent classes with no Gi states receive non-positive rewards, making their utility lower than that of a satisfying policy.The proof establishes Uπ∗(s) < Uπ̄(s), contradicting optimality.
- Utility bounds: Choosing γ sufficiently close to 1 makes repeated visits to Gi dominate utility from transient states, while negative wB penalizes recurrent visits to Bi.The proof uses bounds on transient-state returns and recurrent-class utilities to establish the required inequalities.
- Case 2: For policies violating Case 2, a state in Bi is recurrent under the candidate policy but transient under a satisfying policy, and parameter selection again contradicts optimality.The argument derives utility bounds and selects γ and wB so all such policies fail the optimality condition.