PaperlayerView exact revision on arXiv

Source-linked AI summary

Reward Machines for Signal Temporal Logic

Alper Kamil Bozkurt, Shangtong Zhang, Yuichi Motai

arXiv:2608.13625v1cs.AIcs.LGcs.RO

TL;DR

History-dependent STL robustness rewards violate the Markov property needed by standard RL, complicating control synthesis for expressive, long-horizon specifications. The paper compiles STL into reward machines with compact memory and Markovian rewards, achieving higher satisfaction rates and robustness scores than history-based baselines.

  • Problem

    STL robustness rewards depend on execution history, violating the Markov property assumed by standard RL and limiting learning for complex specifications.

  • Method

    The approach compiles STL formulas into timed alternating automata and reward machines that augment states with compact memory and induce Markovian rewards.

  • Results

    The proposed STL-RM variants generally achieve higher satisfaction rates and robustness scores than baselines across simulated environments, including near-optimal satisfaction on full specifications.

  • Takeaways & Limitations

    Automata-based reward design provides a promising direction for model-free control synthesis from expressive STL specifications.

  • Takeaways & Limitations

    The finite memory list can become a bottleneck for specifications generating many simultaneous temporal obligations.

Abstract

from arXiv · show

Signal temporal logic (STL) provides a formal language for specifying real-time properties of real-valued observations, along with a quantitative robustness score for monitoring satisfaction. Control synthesis from STL specifications is of interest since manual controller design becomes infeasible as real-world systems grow in complexity. Moreover, many modern autonomous and AI-enabled systems lack accurate and complete system models, which makes optimization-based synthesis approaches unsuitable and motivates learning-based control. Prior work uses STL robustness scores as rewards in reinforcement learning (RL) to obtain control policies satisfying given specifications; however, robustness depends on execution history, leading to intractable state space expansion for general long-horizon specifications with arbitrarily nested temporal operators. This work introduces a novel automata-based approach that provides an efficient memory mechanism and associated Markovian rewards suitable for RL frameworks. Our approach constructs a timed alternating automaton from the given STL specifications, augments the state space with automaton locations and clock valuations, and derives rewards from the automaton acceptance condition. We empirically demonstrate that our approach learns policies that achieve higher robustness scores and satisfaction rates than those learned by existing approaches using robustness-based rewards.

I. INTRODUCTION · II. RELATED WORK · A. Model-Based Synthesis Approaches

STL supports quantitative, real-time specification and motivates automated controller synthesis, but model-based methods face scalability and model-availability limitations. The proposed reward-machine framework addresses history dependence for learning-based control and reports faster learning with higher satisfaction rates.

  • I. INTRODUCTION: STL expresses requirements over real-time, real-valued signals using numerical predicates and metric temporal operators, while robustness measures satisfaction strength.Robustness also accounts for timing and other uncertainties, supporting systematic trace verification.
  • I. INTRODUCTION: Automated STL controller synthesis is needed because manual controller design is impractical for many real-world systems.The motivation includes requirements involving timing perturbations and other uncertainty forms.
  • I. INTRODUCTION: Model-based optimization is widely studied, but high-fidelity models are often unavailable for increasingly complex, AI-enabled autonomous systems.This motivates data-driven learning and direct integration of STL into learning-based control.
  • I. INTRODUCTION: The proposed reward machines mitigate STL satisfaction’s history dependence by providing efficient memory and Markovian rewards for RL-based control synthesis.The framework constructs automata-based memories that make the rewards compatible with off-the-shelf RL algorithms.
  • I. INTRODUCTION: The framework models stochastic control systems as semi-Markov decision processes and derives one-clock alternating timed automata from event-based STL semantics.STL reward machines are then constructed from the automata’s acceptance conditions, with robustness to observation perturbations incorporated into rewards.
  • I. INTRODUCTION: The approach learns control policies faster and achieves higher satisfaction rates than existing methods on long-horizon specifications across several simulated experiments.This is the reported empirical comparison in the introduction.
  • II. RELATED WORK: Prior STL controller-synthesis research is commonly divided into model-based and model-free categories according to whether a system model is assumed available.The related-work discussion reviews prominent approaches and their drawbacks in both categories.
  • A. Model-Based Synthesis Approaches: Model-based STL synthesis primarily uses mixed-integer programs and receding-horizon MPC, but horizon length creates a tradeoff between myopic solutions and computational expense.Control-barrier-function alternatives may be restricted to STL fragments, linear systems, or additional reachable-set computation, while history dependence increases long-horizon computational and gradient difficulties.

B. Model-Free Learning Approaches · III. PRELIMINARIES · A. Semi-Markov Decision Processes

The paper motivates model-free RL for STL control while addressing the history dependence that makes robustness-based rewards non-Markovian and costly for long-horizon specifications. It then formalizes the semi-Markov setting, where real-valued observation durations are explicit and Markovian rewards permit memoryless-policy learning with standard RL tools.

  • B. Model-Free Learning Approaches: RL learns reward-maximizing controllers directly from interaction data without requiring an explicit dynamics model, motivating robustness-based rewards for STL control synthesis.
  • B. Model-Free Learning Approaches: STL satisfaction rates and robustness scores depend on entire traces, making these rewards history-dependent and challenging for standard RL.
  • B. Model-Free Learning Approaches: Augmenting states with specification-determined recent history restores Markovian structure but can make long-horizon STL problems computationally prohibitive.
  • B. Model-Free Learning Approaches: Related automata-based RL methods compile temporal-logic specifications into automata and learn on product systems, mostly for untimed logics such as LTL.
  • A. Semi-Markov Decision Processes: SMDPs model controller-environment interaction with stochastic, real-valued durations between successive observations.
  • A. Semi-Markov Decision Processes: An SMDP comprises states, an initial state, actions, and a probabilistic transition function parameterized by elapsed time.
  • A. Semi-Markov Decision Processes: Elapsed time records transition and dwelling durations explicitly in SMDPs, unlike discrete-time MDPs, which abstract timing away.
  • A. Semi-Markov Decision Processes: When rewards depend only on the latest state and duration, memoryless policies suffice and standard RL can learn an optimal policy despite unknown transitions.

B. Event-Based Signal Temporal Logic

This section defines STL syntax and event-based semantics over infinite timed paths, using predicates, Boolean connectives, and interval-bounded temporal operators. It also explains why history-dependent robustness scores are unsuitable as Markovian RL rewards for long-horizon specifications.

  • STL Syntax: STL predicates are inequalities µ ≥0 mapping states to scalar values, and specifications are recursively constructed from predicates, negation, conjunction, and until.The until operator uses a time interval with nonnegative rational or infinite endpoints.
  • STL Syntax: Derived STL operators include disjunction, implication, true, finally, and globally, with omitted interval subscripts when I = [0, ∞).Finally and globally are defined from true, until, and negation.
  • Event-Based Semantics: The event-based semantics evaluate specifications over infinite timed paths σ = (s0, τ0)(s1, τ1) . . . and define satisfaction on timed suffixes σ[t:].This formulation aligns with standard RL formalisms and recursively specifies conjunction and until satisfaction.
  • Robustness Limitation: History dependence from inf and sup operations over path fragments makes spatial robustness scores unsuitable as Markovian RL rewards for long-horizon specifications.The approach therefore uses these scores for evaluation and comparison rather than directly as rewards.

IV. PROBLEM FORMULATION · V. REWARD MACHINES FOR SIGNAL TEMPORAL LOGIC

The paper formulates STL policy learning in unknown stochastic SMDPs around maximizing satisfaction probability, with robustness as a secondary evaluation objective. It introduces extended reward machines for OCATAs and composes them with SMDPs to produce augmented models with Markovian rewards.

  • IV. PROBLEM FORMULATION: The problem concerns learning control policies satisfying STL specifications in unknown environments modeled as semi-Markov decision processes (SMDPs).SMDPs explicitly represent elapsed time between consecutive observations, enabling real-time constraints to be expressed.
  • IV. PROBLEM FORMULATION: Stochastic transitions can produce different successor states and transition durations across repeated executions of the same policy.The resulting timed paths vary under both SMDP stochasticity and probabilistic satisfaction caused by modeled predicate perturbations.
  • IV. PROBLEM FORMULATION: The primary objective is maximizing the probability that a policy-generated timed path satisfies the STL specification.This objective directly accounts for stochastic timed-path generation and probabilistic specification satisfaction.
  • IV. PROBLEM FORMULATION: Problem 1 asks for a mechanism Rφ that generates memory states and Markovian rewards so efficient RL can learn a policy π∗ maximizing STL satisfaction probability.The formulation assumes an SMDP M with unknown transition function P and an STL specification φ.
  • IV. PROBLEM FORMULATION: Expected robustness is retained only as a secondary evaluation metric rather than the optimization objective.Optimizing expected robustness may favor high robustness on a small subset of trajectories while frequently violating the specification.
  • V. REWARD MACHINES FOR SIGNAL TEMPORAL LOGIC: The proposed solution introduces extended reward machines for OCATAs derived from STL specifications and permits nondeterministic, conjunctive, and probabilistic transitions.The machines also use a Büchi acceptance condition to capture full-STL event-based semantics under observation perturbations.
  • V. REWARD MACHINES FOR SIGNAL TEMPORAL LOGIC: Composing an SMDP with an extended reward machine yields an augmented model with Markovian rewards.This composition addresses Problem 1 by providing the memory and reward structure required for reinforcement learning.

A. One-Clock Alternating Timed Automata

The method translates STL specifications into one-clock alternating timed automata with Büchi acceptance, whose states track locations and clock valuations while transitions support nondeterministic and universal branching. Acceptance is defined over computation trees, requiring every infinite path to revisit accepting locations infinitely often.

  • Construction: The procedure translates a given STL specification into an OCATA with a Büchi acceptance condition based on repeated reachability.Although presented for MITL, the construction applies directly to STL.
  • Transition structure: An OCATA is a one-clock timed automaton whose transitions may use disjunctive and conjunctive branching.Disjunctive transitions introduce nondeterministic choices, whereas conjunctive transitions spawn multiple computation threads.
  • State evolution: An OCATA state consists of a location and a nonnegative clock valuation, initialized at the initial location with clock value zero.Upon each observation, the automaton advances its clock, computes satisfied predicates, and selects a satisfied clock constraint.
  • Acceptance: A run induced by a timed path forms a computation tree, and it is accepting only if every infinite computational path visits accepting locations infinitely often.The acceptance condition applies universally across paths created by conjunctive branching.
  • Illustration: The illustrated OCATA represents eventual target-region reachability followed by return within 1 time unit whenever the region is left.Its disjunction nondeterministically chooses between transitions corresponding to the target-region-reaching behavior.

B. Reward Machine Construction

The STL reward machine is constructed from an OCATA by combining state-based Büchi rewards with mechanisms for nondeterministic and conjunctive transitions. It also incorporates robustness through probabilistic predicate satisfaction induced by pseudoperturbations.

  • Design objectives: Reward design must encode Büchi acceptance, handle disjunctive and conjunctive transitions, and incorporate robustness to state perturbations.These are identified as the main construction challenges.
  • State-based rewards: Accepting locations receive reward r, other locations receive zero, and discount factors distinguish accepting from non-accepting visits.The scheme uses γ = 1 − r in accepting locations and γ′ = 1 − r^2 in non-accepting locations.
  • Nondeterministic transitions: Disjunctive OCATA transitions become ε-actions selected by the RL agent, while expected return lower-bounds satisfaction probability.The lower bound becomes equality when the OCATA is suitably limit-deterministic.
  • Conjunctive transitions: Conjunctive branches are tracked with a memory list of OCATA copies, and averaged copy rewards form a joint reward whose maximization preserves joint-return optimization.A probability mass is associated with each copy; clock resets create new memory entries, while non-resetting branching redistributes mass.
  • Robustness: Robustness is incorporated by treating predicate outputs as noisy observations, yielding predicate-satisfaction probabilities through a cumulative distribution function.For an observed state s, the construction defines PR(µ > 0) = h(µ(s)).

C. Product Construction for Markovian Rewards

The STL reward machine augments SMDP states with a memory list and automaton location to form a product MDP with Markovian rewards. This construction is compatible with standard RL tools, but requires bounded memory because real-valued durations can make memory lists unbounded.

  • Product construction: The reward machine outputs a memory list and scalar reward, enabling an augmented state with Markovian rewards.The product combines the SMDP state, memory-list valuation, and reward-machine location.
  • Product construction: Product transitions follow the SMDP transition when the reward-machine update matches, while product rewards depend only on the reward-machine location.The product action is an SMDP action paired with an ϵ-action, and R×(⟨s, τ, q⟩) := R(q).
  • RL compatibility: The resulting product MDPs are standard discrete-time MDPs usable with off-the-shelf RL tools, with duration effects encoded in the memory list.The memory list is part of the product state and captures how time durations affect STL satisfaction.
  • Memory limitation: Real-valued observed durations can cause unbounded memory-list growth, which the authors view as fundamentally difficult to avoid without additional assumptions.The approach therefore assumes a fixed capacity of N entries; once full, new entries and their probability mass are discarded to a rejecting sink state.
  • Correctness guarantee: Maximum expected return 1 is achievable only under a policy satisfying the STL specification with probability 1.The result relies on the correspondence between product paths and timed paths induced by the reward-machine update function.

VI. EXPERIMENTS

The experiments evaluate STL-RM across diverse control environments against standard history-based reinforcement-learning baselines. The section introduces the specifications, environments, baselines, implementation details, and results, with code publicly available.

  • STL-RM is evaluated across a diverse set of control environments and compared with standard history-based RL baselines.
  • The experiments first introduce the STL specifications used throughout the evaluation.
  • The section then describes the evaluation environments, baselines, implementation details, and experimental results.
  • The authors provide their code at the project’s GitHub repository.Repository: https://github.com/alperkamil/stlrm.

A. STL Tasks

The STL tasks combine ordered target visitation, bounded-time return to a central region, and perpetual safety constraints. They compare a partial specification requiring logical progression with a full specification that additionally requires retaining event timing.

  • Task requirements: The safety requirement constrains the agent to avoid the unsafe regions represented by c1 and c2 at all times.The supplied task description states that safety must hold continuously.
  • Task requirements: The task requires visiting the positive target region (3, ∞) before the negative target region (−∞, −3).This sequencing requirement is represented by visiting a1 and subsequently a2.
  • Task requirements: After either target visit, the agent must return to the central region (−2, 2) within T = 30 time steps.The stability requirement is triggered by visiting either target region.
  • Specification variants: The partial specification φpartial requires ordered target visitation and safety while abstracting away precise event timing.Because it contains only unbounded temporal operators, it primarily requires retaining logical progression and can be represented by a small automaton.
  • Specification variants: The full specification φfull additionally requires memory of both event progression and timing to satisfy the bounded-time stability condition.After a target visit, the agent must retain the temporal context needed to reach the central region within T time steps.

B. Environments

STL-RM is evaluated across five Gymnasium benchmark environments spanning discrete control to high-dimensional robotic manipulation. The experiments standardize STL evaluation by selecting position signals, normalizing them across environments, and removing native learning objectives.

  • Benchmark environments: STL-RM is evaluated on five Gymnasium control environments spanning low-dimensional discrete control through high-dimensional continuous robotic manipulation.The environments are CartPole, Reacher, Pusher, Fetch, and Adroit.
  • Benchmark environments: CartPole uses a discrete action space and evaluates its STL specification using the cart’s horizontal position.All other listed environments use continuous action spaces.
  • Benchmark environments: Reacher, Pusher, Fetch, and Adroit are continuous-control robotic environments using horizontal fingertip, end-effector, or hand positions as STL signals.Pusher is a higher-dimensional manipulation task, while Adroit is a high-dimensional dexterous manipulation environment.
  • Signal preprocessing: Selected position signals are normalized to initial mean zero and environment-specific scaling so one STL specification applies consistently across environments.The transformation places relevant signal values within a reachable range despite differing raw position ranges.
  • Experimental protocol: Episodes last at most 500 time steps, native rewards are removed, and default early termination is disabled except for safety violations.This makes learning driven exclusively by the STL objective rather than environment-specific objectives.

C. Baselines and Implementation

The study compares STL-RM with observation-stacking and recurrent-policy baselines, plus a discretized STL-RM ablation, under a common PPO-based implementation. Baselines use dense-time online STL robustness rewards, while evaluation reports robustness and satisfaction across trajectories.

  • Baselines: STL-RM is compared with observation stacking and recurrent policies, which expose historical information without explicitly constructing a symbolic temporal-specification representation.The recurrent baseline uses an LSTM to learn a latent representation, whereas stacking retains a fixed observation-history window.
  • Implementation: STL-RM constructs Büchi automata for sequencing and safety, represents bounded-time stability with an OCATA and memory mechanism, and sets memory-list capacity to N = 50.The implementation also uses clipped acceptance and rejection transition functions.
  • Baselines: STL-RM (DISCRETE) replaces the continuous transition CDF with h(z) = 1z≥0, isolating the effect of continuous robustness-aware transition construction.The indicator evaluates to 1 when z ≥0 and to 0 otherwise.
  • Baselines: STACKING uses history windows of 5, 50, and 500 observations, while RECURRENT uses a single LSTM layer with 256 hidden units.The stacking configurations represent short, intermediate, and full-episode histories, respectively.

D. Results · VII. CONCLUSION

Across five environments, STL-RM methods outperform robustness-reward baselines, especially for full specifications, while continuous robustness information improves robustness beyond satisfaction. The conclusion presents STL-RM as a compact, Markovian automata-based framework, while noting finite-memory limits and extensions to richer settings.

  • D. Results: Over 400 K steps, STL-RM and STL-RM (DISCRETE) rapidly converge to satisfaction rate 1 for φpartial and outperform baselines except on FETCH.The variants generally achieve higher robustness scores, while FETCH remains competitive for the baselines.
  • D. Results: Baselines substantially degrade from φpartial to φfull, whereas STL-RM variants reach optimal or near-optimal satisfaction rates and STL-RM achieves higher robustness scores.The result demonstrates the difficulty of learning bounded-time requirements from observation history using STL robustness alone.
  • D. Results: The satisfaction-rate difference between STL-RM and STL-RM (DISCRETE) is generally small, but STL-RM typically achieves higher robustness scores.Probabilistic transitions incorporate continuous robustness information, encouraging trajectories that satisfy specifications more robustly than discretized transitions.
  • VII. CONCLUSION: The framework compiles event-based STL formulas into OCATAs and STL-RMs, providing compact memory and Markovian rewards compatible with standard RL algorithms.It also incorporates robustness to observation perturbations into reward construction.
  • VII. CONCLUSION: Policies maximizing cumulative reward satisfy the specification almost surely, while STL-RM achieves higher satisfaction rates and robustness scores than history-based robustness-reward baselines.The empirical results support automata-based reward design for model-free control synthesis from expressive STL specifications.
  • VII. CONCLUSION: The STL-RM memory list may require one entry per temporally constrained condition, making finite memory a bottleneck when many temporal obligations occur simultaneously.The conclusion identifies more compact memory representations as an important direction for future work.
  • VII. CONCLUSION: The reward-machine formulation enables extensions using counterfactual reasoning, lexicographic objectives, and stochastic games for richer multi-objective and multi-agent policy synthesis.These extensions may improve learning efficiency and broaden STL-based policy synthesis.
Loading 2608.13625v1…