PaperlayerView exact revision on arXiv

Source-linked AI summary

Control Synthesis from Linear Temporal Logic Specifications using Model-Free Reinforcement Learning

Alper Kamil Bozkurt, Yu Wang, Michael M. Zavlanos, Miroslav Pajic

arXiv:1909.07299v2cs.ROcs.AIcs.LG

TL;DR

The paper tackles LTL control synthesis when an MDP’s transition probabilities are unknown and seeks policies maximizing specification satisfaction without learning a model. It converts LTL satisfaction to a Büchi objective on a product MDP, then uses LTL-based rewards and path-dependent discounting in model-free RL. The resulting policy optimizes satisfaction probability, with convergence guaranteed under the proposed discounting, and the approach is demonstrated in motion-planning case studies.

  • Problem

    The problem is to maximize the probability of satisfying an LTL specification in an MDP with completely unknown transition probabilities, without constructing the MDP model.

  • Method

    The method converts LTL satisfaction into a Büchi objective on an LDBA-product MDP and applies accepting-state rewards with path-dependent discounting in model-free RL.

  • Results

    The optimal policy for the discounted reward maximizes the LTL satisfaction probability, and the model-free learning procedure is guaranteed to converge to such a policy.

  • Takeaways & Limitations

    The framework provides model-free LTL policy synthesis for unknown stochastic environments and is illustrated on mobile-robot motion-planning case studies.

Abstract

from arXiv · show

We present a reinforcement learning (RL) framework to synthesize a control policy from a given linear temporal logic (LTL) specification in an unknown stochastic environment that can be modeled as a Markov Decision Process (MDP). Specifically, we learn a policy that maximizes the probability of satisfying the LTL formula without learning the transition probabilities. We introduce a novel rewarding and path-dependent discounting mechanism based on the LTL formula such that (i) an optimal policy maximizing the total discounted reward effectively maximizes the probabilities of satisfying LTL objectives, and (ii) a model-free RL algorithm using these rewards and discount factors is guaranteed to converge to such policy. Finally, we illustrate the applicability of our RL-based synthesis approach on two motion planning case studies.

I. INTRODUCTION

The paper addresses LTL control synthesis in unknown stochastic environments, where model-based methods require learning and storing transition probabilities. It proposes model-free reinforcement learning with LTL-based rewards and discounting to maximize satisfaction probabilities.

  • Unknown MDP transition probabilities require learning control policies directly from samples rather than applying standard model-checking synthesis.
  • Model-based RL methods estimate transition probabilities but incur significant space requirements that restrict use in large or high-dimensional systems.
  • LTL tasks can be encoded through finite-memory rewards or automata accepting conditions so discounted reward optimization represents temporal-logic satisfaction.
  • Prior reward schemes based on Rabin or LDBA conditions may fail to produce policies satisfying LTL properties almost surely in rejecting or non-accepting components.
  • The paper develops a model-free RL algorithm and evaluates it on mobile-robot motion-planning problems.
  • The proposed method directly rewards accepting states and uses discounting so optimal values converge to maximal Büchi satisfaction probabilities for discount factors below 1.

A. Markov Decision Processes and Reinforcement Learning

This section introduces MDPs, policies, induced Markov chains, discounted returns, and the model-free RL objective. Model-free learning seeks an optimal policy without explicitly estimating transition probabilities.

  • An MDP models nondeterministic action choices with probabilistic outcomes.
  • A labeled MDP consists of states, actions, transition probabilities, an initial state, atomic propositions, and a labeling function.
  • A policy maps finite state histories to available actions, while a memoryless policy depends only on the current state.
  • A discounted K-step return accumulates rewards from a path using discount factor γ ∈ (0, 1).
  • RL seeks a policy maximizing expected return from samples, and model-free RL does so without explicitly estimating transition probabilities.

B. LTL and Limit-Deterministic B¨uchi Automata

LTL specifies temporal properties using Boolean and temporal operators, and satisfaction can be evaluated with an LDBA. An LDBA accepts paths whose accepting states are visited infinitely often.

  • LTL formulas are built from atomic propositions, Boolean operators, negation, next, and until.
  • A path satisfies ϕ1 U ϕ2 when it reaches ϕ2 at some position while satisfying ϕ1 at every earlier position.
  • Eventually and always operators are derived from until and negation, respectively.
  • An LTL formula can be translated into an LDBA for evaluating satisfaction on paths.
  • An LDBA has initial and accepting components, with deterministic alphabet transitions and no epsilon moves from the accepting component.
  • The LDBA Büchi condition requires that at least one accepting state be visited infinitely often.

C. Problem Statement

The problem is to synthesize a finite-memory policy maximizing the probability of satisfying an LTL specification in an MDP whose transition probabilities are completely unknown. The policy must be learned through direct interaction without constructing an MDP model.

  • The environment is modeled as an MDP with unknown transition probabilities, including unknown transition support.
  • The desired objective is an LTL formula, and the goal is to maximize its satisfaction probability.
  • Problem 1 asks for a model-free RL algorithm that finds a finite-memory objective policy achieving Prmax(s |= ϕ) for all states.

III. RL-BASED SYNTHESIS FROM LTL SPECIFICATIONS

The framework converts an LTL objective into a repeated-reachability Büchi objective on a product MDP, enabling model-free RL synthesis.

  • Any LTL formula is transformed into an LDBA, reducing satisfaction of ϕ in an MDP to the repeated-reachability objective □◇B on the product MDP.The LDBA has nondeterministic transitions only through ε-moves from its initial to accepting component.

A. Design of Product MDP

The product MDP composes the original MDP with an LDBA derived from the LTL formula, representing automaton ε-moves as actions and preserving the satisfaction objective. Policies maximizing the product's Büchi satisfaction probability induce finite-memory policies maximizing the original LTL satisfaction probability.

  • Product construction: The product MDP is constructed by composing M with an LDBA Aϕ over the alphabet 2^AP, which is automatically derived from ϕ.This composition supports quantitative analysis of LTL satisfaction in the MDP.
  • Product construction: Its state space is S × Q, its actions include environment actions and ε-actions, its initial state is ⟨s0,q0⟩, and accepting states have automaton components in B.A product path satisfies the Büchi condition when it visits accepting product states infinitely often.
  • Product dynamics: The nondeterministic ε-moves of the LDBA are represented as ε-actions in the product MDP.An ε-action updates only the LDBA state, while an MDP action determines the next MDP state probabilistically and advances the automaton using the current label.
  • RL synthesis: Algorithm 1 translates ϕ to an LDBA, constructs the product MDP, initializes Q-values, and repeatedly updates them using rewards and path-dependent discount factors.The learned greedy policy is obtained from the Q-values after interaction with the environment.
  • Product dynamics: A wrong ε-action guess cannot be corrected within an episode, but a later episode can make the correct guess.This episodic treatment addresses the LDBA's nondeterministic ε-transitions during iterative learning.
  • Policy correspondence: A product policy maximizing Büchi satisfaction probability induces a finite-memory policy maximizing LTL satisfaction probability on the original MDP.The induced policy tracks the LDBA state alongside the MDP state, with automaton updates driven by observed labels.

B. Learning for B¨uchi Conditions with Discounted Rewards

The paper develops model-free learning for Büchi objectives using rewards and state-dependent discounting, proving that optimal discounted-return policies maximize satisfaction probabilities as discounting approaches one. It establishes convergence results and a threshold beyond which the optimal policy satisfies the objective.

  • Objective: The objective is to learn a memoryless policy maximizing the probability of satisfying a Büchi condition.Memoryless policies are sufficient for Büchi objectives.
  • Reward and discount design: The proposed model-free method uses carefully designed rewards and state-dependent discounting based on the Büchi condition.The path return is defined so state values approach objective-satisfaction probabilities as γ approaches 1.
  • Value bounds: Lemma 2 bounds returns and shows that replacing path prefixes with accepting states never decreases return, while replacing them with non-accepting states never increases it.These bounds support the later value-function analysis.
  • Accepting components: Values of states in accepting bottom strongly connected components approach 1 under a fixed policy, providing a key step in proving the convergence theorem.The proof uses recurrence in accepting components and return inequalities.
  • Convergence theorem: The optimal value converges to the maximal Büchi-satisfaction probability as γ approaches 1 from below.The theorem derives matching upper and lower bounds, and the corollary relates optimal state values to maximal satisfaction probabilities.
  • Policy optimality: Because policies are discrete, there is a threshold γ′ such that every γ > γ′ yields a satisfaction-probability-maximizing optimal policy.Using γ = 1 can instead allow convergence to a non-optimal policy because multiple fixed-point solutions may exist.

IV. IMPLEMENTATION AND CASE STUDIES

The framework is implemented with Rabinizer 4 and Q-learning, then evaluated in two stochastic grid-world motion-planning scenarios. Training uses ε-greedy exploration, decreasing learning parameters, and 100,000 episodes.

  • The implementation maps LTL formulas into LDBAs with Rabinizer 4 and applies Q-learning using the proposed discounting rewards.
  • The evaluation uses two grid-world scenarios in which a mobile robot chooses among four directional actions under stochastic motion.
  • 100,000 episodes are used to obtain the objective policies and estimates of maximal satisfaction probabilities.
  • The experiments use γ_B = 0.99 and γ = 0.99999, while ε and α decrease from 1.0 to 0.1 and then 0.001.

A. Motion Planning with Safe Absorbing States

The first case study evaluates reaching safe absorbing states while avoiding unsafe states. The learned policy chooses a route that achieves the safety objective almost surely, while the estimates reflect stochastic returns and sampling error.

  • The robot seeks a safe absorbing state while avoiding unsafe states, expressed as an LTL objective.
  • The LDBA has 4 states, the product MDP has 80 states, and episodes terminate after T = 100 steps.
  • From (0, 0), the optimal policy avoids the shorter route through (1, 2) because it reaches an unsafe state with probability 0.2.
  • The policy instead enters (3, 0) or (3, 2) through (3, 1), eventually reaching a safe absorbing state without visiting an unsafe state almost surely.
  • Approximation errors at (1, 2) and (4, 2) arise from return variance, with returns equal to 1 or 0 with probabilities 0.8 and 0.2.
  • The values in Fig. 2a and Fig. 2b come from one run of K=100 000 episodes, while Fig. 2c averages L2 errors over 100 repetitions.

B. Mobile Robot in Nursery Scenario

The nursery case study requires repeated baby checks and charger visits while avoiding danger and following conditional notification rules. The synthesized policy produces distinct routes for leaving the charger, returning while the baby sleeps, and responding when the baby is awake.

  • The robot repeatedly checks the baby and returns to the charger while avoiding the danger zone.
  • The specification encodes six rules covering danger avoidance, baby departure and return, adult notification, charging, and the baby’s waking state.
  • The LDBA has 47 states, the product MDP has 940 states, episodes last 1000 steps, and the robot position resets to charging.
  • After leaving the charger, the policy almost surely reaches the baby at (0, 2) while avoiding a.
  • When the baby is sleeping, the policy returns to the charger; when the baby is awake, it takes the shortest path to a.

V. CONCLUSION

The paper reduces LTL control synthesis in unknown stochastic MDPs to a Büchi-objective problem on a product MDP and solves it with model-free learning. A novel reward and discounting scheme makes the learned memoryless policy maximize satisfaction probability, demonstrated in two motion-planning studies.

  • The method targets control policies that maximize LTL satisfaction probability in unknown stochastic environments modeled as MDPs.
  • LTL synthesis is converted into synthesizing a memoryless policy for a Büchi objective on the product MDP.
  • A novel discounting and reward scheme makes the policy optimizing expected reward also optimize the Büchi and original LTL satisfaction probabilities.
  • The synthesis method is evaluated on two motion-planning case studies.
Loading 1909.07299v2…