PaperlayerView exact revision on arXiv

Source-linked AI summary

Probably Approximately Correct MDP Learning and Control With Temporal Logic Constraints

Jie Fu, Ufuk Topcu

arXiv:1404.7073v2eess.SYcs.LGcs.LOcs.RO

TL;DR

The paper addresses temporal-logic control synthesis when an MDP’s transition probabilities are initially unknown. It extends model-based PAC-MDP learning by maintaining a learned model and product MDP, updating policies from observations. The resulting policy is approximately optimal with high probability and polynomial sample, time, and space complexity, subject to the stated finite-horizon setting.

  • Problem

    The paper asks how to maximize temporal-logic satisfaction probability when the underlying stochastic MDP has unknown transition probabilities.

  • Method

    The method learns an MDP model online, constructs a product MDP with the specification automaton, and iteratively updates the control policy using observed transitions.

  • Results

    The algorithm yields an approximately optimal policy with probability 1 −δ using polynomial sample, time, and space complexity in the MDP, automaton, accuracy, confidence, and finite horizon.

  • Takeaways & Limitations

    Learning and control can be integrated for temporal-logic-constrained synthesis in unknown MDPs while balancing exploration and exploitation without i.i.d. samples.

  • Takeaways & Limitations

    The current work considers one-player stochastic games; extending the approach to two-player games may require additional strategy classes and synthesis methods.

Abstract

from arXiv · show

We consider synthesis of control policies that maximize the probability of satisfying given temporal logic specifications in unknown, stochastic environments. We model the interaction between the system and its environment as a Markov decision process (MDP) with initially unknown transition probabilities. The solution we develop builds on the so-called model-based probably approximately correct Markov decision process (PAC-MDP) methodology. The algorithm attains an $\varepsilon$-approximately optimal policy with probability $1-δ$ using samples (i.e. observations), time and space that grow polynomially with the size of the MDP, the size of the automaton expressing the temporal logic specification, $\frac{1}{\varepsilon}$, $\frac{1}δ$ and a finite time horizon. In this approach, the system maintains a model of the initially unknown MDP, and constructs a product MDP based on its learned model and the specification automaton that expresses the temporal logic constraints. During execution, the policy is iteratively updated using observation of the transitions taken by the system. The iteration terminates in finitely many steps. With high probability, the resulting policy is such that, for any state, the difference between the probability of satisfying the specification under this policy and the optimal one is within a predefined bound.

I. INTRODUCTION

The paper extends model-based PAC-MDP reinforcement learning to control synthesis under temporal logic constraints in unknown, stochastic MDPs. It combines learned models, product constructions, and iterative policy updates to obtain approximately optimal policies efficiently.

  • Approach: The proposed method extends model-based PAC-MDP reinforcement learning to maximize temporal-logic satisfaction probability.The agent maintains an observation-based MDP model and updates its controller as learning proceeds.
  • Motivation: Unknown stochastic environments can be modeled as MDPs with transition probabilities learned from observations.Finite samples can approximate the true MDP while supporting reasoning about policy optimality and temporal-logic correctness.
  • Guarantees: The method converges efficiently within a finite horizon without requiring independently and identically distributed samples.The number of policy updates depends on the underlying MDP size and is independent of the specification.
  • Temporal logic: LTL specifications express desired properties including safety, liveness, persistence, and stability.Each LTL formula can be represented by a deterministic Rabin automaton for synthesis.
  • Product synthesis: The product MDP combines system states with specification-automaton states and lifts the automaton acceptance condition into the product.This construction allows temporal-logic satisfaction to be treated as a quantitative control objective.
  • Policy representation: Memoryless deterministic policies in the product MDP correspond to finite-memory policies in the underlying MDP and suffice for one-player stochastic games.The automaton state serves as memory when translating the product policy back to the original system.

C. Problem statement

The problem is to learn an unknown MDP online while synthesizing a policy that maximizes finite-horizon temporal-logic satisfaction probability. The paper seeks high-probability near-optimality with polynomial learning and computation complexity.

  • Problem setting: Known-MDP synthesis methods cannot directly produce optimal temporal-logic policies when transition probabilities are unavailable.The motivating example is robotic motion planning in unknown terrain.
  • Problem setting: The system learns the true MDP online and iteratively updates the synthesized policy using the accumulated model knowledge.This integrates exploration with control during execution.
  • Objective: The state value is the probability of satisfying the specification from a product-MDP state onward, while the optimal policy maximizes this value for each state.Satisfaction probability equals the probability of entering the accepting end-state set.
  • Objective: The T-step state value measures specification-satisfaction probability over a finite horizon, and the optimal T-step policy maximizes that value.The state-value formulation is also expressible as expected accumulated reward for entering accepting end states.
  • Formal goal: With probability at least 1 −δ, the algorithm must output an ε-close policy while using polynomial sample, space, and time complexity.The target guarantee is required for every product-MDP state over the finite horizon T.

III. MAIN RESULT

The method partitions states by whether they are sufficiently known, then plans over a learned product MDP with an absorbing sink for unknown states. Once all states become known, the learned product MDP matches the true accepting end components and yields a near-optimal policy with high probability.

  • III. MAIN RESULT: States become known after sufficiently many visits determined by δ, ε, MDP size, and finite horizon T.The approach assumes full observations of state and action spaces.
  • III. MAIN RESULT: The learned product MDP retains known states and aggregates unknown states into an additional absorbing sink.The known product uses the state set H × S, where H is the set of known MDP states.
  • III. MAIN RESULT: In T steps, the policy either reaches accepting end states with high probability or explores an unknown state that can later become known.This mechanism supports iterative policy improvement through exploration and control.
  • III. MAIN RESULT: Once all states are known, the learned and true product MDPs have identical accepting end components, and the learned policy is near optimal with probability at least 1 −δ.Near optimality compares finite-horizon satisfaction probability with the eventual satisfaction probability of the optimal policy, up to a small quantity.
  • III. MAIN RESULT: Figure 1 illustrates an eight-state MDP with two actions and transition probabilities specified by P.The figure defines Q = {q_i, i = 0, . . . , 7} and Σ = {α, β}.

B. Maximum likelihood estimation of transition probabilities

The paper models transition uncertainty with independent Dirichlet distributions and updates transition-count beliefs from observed transitions. Approximation and simulation results relate learned-model accuracy to finite-horizon product-MDP values, while the specification automaton does not affect the required model accuracy for a fixed horizon.

  • B. Maximum likelihood estimation of transition probabilities: Each state-action transition distribution is assumed to follow an independent Dirichlet distribution.The distribution Dist(q, a) assigns probabilities P(q, a, q′) to successor states.
  • B. Maximum likelihood estimation of transition probabilities: The belief vector records transition observations and increments the corresponding count after each observed transition.For a transition (q1, σ, q2), the associated count is updated by one.
  • C. Approximating the underlying MDP: An α-approximation preserves the labeled MDP’s state-action structure and labeling while bounding corresponding transition-probability differences.The product construction preserves this approximation relation between the underlying and specification-constrained MDPs.
  • C. Approximating the underlying MDP: For an ϵ/(NT)-approximation, the simulation lemma bounds T-step state-value differences for any policy in the product MDP.The bound applies for any specification automaton and any product state.
  • C. Approximating the underlying MDP: The confidence level for the final T-step value bound is not obtained by simply raising the per-transition confidence level to the Tth power.The paper refers to the proof for the precise confidence calculation.
  • C. Approximating the underlying MDP: For fixed finite horizon T, the specification automaton size does not affect the learned-model accuracy required for an ϵ-close T-step state value.The specification can still influence the choice of T through the state-value mixing time.

D. Exploration and exploitation

The algorithm alternates exploitation of a T-step optimal policy with exploration of insufficiently known states in a known product MDP. A key lemma guarantees that the policy is either near-optimal or reaches an unknown non-accepting state with substantial probability.

  • Exploration and exploitation: The system exercises a T-step optimal policy in an MDP built from its current set of known states.This implicitly balances exploitation of the current model with exploration of states whose transition knowledge is insufficient.
  • Known-state criterion: Known-state transitions are defined through a confidence requirement based on the variance of the maximum-likelihood estimator and a 1−δ confidence interval.The threshold uses the ε-state-value mixing time T and the number of underlying MDP states.
  • Known product MDP: Known states in the product MDP retain their original transitions, while transitions from known states toward unknown states are aggregated into an absorbing sink.The known product MDP also assigns an acceptance condition involving the sink to encourage exploration.
  • Exploration guarantee: If the T-step policy is not within α of the optimal T-step value, it visits an unknown non-accepting state within T steps with probability at least α.Thus, a policy that is not near-optimal generates informative exploration rather than merely exploiting an inaccurate model.
  • Exploration guarantee: Unknown accepting states can be revisited through their accepting end components until they become known.This handles unknown states that lie in accepting end components rather than the non-accepting states covered directly by the lemma.

IV. PAC-MDP ALGORITHM IN CONTROL WITH TEMPORAL LOGIC CONSTRAINTS.

The PAC-MDP algorithm learns an unknown MDP, constructs a known product MDP with the temporal-logic automaton, and repeatedly synthesizes a T-step policy. With probability at least 1−δ, it returns a policy whose state values are within the specified approximation and whose resource requirements are polynomial.

  • Guarantee: With probability no less than 1−δ, Algorithm 1 returns a policy in the class with ε-state-value mixing time T satisfying the theorem’s approximation guarantee.The theorem applies to an MDP with unknown transition probabilities and an LTL specification represented by a product MDP.
  • Learning and policy updates: Before all states are known, the current policy is T-step optimal in the known product MDP and either achieves a near-optimal value or explores efficiently.The learned product MDP is an ε/(N T)-approximation, producing a combined (2ε+α) value bound in the lemma-based argument.
  • Guarantee: After all states become known, the learned MDP approximates the true MDP and the resulting policy is near-optimal with probability at least 1−δ.The proof connects model accuracy, the mixing-time choice, and the final T-step policy guarantee.
  • Complexity: The sample complexity is polynomial in |Q|, |Σ|, T, and 1/δ, independently of the specification automaton size.Policy-synthesis time and space are polynomial in |Q|, |S|, |Σ|, T, and 1/δ.
  • Complexity: The policy is updated at most |Q| times, because observations that do not make a state known do not require recomputation.The input mixing time T can also be removed by estimating an upper bound or increasing T iteratively.
  • Exploration mechanism: When an action appears self-looping, the algorithm either continues exploring the state or restarts from a random initial state with probability p.This addresses the possibility that an unobserved outgoing transition has not yet been discovered.

V. EXAMPLES

The paper evaluates Algorithm 1 on a running example and a robotic motion-planning problem in unknown terrain, using Python implementations on a desktop computer.

  • Experimental setup: Algorithm 1 is applied to the running example MDP and to robotic motion planning in an unknown terrain.The implementations use Python and run on a desktop with an Intel Core processor and 16 GB of memory.

A. The running example

The running example evaluates policy learning under several accuracy parameters and illustrates finite termination, policy recomputation, and convergence of state values. Tighter accuracy requirements require more exploration, while the reported maximal error remains below the chosen bound.

  • The running example: For ε=0.01, all states become known after 274968 steps, and policy updates terminate after 8 updates in 35.12 seconds.The experiment uses δ=0.05 and T=15.
  • The running example: For ε=0.01, the policy has converged to the optimal policy by step 204468, before the learned model’s T-step value becomes ε-close at step 274968.The distinction separates policy convergence from convergence of the hypothesis-based value estimate.
  • The running example: For ε=0.02, all states become known in 136403 steps and 17.73 seconds, and the resulting policy is optimal.This setting is one of the tested assignments with δ=0.05 and T=15.
  • The running example: For ε=0.05, all states become known in 55321 steps and 7.18 seconds, but the learned policy is sub-optimal at q0 with state value 0.22 versus 0.22445 optimally.The learned policy chooses α at q0, whereas the optimal policy chooses β at both q0 and q5.
  • The running example: Across three experiments, the actual maximal error is 0.00445 for ε=0.05 and never exceeds 0.01.The paper attributes this to using a loose error upper bound to guarantee correctness.

B. A motion planning example

The motion-planning experiment evaluates iterative policy updates for a robot navigating unknown terrains under a temporal-logic surveillance and safety specification. With ε = 0.01, δ = 0.05, and T = 50, the learned policy is reported as optimal in the true MDP.

  • Environment: The robot operates across four unknown terrains—pavement, grass, gravel, and sand—with terrain- and action-dependent transition probabilities.The available correct-cell probability ranges include [0.9, 0.95] for pavement and [0.85, 0.9] for grass.
  • Specification: The objective is to maximize the probability of satisfying ϕ = □♦(R1 ∧♦(R2 ∧♦R3)) ∧□¬R4.R1, R2, and R3 are critical surveillance cells, while R4 denotes unsafe cells to avoid.
  • Evaluation: The experiment evaluates policies iteratively from initial robot locations in a marked subset of cells labeled 1, 2, 3, and 4.The policy is updated as the robot learns about the unknown terrains.
  • Results: 155089 steps and 1593.45 seconds were required for all states to become known, with four policy updates corresponding to the four terrain types.The reported settings are ε = 0.01, δ = 0.05, and T = 50.
  • Results: The policy output by Algorithm 1 is the optimal policy in the true MDP for the evaluated initial states.The plotted value function is evaluated for q0 ∈ {1, 2, 3, 4} over the finite horizon.

VI. CONCLUSION AND FUTURE WORK

The paper concludes that PAC-MDP learning can integrate model learning and control for temporal-logic-constrained synthesis in unknown MDPs. It reports approximately optimal policies with polynomial resource complexity and identifies extensions to richer games, objectives, and model-free learning.

  • Conclusion: The proposed PAC-MDP method integrates learning and control to synthesize approximately optimal policies for temporal-logic constraints in unknown MDPs.The method is presented as a synthesis approach for unknown stochastic systems.
  • Conclusion: Time, space, and sample complexity grow polynomially for the temporal-logic-constrained synthesis algorithm.The conclusion states this complexity result at the paper level.
  • Future Work: Future work includes multi-vehicle motion planning, comparison with alternative methods, and removing the need to provide the finite horizon T.The proposed implementation change follows the cited PAC-MDP direction in.
  • Future Work: The approach could be extended from one-player stochastic games to two-player stochastic games, where deterministic memoryless policies may be insufficient.Different deterministic, randomized, memoryless, and finite-memory strategy classes may require different synthesis methods.
  • Future Work: Other possible objectives include minimizing weighted average costs in addition to maximizing temporal-logic satisfaction probability.This is identified as a possible extension of the objective.

APPENDIX

The appendix analyzes how errors in the learned MDP affect finite-horizon satisfaction values in the product MDP. It compares intermediate models whose transition probabilities switch from the learned model to the true model and bounds the resulting differences.

  • Proof Setup: The learned and true product MDPs share the same structure and accepting end states under the specification automaton.This provides the structural basis for comparing their induced Markov chains.
  • Proof Setup: For any policy, intermediate Markov chains use learned-model transitions for the first i steps and true-model transitions thereafter.The endpoint chains are the fully learned model at i = 0 and the true model at i = T.
  • Proof Argument: The proof tracks path probabilities and finite-horizon hitting values while changing one transition layer at a time.For the first i and final T − i − 1 transitions, the relevant probabilities agree with the endpoint chains.
  • Proof Argument: A transition from product state v′ to v′′ uses the underlying MDP transition P(q′, a, q′′), with the automaton successor determined by s′ and the next state label.This separates the MDP transition approximation from the automaton update in the product construction.
  • Bound: The difference term is bounded by εT because path probabilities sum to at most one and the number of possible underlying successor states is N.The appendix states Diff1 ≤ Diff2 ≤ ε/(NT) · N = ε/T.
Loading 1404.7073v2…