Source-linked AI summary
Environment-Independent Task Specifications via GLTL
Michael L. Littman, Ufuk Topcu, Jie Fu, Charles Isbell, Min Wen, James MacGlashan
TL;DR
Reward functions control behavior but are difficult to use for environment-independent task specification, and classical LTL can require impossible precision for finite-time learning. The paper introduces probabilistic GLTL and specification MDPs to express tasks independently of the environment while retaining learnable approximations. The resulting construction supports standard reinforcement-learning tasks and makes satisfaction maximization compatible with solving a fixed MDP.
Problem
Reward functions are difficult to structure as reliable environment-independent specifications, while some LTL tasks cannot be learned from finite-precision environment approximations.
Method
The paper extends LTL with probabilistic expiration and composes GLTL specification MDPs with environment MDPs so task satisfaction becomes an optimization objective.
Results
GLTL yields a well-behaved dependence of satisfaction probability on transition-estimate accuracy, unlike LTL's infinite-precision requirement in the example.
Takeaways & Limitations
GLTL provides environment-independent specifications that capture standard MDP tasks and can be automatically incorporated into an environment MDP.
Takeaways & Limitations
Classical LTL lacks the approximation property needed to guarantee near-optimal satisfaction from any finite-accuracy model approximation.
Abstract
from arXiv · showhide
We propose a new task-specification language for Markov decision processes that is designed to be an improvement over reward functions by being environment independent. The language is a variant of Linear Temporal Logic (LTL) that is extended to probabilistic specifications in a way that permits approximations to be learned in finite time. We provide several small environments that demonstrate the advantages of our geometric LTL (GLTL) language and illustrate how it can be used to specify standard reinforcement-learning tasks straightforwardly.
1 Introduction
The paper argues that reward functions are useful for controlling behavior but difficult to design as environment-independent task specifications. It motivates a probabilistic temporal-logic representation that preserves task structure while supporting finite-time learning.
- 1 Introduction: Reward functions are difficult to use for reliably specifying tasks when utilities such as avoiding damage cannot be expressed in a consistent unit.The paper frames behavior specification as programming: the same task specification should work across different environments.
- 1.1 Specifying behavior via reward functions: Repeatedly redesigning rewards and relearning in the target environment can undermine the purpose of autonomous learning.
- 1.1 Specifying behavior via reward functions: At slip probability p = 0.3, no value of r makes action a2 preferable to a1, so the desired behavior cannot be induced by this reward structure.For p = 0.1, setting r > 0.16 does encourage the desired behavior; the paper attributes the failure to trading off one certain bad-state visit against potentially repeated visits.
- 1.2 Specifying behavior via LTL: LTL can express safety, goal, progress, response, and stability properties, but some LTL tasks cannot be learned with finite-time model approximations.The paper gives standard task examples including mountain car, cart pole, taxi, and pendulum swing up.
- 1.2 Specifying behavior via LTL: For □g, distinguishing p1 = 1 from p1 < 1 may require an unbounded number of trials, making near-optimal behavior unavailable in worst-case finite time.
- 1.2 Specifying behavior via LTL: The proposed hybrid approach combines the strengths of reward functions and temporal-logic specifications.
2 Learning To Satisfy LTL
GLTL extends LTL with geometrically bounded temporal operators and specification MDPs, enabling finite-time learning while preserving environment-independent task specifications. Its construction also improves sensitivity to transition-probability estimation compared with standard LTL.
- Motivation: Correctness for complicated, high-level task specifications during learning and in learned behavior has received limited attention relative to efficiency and optimality.This motivates studying specification languages with learnability and correctness properties.
- Geometric linear temporal logic: GLTL restricts temporal operators to stochastic bounded windows, with expiration times sampled from geometric distributions.For example, ♦µb requires b within k steps, where k ∼ G1(µ).
- Geometric linear temporal logic: GLTL avoids unnecessary specification-state expansion by representing event occurrence rather than merely elapsed time.The geometric decay is also described as a generalization of reward discounting.
- Specification MDPs: GLTL formulas are encoded as specification MDPs whose states, actions, and probabilities represent formula-derived task conditions and operator expiration.For □µg, violating g immediately fails the specification, while continued satisfaction can transition to success when the temporal window expires.
- Learning properties: For µ = .9, satisfaction-value dependence on ϵ is .1/(.1+ϵ), with sensitivity bounded by 1/(1−µ)^2, making GLTL more learnable than LTL.The cited bound describes the maximum dependence of computed satisfaction probability on transition-estimation accuracy.
- Environment-independent specifications: In the example MDP, ¬q Uµp penalizes any bad-state encounter or timeout, so maximizing satisfaction selects a1 independently of p.The construction allows a penalty on the first bad-state encounter without repeated penalties afterward.
3 Related Work
Prior work uses discounting in quantitative temporal logic and temporal-logic methods for verification, synthesis, and robot planning. Table 1 records operator precedence for constructing specification MDPs.
- Discounting in temporal logic: Discounting in quantitative temporal logic weights satisfaction of properties in the near future more heavily than satisfaction in the far future.Related approaches augment CTL or refine LTL’s eventually operator with discounting.
- Temporal logic for robotics: LTL-based research has addressed trustworthiness, verification, and synthesis for robotic motion, task, and mission planning.The cited work includes deterministic, stochastic, and nondeterministic finite-state models, plus continuous-state models through finite-state abstractions.
- Specification MDP construction: Table 1 specifies operator precedence used when constructing specification MDPs.The precedence determines how nested GLTL expressions are grouped during recursive conversion.
4 Generating Specification MDPs
GLTL formulas are recursively converted into specification MDPs whose stochastic operator expirations support finite-time learning. These specification MDPs are composed with environment MDPs, then solved to obtain policies maximizing satisfaction probability.
- Specification MDP construction: GLTL extends LTL with probabilistic temporal operators, including µ-until, µ-eventually, and µ-always.Derived operators include disjunction, ♦µ, and □µ.
- Specification MDP construction: Specification MDPs are constructed recursively from atomic propositions and Boolean operators by defining states, actions, transitions, and accepting or rejecting terminal states.Negation swaps accepting and rejecting states, while conjunction combines component specification MDPs.
- Specification MDP construction: The µ-until construction tracks two operand specifications, accepts when the second succeeds first, rejects when the first fails first, and otherwise permits stochastic expiration.Its transition probabilities combine the operand transitions with the operator-expiration probabilities.
- Derived temporal operators: µ-eventually succeeds when its operand is achieved within a stochastic observation period, while µ-always requires no operand failure during that period.These operators are implemented through corresponding specification MDP transition constructions.
- Environment composition and policy: A joint MDP is formed by taking the cross product of the environment and specification MDP, making terminal specification states sinks, and solving the result for a policy.The resulting policy maximizes formula-satisfaction probability over both environment and specification stochastic transitions and tends to favor faster satisfaction.
5 Example Domain
The grid-world example uses a temporal specification requiring the agent to reach red without blue and then reach green. The resulting policy routes around the blue barrier before red, then crosses it directly toward green.
- Task specification: The task requires reaching a red state without encountering blue, then proceeding to a green state.This sequence is expressed as a temporal specification rather than as independent positive rewards.
- Environment: The grid world has colored cells, four directional actions, and a 0.02 probability that an action moves in one of the other directions.The stochastic movement encourages paths that maintain distance from dangerous cells when possible.
- Policy behavior: The optimal policy reaches red and then green, a sequence that is difficult to encode with standard rewards because both destinations receive positive reward.A reward-only formulation could make either red or green a sensible stopping point.
- Policy behavior: The policy goes around the blue wall before red but crosses the barrier directly after red because the prohibition on blue is then lifted.This demonstrates how the until condition changes the allowed behavior after the intermediate goal is reached.
- Environment composition: The 25-state environments become 98-state MDPs after composition with the specification MDP.
6 Conclusion
The paper provides an environment-independent task specification that captures standard MDP tasks and converts them into fixed MDPs whose reward optimization maximizes specification satisfaction. Future work targets inverse reinforcement learning for task specifications and faster planning.
- The proposed specification is environment-independent, unlike standard MDP reward functions.
- The language captures standard MDP tasks and can be automatically incorporated into an environment MDP to create a fixed MDP for solving.
- Maximizing reward in the resulting MDP maximizes the probability of satisfying the task specification.
- Future work includes inverse reinforcement learning of task specifications and techniques for accelerating planning.