Reinforcement Learning for Temporal Logic Control Synthesis with Probabilistic Satisfaction Guarantees

Mohammadhosein Hasanbeig; Yiannis Kantaros; Alessandro Abate; Daniel Kroening; George J. Pappas; Insup Lee

Source-linked AI summary

Reinforcement Learning for Temporal Logic Control Synthesis with Probabilistic Satisfaction Guarantees

Mohammadhosein Hasanbeig, Yiannis Kantaros, Alessandro Abate, Daniel Kroening, George J. Pappas, Insup Lee

arXiv:1909.05304v1Sep 11, 2019cs.LOcs.LGeess.SYstat.ML

TL;DR

The paper addresses LTL control synthesis when the PL-MDP’s dynamics, labels, and graph structure are unknown. It combines model-free RL with an LDBA-based product and synchronous reward, and proves that the resulting policy maximizes satisfaction probability while also producing a closest-to-satisfaction policy when the specification is unsatisfiable.

Problem
The problem is to synthesize policies maximizing LTL satisfaction probability in PL-MDPs with unknown stochastic behavior, labels, and graph structure.
Method
The method translates LTL into an LDBA, forms an on-the-fly product with the PL-MDP, and uses acceptance-based synchronous rewards with model-free RL.
Results
The optimal policy maximizing expected accumulated reward also maximizes the probability of satisfying the LTL property when the property is satisfiable.
Takeaways & Limitations
When the specification is unsatisfiable, the algorithm synthesizes the closest-to-satisfaction policy, including cases where AMEC-based methods cannot provide one.

Abstract

from arXiv · show

Reinforcement Learning (RL) has emerged as an efficient method of choice for solving complex sequential decision making problems in automatic control, computer science, economics, and biology. In this paper we present a model-free RL algorithm to synthesize control policies that maximize the probability of satisfying high-level control objectives given as Linear Temporal Logic (LTL) formulas. Uncertainty is considered in the workspace properties, the structure of the workspace, and the agent actions, giving rise to a Probabilistically-Labeled Markov Decision Process (PL-MDP) with unknown graph structure and stochastic behaviour, which is even more general case than a fully unknown MDP. We first translate the LTL specification into a Limit Deterministic Buchi Automaton (LDBA), which is then used in an on-the-fly product with the PL-MDP. Thereafter, we define a synchronous reward function based on the acceptance condition of the LDBA. Finally, we show that the RL algorithm delivers a policy that maximizes the satisfaction probability asymptotically. We provide experimental results that showcase the efficiency of the proposed method.

I. INTRODUCTION

The paper targets LTL-constrained control synthesis when MDP dynamics, workspace properties, and graph structure are uncertain. It proposes a model-free RL method using PL-MDPs and reports benefits from LDBA-based synthesis without AMEC computation.

Temporal logic expresses safety, liveness, sequential, coverage, and ordering requirements beyond point-to-point navigation.
The problem includes uncertainty in environment properties, agent actions, and the underlying workspace graph, yielding a PL-MDP.
The method addresses uncertainty more broadly than related approaches that model uncertainty only in agent actions or assume known MDP structure.
The proposed method is a model-free RL algorithm for synthesizing policies that maximize the probability of satisfying LTL specifications.
LDBA-based synthesis avoids the DRA conversion used by related methods and does not require computing AMECs of a product MDP.

II. PROBLEM FORMULATION

The paper formulates control synthesis over a fully observable PL-MDP with uncertain transitions and labels, seeking a deterministic stationary policy that maximizes LTL satisfaction probability. Runs combine states, observations, and actions into traces evaluated against the specification.

A PL-MDP models a finite-state robot environment with uncertain motion and workspace properties.
Its transition function gives action-conditioned state-transition probabilities, while its labeling function gives probabilities for observed atomic-proposition sets.
The model is assumed fully observable, so the current state and observation are known at each stage.
A run records the successive states, observations, and control actions taken by the robot.
The synthesis objective is a deterministic stationary policy maximizing the probability that generated traces satisfy the LTL formula.

III. A NEW LEARNING-FOR-PLANNING ALGORITHM

The algorithm translates the LTL specification into an LDBA, composes it on the fly with the PL-MDP, and rewards product transitions according to the automaton’s acceptance condition. The resulting product policy is projected back to obtain a policy for the original model.

The method first translates the LTL formula into an LDBA and constructs a product by composing the PL-MDP with that automaton.
It assigns rewards to product-MDP transitions based on the LDBA acceptance condition.
The algorithm synthesizes a product policy maximizing the probability of satisfying the LDBA acceptance conditions.
Projecting the product policy onto the PL-MDP yields a policy that solves the original synthesis problem.

A. Translating LTL into an LDBA

The paper uses LDBAs to represent LTL properties more compactly than conventional DRAs, reducing the product state space explored by learning. LDBA acceptance combines nondeterministic guessing with deterministic behavior after entering the deterministic component.

An LTL formula is represented by an automaton that recognizes the words satisfying the specification.
LDBAs provide a more succinct alternative to DRAs, whose worst-case size is doubly exponential in the original formula size.
The resulting automaton reduces the state space that must be explored during product-based synthesis.
An LDBA partitions states into nondeterministic and deterministic sets, with accepting sets contained in the deterministic component.
Unknown graph structure prevents methods requiring knowledge of which transition probabilities are zero from being applied.

B. Product MDP

The product MDP composes the PL-MDP with an LDBA so that workspace states, observations, and automaton states jointly represent LTL-constrained behavior. Its transitions combine environment dynamics and probabilistic labeling, while ε-transitions are handled through added product actions.

Product construction: The product state is a tuple of an environment state, observed label, and LDBA state: s = (x, ℓ, q).The product state space is S = X × 2^AP × Q, with the initial state combining the initial PL-MDP state, label, and automaton state.
Product construction: Product transitions combine PL-MDP motion probabilities with observation-label probabilities, while the next automaton state follows q′ = δ(q, ℓ′).The transition probability is defined as PC(x, u, x′)PL(x′, ℓ′).
Acceptance: Accepting product states lift each LDBA accepting set Fj across all environment states and labels, forming FPj = X × 2^AP × Fj.The product accepting-state family is FP = {FPj}, indexed by the LDBA accepting sets.
ε-transitions: ε-transitions in the LDBA become explicit product actions that preserve the environment state and label while changing the automaton state.These actions are added to the available action set, with deterministic transition probability one for the matching product successor.
Acceptance: An infinite product run is accepting when every accepting set of the LDBA is visited infinitely often.The construction therefore connects LTL satisfaction to the Büchi acceptance condition in the product MDP.

C. Construction of the Reward Function

The reward construction tracks which LDBA accepting sets remain to be visited and rewards progress through them. Episodic model-free Q-learning then optimizes this reward without explicitly storing the product MDP.

Reward design: Visiting an accepting set Fj yields positive reward, while revisiting Fj yields zero reward until the other accepting sets have also been visited.All other transitions receive zero reward, making reward accumulation synchronous with the Büchi acceptance condition.
Accepting frontier: The accepting frontier set A records the accepting sets that still need to be visited and is updated whenever an accepting set is reached.The frontier is initialized from the family of accepting sets and updated on-the-fly through the accepting frontier function.
Reward design: The reward function assigns r > 0 when the reached automaton state belongs to the current accepting frontier and zero otherwise.The reached product state s′ determines whether the transition receives the positive reward.
On-the-fly execution: Because the LDBA components are deterministic, automaton transitions can be executed on-the-fly instead of explicitly building and storing the product MDP.This avoids explicit product construction during the proposed algorithm.
Policy synthesis: Episodic Q-learning constructs a stationary deterministic policy by optimizing expected accumulated return, using action values because the product MDP is unknown.The learned product policy is projected onto the PL-MDP state space to obtain the finite-memory control policy ξ∗.

IV. ANALYSIS OF THE ALGORITHM

The analysis establishes that the learned policy maximizes LTL satisfaction probability when the property is satisfiable and yields the closest policy otherwise. The experiments illustrate the algorithm in grid-world and Pacman settings.

Algorithm: The algorithm is model-free and can use off-the-shelf temporal-difference learning methods, including variants of Q-learning.Algorithm 1 is presented as an RL procedure for the LTL objective.
Algorithm: Q-learning updates action values from observed rewards and successor states while maintaining action-visit counts.The update uses an incremental count-based step and the discounted maximum successor action value.
Optimality: If an LTL property is satisfiable by the PL-MDP, the optimal policy for expected accumulated reward also maximizes its satisfaction probability.This is the main optimality result for the proposed reward construction.
Unsatisfiable properties: When no policy satisfies the property, the algorithm returns a policy closest to satisfaction according to intersections between induced runs and automaton accepting sets.Closeness is defined by having more run intersections with accepting sets than another unsatisfying policy.

V. EXPERIMENTS

The experiments evaluate the method in dynamic grid-world and Pacman settings, including deterministic and noisy actions. They report policy synthesis behavior, satisfaction probabilities, and reduced automaton size.

Experimental setup: Three case studies use two 10 × 10 grid-world experiments and a difficult Atari Pacman configuration.The experiments were implemented in MATLAB R2016a on an Intel Xeon 2.93 GHz computer with 4 GB RAM.
Grid-world task: The robot task combines eventual visitation, repeated visits and observations, ordering constraints, and obstacle avoidance.The corresponding LTL formula includes target, user, and obstacle requirements.
Grid-world task: The LTL formula has 11 states as a DRA but only 5 states as an LDBA, reducing the state space to explore.The robot’s PL-MDP has 100 states, 10 actions per state, and probabilistically varying target and user locations.
Case studies: With deterministic robot actions, the optimal policy was constructed in approximately 30 minutes over 260000 episodes.The first case study has AMECs, and Figure 1 shows the projected optimal control path.
Case studies: With a noisy controller selecting the desired action with probability 0.8, the policy was synthesized in approximately 2 hours over 800000 episodes.This case has no AMECs because obstacle collisions retain non-zero probability, yet the method still synthesizes a closest-to-satisfaction policy.
Case studies: In the Pacman experiment, deterministic actions were trained over 186000 episodes, whereas standard Q-learning without LTL guidance was described as impractical for the task.The Pacman LTL formula uses an LDBA with 4 states and requires eating both foods while avoiding ghosts.
Results: The synthesized policy satisfies the specification with probability 1 in the first case, while satisfaction probability is 0 in the second because AMECs do not exist.The proposed algorithm can nevertheless synthesize the closest-to-satisfaction policy in the second case.

VI. CONCLUSIONS

The paper concludes that its model-free RL method synthesizes policies for LTL objectives in unknown PL-MDPs. Its construction combines LDBAs with reward shaping, and the reported conclusion includes best-possible behavior when specifications are unsatisfiable.

Conclusions: The paper proposes a model-free RL algorithm for unknown PL-MDPs that maximizes the probability of satisfying LTL specifications.The environment includes an unknown probabilistically-labeled MDP interaction model.
Conclusions: The paper states that its RL algorithm produces a policy maximizing satisfaction probability and synthesizes the best possible policy when the specification cannot be satisfied.Numerical experiments provide evidence for the method’s efficiency.
Conclusions: The accepting-frontier mechanism represents progress by tracking accepting sets that still need to be visited.The construction assumes an ordering of G-subformulas and postpones later monitors while checking the current one.
Conclusions: The method translates LTL specifications into LDBAs and uses a synchronous reward construction tied to accepting sets.The automaton monitors G-subformulas through a product of G-monitors.

B. Proof of Theorem 4.2

The proof argues that policies satisfying the LTL property generate accepting recurrent behavior with sustained positive reward. Any policy whose recurrent behavior is non-accepting eventually loses that reward advantage.

Proof structure: A policy satisfying the property with positive probability induces a Markov chain composed of transient states and irreducible recurrent classes.The proof analyzes these recurrent classes to compare accepting and non-accepting behavior.
Accepting classes: An accepting recurrent class yields positive rewards indefinitely because the policy keeps visiting all accepting sets infinitely often.The reward construction grants positive reward after reaching such a class.
Non-accepting classes: A non-accepting recurrent class either avoids accepting sets or misses at least one, so positive rewards cease after finitely many visits.In the second case, the accepting frontier is never reinitialized.
Contradiction: If the optimal policy had no accepting recurrent class, an accepting policy would have higher expected reward, contradicting its optimality.The contradiction completes the proof that reward maximization supports satisfaction maximization.

C. Proof of Theorem 4.3

The proof connects the proposed reward formulation to standard value-iteration reasoning for satisfaction probability. It concludes that Q-learning selects a policy maximizing the corresponding expected accumulated reward, including when no policy can satisfy the property.

Known-MDP comparison: When the MDP is known, value iteration over the product MDP converts satisfaction probability into reaching accepting maximum end components.The optimal value function represents the maximum probability of satisfying the property at each state.
Known-MDP comparison: The converged value function initializes non-accepting maximum end components at 0 and the rest of the state space at 1.The optimal action is selected by maximizing the transition-weighted successor value.
Reward reduction: A terminal reward of 1 at accepting maximum end components reduces quantitative model checking to an equivalent reward problem.Bellman updates then produce a policy maximizing satisfaction probability.
Reward reduction: In the proposed method, reaching an accepting maximum end component causes all accepting sets to have been visited and yields infinitely many positive rewards.This aligns the proposed reward process with the standard reachability formulation.
Unsatisfiable specifications: When no policy can satisfy the property, Q-learning still converges to a policy with the highest expected accumulated reward and greatest accepting-set intersection.The result follows from the reward construction and the assumption that every policy has only non-accepting recurrent classes.

E. Counter-example

The counter-example examines episodic Q-learning under discounted and undiscounted learning, showing when the expected return favors the left action. The analysis finds that the episodic formulation also handles γ = 1, while the action preference depends on ν.

Undiscounted case: The episodic algorithm covers the undiscounted case, allowing γ = 1 when the discounted sufficient conditions would otherwise fall outside 0 ≤ γ < 1.This is attributed to the episodic nature of the proposed algorithm.
Expected returns: The expected return for the left action is represented as a geometric series of rewards at successive discounted time steps.The return is written as U µ(s0, left) = γ2r + γ5r + γ8r + ... .
Discounted case: For 0 ≤ γ < 1, the discounted case yields a sufficient condition on γ expressed in terms of ν.The condition follows by taking the limit as n approaches infinity, where γn and γ3n vanish.
Undiscounted case: When γ = 1, the derivation based on inequality (14) is unavailable because the relevant limits and cancellation steps fail.The associated expressions become undefined or diverge in the undiscounted limit.
Action preference: For 0 < ν ≤ 1, the limiting return ratio exceeds one, so the expected return for left becomes greater than that for right after finitely many episodes.When ν = 0, the ratio is one and the algorithm is indifferent between the two actions.