Reward Machines for Signal Temporal Logic

# Reward Machines for Signal Temporal Logic
Source: [https://arxiv.org/html/2608.13625](https://arxiv.org/html/2608.13625)
Shangtong ZhangYuichi MotaiThanks:This work was supported by the Commonwealth Cyber Initiative HV\-2Q25\-035, HC\-2Q25\-033, and the Central Virginia Node under the award VV\-1Q26\-001\.Thanks:A\. K\. Bozkurt and Y\. Motai are with the Department of Electrical & Computer Engineering, Virginia Commonwealth University, Richmond, VA, USA \(e\-mail:\{bozkurta,ymotai\}@vcu\.edu\), and S\. Zhang is with the Department of Computer Science, University of Virginia, Charlottesville, VA, USA \(e\-mail:xdm2bt@virginia\.edu\)\.

###### Abstract

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\.

###### Index Terms:

alternating timed automata, reinforcement learning, robust satisfaction, signal temporal logic

## IIntroduction

Signal temporal logic \(STL\) is a formal specification language for expressing requirements over real\-time, real\-valued signals\[[1](https://arxiv.org/html/2608.13625#bib.bib1)\]\. STL combines numerical predicates, expressed as inequalities over signal values, with metric temporal operators that impose explicit real\-time constraints\. STL enables systematic verification by evaluating execution traces with a robustness score\[[2](https://arxiv.org/html/2608.13625#bib.bib2)\]that captures not only whether a specification is satisfied, but also how strongly it is satisfied, which is critical for noisy signals or imperfect models\. These properties make STL well suited to time\-critical control systems with continuous or hybrid dynamics, and it has been applied successfully in domains such as robotics\[[3](https://arxiv.org/html/2608.13625#bib.bib3)\], traffic\[[4](https://arxiv.org/html/2608.13625#bib.bib4)\], and medical systems\[[5](https://arxiv.org/html/2608.13625#bib.bib5)\]\. Over the past two decades, STL has been extended in many directions, including online monitoring methods for robustness\[[6](https://arxiv.org/html/2608.13625#bib.bib6),[7](https://arxiv.org/html/2608.13625#bib.bib7),[8](https://arxiv.org/html/2608.13625#bib.bib8)\]and richer robustness notions that account not only for spatial perturbations, but also for timing perturbations and other forms of uncertainty\[[9](https://arxiv.org/html/2608.13625#bib.bib9)\]\. Despite the practical value of runtime verification for existing control systems, synthesizing controllers directly from STL specifications is required since manual controller design is impractical for many real\-world systems\[[10](https://arxiv.org/html/2608.13625#bib.bib10)\]\.

Control synthesis from STL specifications via optimization for the systems with available models has been widely studied \(e\.g\.,\[[11](https://arxiv.org/html/2608.13625#bib.bib11),[12](https://arxiv.org/html/2608.13625#bib.bib12),[13](https://arxiv.org/html/2608.13625#bib.bib13),[14](https://arxiv.org/html/2608.13625#bib.bib14),[15](https://arxiv.org/html/2608.13625#bib.bib15)\]\)\. However, as modern autonomous systems grow more complex and incorporate more AI components, high\-fidelity models suitable for standard optimization techniques are often unavailable, necessitating data\-driven learning\. As a result, a growing body of work has sought to integrate STL directly into learning\-based control, leveraging its quantitative robustness scores as rewards in reinforcement learning \(RL\) pipelines\. However, the history\-dependent semantics of robustness scores over traces violates the Markov property, a common assumption in standard RL frameworks\. Existing approaches address this issue either by augmenting the state with previously visited states\[[16](https://arxiv.org/html/2608.13625#bib.bib16),[17](https://arxiv.org/html/2608.13625#bib.bib17)\], which is intractable for long\-horizon specifications; or by restricting attention to limited fragments of STL\[[18](https://arxiv.org/html/2608.13625#bib.bib18),[19](https://arxiv.org/html/2608.13625#bib.bib19),[20](https://arxiv.org/html/2608.13625#bib.bib20),[21](https://arxiv.org/html/2608.13625#bib.bib21),[22](https://arxiv.org/html/2608.13625#bib.bib22)\]\. To the best of our knowledge, there is no existing RL approach that considers full STL while remaining more tractable than state augmentation with the entire history\.

In this work, we mitigate the history dependence of STL satisfaction by constructing reward machines \(RMs\), which provide an efficient memory mechanism and induce Markovian rewards, thereby enabling RL\-based control synthesis from STL specifications\. Our contributions are as follows:

- •We introduce a novel automata\-based framework for learning controllers from STL specifications\. We model stochastic control systems as semi\-Markov decision processes \(SMDPs\) and adopt event\-based STL semantics, which enables the derivation of one\-clock alternating timed automata \(OCATAs\)\[[23](https://arxiv.org/html/2608.13625#bib.bib23)\]from the specifications\.
- •We construct STL\-RMs from the derived OCATAs using their acceptance conditions, while additionally incorporating robustness to observation perturbations inspired by the differentiable rewards from\[[24](https://arxiv.org/html/2608.13625#bib.bib24)\]\. Beyond providing rewards, our RMs maintain a list of automaton locations with clock valuations that serves as memory for state augmentation, which makes the rewards Markovian and compatible with off\-the\-shelf RL algorithms\. We formalize that any control policy learned using our RMs that achieves the maximum cumulative reward of11satisfies the given STL specification with probability11\.
- •We show that our approach outperforms existing methods by learning control policies faster and achieving higher satisfaction rates on long\-horizon specifications across several simulated experiments\.

The rest of the paper is organized as follows\. In Section[II](https://arxiv.org/html/2608.13625#S2), we review the related work, and in Section[III](https://arxiv.org/html/2608.13625#S3), we provide necessary background information and establish our notation\. We introduce our approach in Section[V](https://arxiv.org/html/2608.13625#S5)and present our experimental results in Section[VI](https://arxiv.org/html/2608.13625#S6)\. Finally, we draw conclusions in Section[VII](https://arxiv.org/html/2608.13625#S7)\.

## IIRelated Work

Prior work on controller synthesis from STL specifications falls into two categories, depending on whether a system model is assumed to be available: model\-based and model\-free\. We discuss prominent approaches and their drawbacks in both of these categories below\. We refer to\[[25](https://arxiv.org/html/2608.13625#bib.bib25)\]for detailed discussions\.

### II\-AModel\-Based Synthesis Approaches

Previous research has largely focused on establishing mixed\-integer programs \(MIPs\) for synthesizing controllers from STL specifications\[[26](https://arxiv.org/html/2608.13625#bib.bib26),[27](https://arxiv.org/html/2608.13625#bib.bib27),[28](https://arxiv.org/html/2608.13625#bib.bib28),[29](https://arxiv.org/html/2608.13625#bib.bib29)\]\. A common approach is to utilize model predictive control \(MPC\), where, at each time step, an optimal control policy over a finite horizon is obtained by the MIP formulated based on the system dynamics; this procedure is then repeated iteratively in a receding\-horizon manner\[[11](https://arxiv.org/html/2608.13625#bib.bib11)\]\. Such approaches have been extended to worst\-case scenarios\[[30](https://arxiv.org/html/2608.13625#bib.bib30)\], adversarial settings\[[12](https://arxiv.org/html/2608.13625#bib.bib12)\], systems under disturbance\[[31](https://arxiv.org/html/2608.13625#bib.bib31)\], uncertain or stochastic environments\[[32](https://arxiv.org/html/2608.13625#bib.bib32),[33](https://arxiv.org/html/2608.13625#bib.bib33),[34](https://arxiv.org/html/2608.13625#bib.bib34)\], resilient control\[[35](https://arxiv.org/html/2608.13625#bib.bib35)\], multiple objectives\[[36](https://arxiv.org/html/2608.13625#bib.bib36)\], and unbounded specifications\[[37](https://arxiv.org/html/2608.13625#bib.bib37)\]\.

A main issue in these MPC formalisms is that shorter planning horizons can lead to undesirable, myopic solutions, whereas longer horizons can be computationally expensive\. Some approaches propose using control barrier functions \(CBFs\) for computational efficiency; however, they typically consider only fragments of STL\[[38](https://arxiv.org/html/2608.13625#bib.bib38),[3](https://arxiv.org/html/2608.13625#bib.bib3)\], assume linearity\[[39](https://arxiv.org/html/2608.13625#bib.bib39)\], or require additional reachable set computation\[[40](https://arxiv.org/html/2608.13625#bib.bib40)\]\. Another line of studies, e\.g\.,\[[41](https://arxiv.org/html/2608.13625#bib.bib41),[42](https://arxiv.org/html/2608.13625#bib.bib42),[43](https://arxiv.org/html/2608.13625#bib.bib43),[44](https://arxiv.org/html/2608.13625#bib.bib44),[45](https://arxiv.org/html/2608.13625#bib.bib45),[46](https://arxiv.org/html/2608.13625#bib.bib46)\], proposes smoothed versions of robustness to enable gradient\-based optimization for faster computation, and has also explored combining these methods with neural networks\[[47](https://arxiv.org/html/2608.13625#bib.bib47),[48](https://arxiv.org/html/2608.13625#bib.bib48)\]via backpropagation\. Others include tube\-based\[[49](https://arxiv.org/html/2608.13625#bib.bib49),[50](https://arxiv.org/html/2608.13625#bib.bib50)\], prescribed performance control \(PPC\)\[[51](https://arxiv.org/html/2608.13625#bib.bib51),[52](https://arxiv.org/html/2608.13625#bib.bib52),[53](https://arxiv.org/html/2608.13625#bib.bib53)\], time\-interval decomposition\[[54](https://arxiv.org/html/2608.13625#bib.bib54),[55](https://arxiv.org/html/2608.13625#bib.bib55)\], system transformation\[[56](https://arxiv.org/html/2608.13625#bib.bib56)\], all introducing additional requirements, e\.g\., on STL formulas, or system dynamics\.

Overall, model\-based synthesis for STL has been an active research area, yielding many studies\. However, the history dependence of STL robustness scores remains a key obstacle in control synthesis\. This dependence increases the computational burden in MILP formalisms for longer planning horizons and can cause vanishing/exploding gradient issues when backpropagating through long histories\. Additionally, all these approaches rely on the assumption that a system model is available, limiting their applicability\.

### II\-BModel\-Free Learning Approaches

Modern RL has achieved strong empirical performance in learning reward\-maximizing controllers directly from interaction data, without requiring an explicit dynamics model\[[57](https://arxiv.org/html/2608.13625#bib.bib57)\]\. This success has motivated the use of RL for control synthesis from STL specifications, by employing robustness scores as the rewards in RL objective\[[58](https://arxiv.org/html/2608.13625#bib.bib58),[59](https://arxiv.org/html/2608.13625#bib.bib59),[60](https://arxiv.org/html/2608.13625#bib.bib60)\]\. A central challenge is that the satisfaction rates and robustness scores are calculated over the entirety of traces, making them history\-dependent, thereby breaking the Markov property assumed by most RL formulations\. This non\-Markovian dependence can destabilize learning and may lead to poor performance, or even divergence, particularly for value\-based methods such as Q\-learning and actor\-critic algorithms\.

A common technique to restore Markovian structure is augmenting the state space with the recent history of the visited states, where the required history length is determined by the temporal structure of the STL specification\[[16](https://arxiv.org/html/2608.13625#bib.bib16),[17](https://arxiv.org/html/2608.13625#bib.bib17),[61](https://arxiv.org/html/2608.13625#bib.bib61),[62](https://arxiv.org/html/2608.13625#bib.bib62)\]\. While conceptually simple, this approach can dramatically increase the state dimension, and the resulting complexity becomes prohibitive for long\-horizon specifications\. To mitigate this blow\-up, several works restrict attention to tractable fragments of STL or introduce alternative intermediates that avoid full\-history augmentation\. Examples include augmenting the state with compact bookkeeping variables for limited nesting\[[18](https://arxiv.org/html/2608.13625#bib.bib18),[19](https://arxiv.org/html/2608.13625#bib.bib19),[20](https://arxiv.org/html/2608.13625#bib.bib20)\], prescribed performance control formulations\[[21](https://arxiv.org/html/2608.13625#bib.bib21)\], sampling\-based planning methods\[[63](https://arxiv.org/html/2608.13625#bib.bib63)\], learning with control barrier functions\[[22](https://arxiv.org/html/2608.13625#bib.bib22)\], and funnel\-based control\[[64](https://arxiv.org/html/2608.13625#bib.bib64)\]\. Despite these advances, there remains no model\-free approach that scales to full STL while avoiding intractable history\-based state augmentation\.

A line of work closely related to ours focuses on crafting automata\-based rewards for RL by compiling temporal\-logic specifications into automata and learning over the product system\. Most existing methods build rewards from omega automata obtained from logics without real\-time constraints such as linear temporal logic \(LTL\), e\.g\.,\[[65](https://arxiv.org/html/2608.13625#bib.bib65),[66](https://arxiv.org/html/2608.13625#bib.bib66),[67](https://arxiv.org/html/2608.13625#bib.bib67),[68](https://arxiv.org/html/2608.13625#bib.bib68),[69](https://arxiv.org/html/2608.13625#bib.bib69),[70](https://arxiv.org/html/2608.13625#bib.bib70),[71](https://arxiv.org/html/2608.13625#bib.bib71),[72](https://arxiv.org/html/2608.13625#bib.bib72),[73](https://arxiv.org/html/2608.13625#bib.bib73)\], and a few consider reward shaping for a given timed automaton\[[74](https://arxiv.org/html/2608.13625#bib.bib74)\], a formalism extending transition systems with clock variables and time constraints\. To the best of our knowledge, however, prior work has not constructed rewards from an automaton directly derived from STL in a way that is compatible with standard RL settings\. While STL can be translated into continuous\-time signal transducers\[[13](https://arxiv.org/html/2608.13625#bib.bib13)\], those representations are not well matched to RL, where the agent typically receives point\-wise state observations at discrete decision times\. In this work, we translate STL specifications into OCATAs\[[23](https://arxiv.org/html/2608.13625#bib.bib23)\]and design rewards to accommodate their conjunctive branching structure and the associated acceptance condition, which can be incorporated into RL via augmentation with automaton states and clock variables\.

## IIIPreliminaries

### III\-ASemi\-Markov Decision Processes

We model the interaction between controllers and the environments as SMDPs, which extend standard MDPs by allowing stochastic, real\-valued durations between successive observations\.

###### Definition 1\(SMDP\)

An SMDP is a tupleℳ=\(S,s0,A,P\)\\mathcal\{M\}=\(S,s\_\{0\},A,P\), whereSSis a set of states,s0s\_\{0\}is the initial state,AAis a set of actions111We primarily consider continuous state and action spaces, although our approach also applies to discrete settings\., andPPis a probabilistic transition function\. We writeP\(s′,τ′∣s,a\)P\(s^\{\\prime\},\\tau^\{\\prime\}\\mid s,a\)for the probability density \(or probability mass, in the discrete case\) of transitioning from the states∈Ss\\in Sto the states′∈Ss^\{\\prime\}\\in Swhen taking actiona∈Aa\\in A, after a nonnegative elapsed timeτ′∈ℝ≥0\\tau^\{\\prime\}\\in\\mathbb\{R\}\_\{\\geq 0\}\.

The time valueτ\\taucaptures the duration between observingssand observings′s^\{\\prime\}, including both transition and dwelling time; this timing information is explicit in SMDPs, whereas it is abstracted away in discrete\-time MDPs\.

A control policyπ:\(S×ℝ≥0\)\+↦A\\pi:\(S\\times\\mathbb\{R\}\_\{\\geq 0\}\)^\{\+\}\\mapsto Afor an SMDPℳ\\mathcal\{M\}is a mapping that selects an action based on the history of states with duration stamps\. Starting from the initial pair222For simplicity, we assume a fixed initial states0s\_\{0\}and durationτ0=0\\tau\_\{0\}=0\. Our approach extends directly to random initial states and duration\.\(s0,τ0\)\(s\_\{0\},\\tau\_\{0\}\), execution of a policyπ\\piin an SMDPℳ\\mathcal\{M\}generates a*timed path*, an infinite sequence of duration\-stamped statesσ≔\(s0,τ0\)​\(s1,τ1\)​…\\sigma\\coloneqq\(s\_\{0\},\\tau\_\{0\}\)\(s\_\{1\},\\tau\_\{1\}\)\\dotsaccording to the induced Markov chain \(MC\)ℳπ\\mathcal\{M\}\_\{\\pi\}, where the incrementτt\\tau\_\{t\}is the duration between observations ofsts\_\{t\}andst\+1s\_\{t\+1\}for allt\>0t\>0\. We useσ⁡\[t\]\\sigma\[t\],σ\[:t\]\\sigma\[\{:\}t\], andσ\[t:\]\\sigma\[t\{:\}\]to denote the timed state\(st,τt\)\(s\_\{t\},\\tau\_\{t\}\), the prefix\(s0,τ0\)​…​\(st,τt\)\(s\_\{0\},\\tau\_\{0\}\)\\dots\(s\_\{t\},\\tau\_\{t\}\), and the suffix\(st,τt\)​\(st\+1,τt\+1\)​…\(s\_\{t\},\\tau\_\{t\}\)\(s\_\{t\+1\},\\tau\_\{t\+1\}\)\\dots, respectively\.

For a given bounded reward function333We consider state\-based reward functions for simplicity; our approach is compatible with state\-action\-based reward functions as well\.R:\(S×ℝ≥0\)\+↦ℝR:\(S\\times\\mathbb\{R\}\_\{\\geq 0\}\)^\{\+\}\\mapsto\\mathbb\{R\}mapping timed path prefixes to real\-valued scalars, and a given discount factorγ∈\[0,1\)\\gamma\\in\[0,1\), the returnG⁡\(σ\)G\(\\sigma\)of a pathσ\\sigmais the sum of discounted rewardsG\(σ\)=∑t=0∞γtR\(σ\[:t\]\)G\(\\sigma\)=\\sum\_\{t=0\}^\{\\infty\}\\gamma^\{t\}R\(\\sigma\[\{:\}t\]\)\. In standard formulations, discounting uses a fixed factorγ\\gamma; but this can be relaxed to allow for state\-dependent discounting as described in\[[67](https://arxiv.org/html/2608.13625#bib.bib67)\]\.

The objective in an SMDPℳ\\mathcal\{M\}with a reward functionRRis to find an optimal policy that maximizes expected returnπ∗=argmaxπ​𝔼σ∼ℳπ​\[G⁡\(σ\)\]\\pi^\{\*\}=\\mathrm\{argmax\}\_\{\\pi\}\\mathbb\{E\}\_\{\\sigma\\sim\\mathcal\{M\}\_\{\\pi\}\}\\left\[G\(\\sigma\)\\right\]\. When rewards are Markovian \(i\.e\., the reward functionR:S×ℝ≥0↦ℝR:S\\times\\mathbb\{R\}\_\{\\geq 0\}\\mapsto\\mathbb\{R\}maps based only on the last observed state and duration\), it is sufficient to consider memoryless policiesπ:S↦A\\pi:S\\mapsto A, and an optimal policy can be learned using off\-the\-shelf RL tools when the transition functionPPis unknown\. However, in history\-dependent settings \(e\.g\., STL objectives\), applying RL typically requires a Markovian reward design, which can be achieved by augmenting the state space with a tractable set of memory variables\.

### III\-BEvent\-Based Signal Temporal Logic

STL provides a language to specify temporal properties of real\-valued observations using predicates, Boolean connectives, and temporal operators\[[1](https://arxiv.org/html/2608.13625#bib.bib1)\]\.

###### Definition 2

An STL predicate is an inequalityμ≥0\\mu\\geq 0, whereμ:S→ℝ\\mu:S\\to\\mathbb\{R\}is a function mapping a state to a scalar\. STL specifications can be formulated recursively by the following grammar:

φ≔μ≥0​∣¬φ∣​φ1∧φ2\|φ1​UI​φ2,μ∈Λ,\\varphi\\coloneqq\\mu\\geq 0\\ \\mid\\ \\neg\\varphi\\ \\mid\\ \\varphi\_\{1\}\\wedge\\varphi\_\{2\}\\ \\mid\\ \\varphi\_\{1\}\\,\\mathrm\{U\}\_\{I\}\\,\\varphi\_\{2\}\\ ,\\quad\\mu\\in\\Lambda\\,,\(1\)where¬\\negis negation,∧\\wedgeis conjunction,U\\mathrm\{U\}is the until operator, andI⊆ℝ≥0I\\subseteq\\mathbb\{R\}\_\{\\geq 0\}is a time interval \(closed, open, or half\-open\) with nonnegative rational or infinite endpoints \(ℚ≥0∪\{∞\}\\mathbb\{Q\}\_\{\\geq 0\}\\cup\\\{\\infty\\\}\), andΛ\\Lambdais the set of predicate functions\.

We also use the standard derived operators: disjunctionφ1∨φ2:=¬\(¬φ1∧¬φ2\)\\varphi\_\{1\}\\vee\\varphi\_\{2\}:=\\neg\(\\neg\\varphi\_\{1\}\\land\\neg\\varphi\_\{2\}\), implicationφ1⟹φ2:=¬φ1∨φ2\\varphi\_\{1\}\\implies\\varphi\_\{2\}:=\\neg\\varphi\_\{1\}\\lor\\varphi\_\{2\}, true⊤≔φ∨¬φ\\top\\coloneqq\\varphi\\vee\\neg\\varphi, finallyFI​φ:=⊤UI​φF\_\{I\}\\varphi:=\\top\\ \\mathrm\{U\}\_\{I\}\\varphi, and globallyGI​φ:=¬FI​¬φG\_\{I\}\\varphi:=\\neg F\_\{I\}\\neg\\varphi\. WhenI=\[0,∞\)I=\[0,\\infty\), we omit the interval subscript from temporal operators\.

We adopt an*event\-based*semantics defined over infinite timed pathsσ=\(s0,τ0\)​\(s1,τ1\)​…\\sigma=\(s\_\{0\},\\tau\_\{0\}\)\(s\_\{1\},\\tau\_\{1\}\)\\dots\(rather than continuous\-time signal semantics\) to align with standard RL formalisms\. We writeσ\[t:\]⊧φ\\sigma\[t\{:\}\]\\models\\varphito denote that the timed suffixσ\[t:\]\\sigma\[t\{:\}\]satisfies the specificationφ\\varphi\. Following the formulation in\[[75](https://arxiv.org/html/2608.13625#bib.bib75)\]for metric interval temporal logic \(MITL\), we define the semantics recursively by

σ\[t:\]⊧μ≥0\\displaystyle\\sigma\[t\{:\}\]\\models\\mu\\geq 0⇔μ⁡\(st\)≥0\\displaystyle\\iff\\mu\(s\_\{t\}\)\\geq 0σ\[t:\]⊧¬φ\\displaystyle\\sigma\[t\{:\}\]\\models\\neg\\varphi⇔σ\[t:\]⊧̸φ\\displaystyle\\iff\\sigma\[t\{:\}\]\\not\\models\\varphiσ\[t:\]⊧φ1∧φ2\\displaystyle\\sigma\[t\{:\}\]\\models\\varphi\_\{1\}\\wedge\\varphi\_\{2\}⇔σ\[t:\]⊧φ1andσ\[t:\]⊧φ2\\displaystyle\\iff\\sigma\[t\{:\}\]\\models\\varphi\_\{1\}\\text\{ and \}\\sigma\[t\{:\}\]\\models\\varphi\_\{2\}σ\[t:\]⊧φ1𝒰Iφ2\\displaystyle\\sigma\[t\{:\}\]\\models\\varphi\_\{1\}\\mathrel\{\\mathcal\{U\}\_\{I\}\}\\varphi\_\{2\}⇔∃is\.t\.τi−τt∈I,σ\[i:\]⊧φ2,\\displaystyle\\iff\\exists i\\text\{ s\.t\. \}\\tau\_\{i\}\-\\tau\_\{t\}\\in I,\\ \\sigma\[i\{:\}\]\\models\\varphi\_\{2\},and∀t≤j<i,σ\[j:\]⊧φ1\.\\displaystyle\\hskip 37\.00002pt\\text\{ and \}\\forall t\\leq j<i,\\ \\sigma\[j\{:\}\]\\models\\varphi\_\{1\}\.Similarly, we define the semantics of spatial robustness scores as follows:

ρ\(σ\[t:\],μ≥0\)=μ\(st\)\\displaystyle\\rho\(\\sigma\[t\{:\}\],\\ \\mu\\geq 0\)=\\mu\(s\_\{t\}\)ρ\(σ\[t:\]¬φ\)=−ρ\(σ\[t:\]φ\)\\displaystyle\\rho\(\\sigma\[t\{:\}\]\\ \\neg\\varphi\)=\-\\rho\(\\sigma\[t\{:\}\]\\ \\varphi\)ρ\(σ\[t:\],φ1∧φ2\)=max\{ρ\(σ\[t:\],φ1\),ρ\(σ\[t:\],φ2\)\}\\displaystyle\\rho\(\\sigma\[t\{:\}\],\\ \\varphi\_\{1\}\\wedge\\varphi\_\{2\}\)=\\max\\\{\\rho\(\\sigma\[t\{:\}\],\\ \\varphi\_\{1\}\),\\ \\rho\(\\sigma\[t\{:\}\],\\ \\varphi\_\{2\}\)\\\}ρ\(σ\[t:\],φ1𝒰Iφ2\)=supi∈\{k\|τk−τt∈I\}\\displaystyle\\rho\(\\sigma\[t\{:\}\],\\ \\varphi\_\{1\}\\mathrel\{\\mathcal\{U\}\_\{I\}\}\\varphi\_\{2\}\)=\\sup\_\{i\\in\\\{k\|\\tau\_\{k\}\-\\tau\_\{t\}\\in I\\\}\}min\{ρ\(σ\[i:\],φ2\),inft≤j<iρ\(σ\[j:\]φ1\)\}\.\\displaystyle\\hskip 70\.0001pt\\min\\left\\\{\\rho\(\\sigma\[i\{:\}\],\\ \\varphi\_\{2\}\),\\ \\inf\_\{t\\leq j<i\}\\rho\(\\sigma\[j\{:\}\]\\ \\varphi\_\{1\}\)\\right\\\}\.The inherent history\-dependence due toinf\\mathrm\{inf\}andsup\\mathrm\{sup\}operations applied over path fragments makes the spatial robustness scores unsuitable for serving as Markovian rewards in RL for long\-horizon specifications\. Thus, we do not utilize these robustness scores directly in our approach; instead, we employ them for evaluation and comparison\.

## IVProblem Formulation

We study the efficient learning of control policies that satisfy given STL specifications in unknown environments\. We adopt SMDPs as the system formalism\. Unlike standard discrete\-time MDPs, in which time is abstracted as a sequence of integer\-valued steps, and continuous\-time MDPs, in which states are observed and actions are selected continuously, SMDPs explicitly represent the elapsed time between consecutive observations\. This representation enables real\-time constraints to be expressed through event\-based STL while retaining compatibility with off\-the\-shelf RL algorithms that operate on pointwise observations\.

A key challenge in this setting is accounting for stochastic transitions\. Repeated executions of the same policy may produce different successor states and transition durations, thereby generating different timed paths\. Our primary objective is therefore to learn a policy that maximizes the satisfaction probability, defined as the probability that a timed path generated under the policy satisfies the STL specification\. As a secondary objective, we incorporate robustness into this probability\-maximization framework by modeling probabilistic satisfaction of predicates under supposed random perturbations\. We formalize the resulting joint problem as follows\.

###### Problem 1

Given an SMDPℳ\\mathcal\{M\}with an unknown transition functionPPand an STL specificationφ\\varphi, design a mechanismℛφ\\mathcal\{R\}\_\{\\varphi\}that generates memory states and corresponding Markovian rewards, thereby enabling efficient RL to obtain an optimal policyπ∗\\pi^\{\*\}that maximizes the probability of satisfyingφ\\varphi:

π∗≔\\displaystyle\\pi^\{\*\}\\coloneqqargmaxπ​Prσ∼ℳπ⁡\(σ⊧φ\)\\displaystyle\\mathrm\{argmax\}\_\{\\pi\}\\Pr\\nolimits\_\{\\sigma\\sim\\mathcal\{M\}\_\{\\pi\}\}\(\\sigma\\models\\varphi\)\(2\)Here,Pr⁡\(⋅\)\\Pr\(\\cdot\)accounts for both \(i\) the stochasticity of a timed pathσ\\sigmagenerated by the SMDPℳ\\mathcal\{M\}under a policyπ\\piand \(ii\) the probabilistic satisfaction of the specificationφ\\varphibyσ\\sigmadue to modeled random perturbations of its predicates\.

Since we consider stochastic environments, the proposed formulation naturally focuses on maximizing satisfaction probability\. We do not optimize the expected robustness degree, as doing so may favor policies that achieve high robustness on a small subset of trajectories while frequently violating the specification\. Instead, we use expected robustness only as an additional evaluation metric alongside satisfaction probability\. Nevertheless, our probabilistic interpretation of predicate satisfaction provides a principled and tunable means of incorporating robustness into the probability\-maximization objective\.

l0l\_\{0\}start∨\\veel1l\_\{1\}∧\\wedgel2l\_\{2\}l3l\_\{3\}l4l\_\{4\}α=⊤\\alpha\{=\}\\topκ=⊤\\kappa\{=\}\\top／​¢=⊥\\mathchoice\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\displaystyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\textstyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 2\.625pt\\kern\-4\.45831pt$\\scriptstyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 1\.875pt\\kern\-3\.95834pt$\\scriptscriptstyle\\not$\\hss\}\{\\cent\}\}\}\{=\}\\bot／​¢=⊥\\mathchoice\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\displaystyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\textstyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 2\.625pt\\kern\-4\.45831pt$\\scriptstyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 1\.875pt\\kern\-3\.95834pt$\\scriptscriptstyle\\not$\\hss\}\{\\cent\}\}\}\{=\}\\botα=\`​\`​\|x−xf\|≤1​"\\alpha\{=\}\`\`\|x\{\-\}x\_\{\\textit\{f\}\}\|\{\\leq\}1"κ=⊤\\kappa\{=\}\\top／​¢=⊥\\mathchoice\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\displaystyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\textstyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 2\.625pt\\kern\-4\.45831pt$\\scriptstyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 1\.875pt\\kern\-3\.95834pt$\\scriptscriptstyle\\not$\\hss\}\{\\cent\}\}\}\{=\}\\botα=\`​\`​\|x−xf\|\>1​"\\alpha\{=\}\`\`\|x\{\-\}x\_\{\\textit\{f\}\}\|\{\>\}1"κ=⊤\\kappa\{=\}\\top／​¢=⊥\\mathchoice\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\displaystyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\textstyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 2\.625pt\\kern\-4\.45831pt$\\scriptstyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 1\.875pt\\kern\-3\.95834pt$\\scriptscriptstyle\\not$\\hss\}\{\\cent\}\}\}\{=\}\\bot／​¢=⊤\\mathchoice\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\displaystyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\textstyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 2\.625pt\\kern\-4\.45831pt$\\scriptstyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 1\.875pt\\kern\-3\.95834pt$\\scriptscriptstyle\\not$\\hss\}\{\\cent\}\}\}\{=\}\\topresetα=\`​\`​\|x−xf\|\>1​"\\alpha\{=\}\`\`\|x\{\-\}x\_\{\\textit\{f\}\}\|\{\>\}1"κ=\`​\`​¢≤1​"\\kappa\{=\}\`\`\\cent\{\\leq\}1"／​¢=⊥\\mathchoice\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\displaystyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\textstyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 2\.625pt\\kern\-4\.45831pt$\\scriptstyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 1\.875pt\\kern\-3\.95834pt$\\scriptscriptstyle\\not$\\hss\}\{\\cent\}\}\}\{=\}\\botα=\`​\`​\|x−xf\|≤1​"\\alpha\{=\}\`\`\|x\{\-\}x\_\{\\textit\{f\}\}\|\{\\leq\}1"κ=\`​\`​¢≤1​"\\kappa\{=\}\`\`\\cent\{\\leq\}1"／​¢=⊥\\mathchoice\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\displaystyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\textstyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 2\.625pt\\kern\-4\.45831pt$\\scriptstyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 1\.875pt\\kern\-3\.95834pt$\\scriptscriptstyle\\not$\\hss\}\{\\cent\}\}\}\{=\}\\botα=⊤\\alpha\{=\}\\topκ=\`​\`​¢\>1​"\\kappa\{=\}\`\`\\cent\{\>\}1"／​¢=⊥\\mathchoice\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\displaystyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\textstyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 2\.625pt\\kern\-4\.45831pt$\\scriptstyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 1\.875pt\\kern\-3\.95834pt$\\scriptscriptstyle\\not$\\hss\}\{\\cent\}\}\}\{=\}\\botα=⊤\\alpha\{=\}\\topκ=⊤\\kappa\{=\}\\topα=⊤\\alpha\{=\}\\topκ=⊤\\kappa\{=\}\\top

Fig\. 1:Illustration of an OCATA derived from the STL formulaφf=F​G​\(¬\`​\`​μf≥0​"⟹F\[0,1\]​\`​\`​μf≥0​"\)\\varphi\_\{f\}=FG\\big\(\\neg\`\`\\mu\_\{f\}\{\\geq\}0"\\implies F\_\{\[0,1\]\}\`\`\\mu\_\{f\}\{\\geq\}0"\\big\)\. Here,μf​\(s\)≔1−\|x−xf\|\\mu\_\{f\}\(s\)\\coloneqq 1\-\|x\{\-\}x\_\{\\textit\{f\}\}\|is a predicate function measuring how close the position componentxxof a statessis to the target positionxfx\_\{\\textit\{f\}\}\. Larger circles\(L=\{l0,l1,l2,l3,l4\}\)\(L=\\\{l\_\{0\},l\_\{1\},l\_\{2\},l\_\{3\},l\_\{4\}\\\}\)represent automaton locations with accepting locations shown as double circles\(\{l1,l3\}\)\(\\\{l\_\{1\},l\_\{3\}\\\}\)\. Arrows represent transitions; and smaller circles,∨\\veeand∧\\wedge, indicate disjunctive \(nondeterministic/existential\) and conjunctive \(universal\) branching, respectively\. Symbolsα\\alpha,κ\\kappa,／​¢\\mathchoice\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\displaystyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\textstyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 2\.625pt\\kern\-4\.45831pt$\\scriptstyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 1\.875pt\\kern\-3\.95834pt$\\scriptscriptstyle\\not$\\hss\}\{\\cent\}\}\}, and¢\\centdenote input letters, clock constraints, clock\-reset flags, and the clock variable, respectively\.
## VReward Machines for Signal Temporal Logic

We address Problem[1](https://arxiv.org/html/2608.13625#Thmproblem1)by introducing extended RMs constructed for OCATAs derived from the STL specifications\. Our RMs extend the standard definition\[[76](https://arxiv.org/html/2608.13625#bib.bib76)\]by allowing nondeterministic, conjunctive, and probabilistic transitions, together with the Büchi acceptance condition, in order to capture the event\-based semantics of full STL under observation perturbations\. We then provide a procedure for composing the product of an SMDP and an RM, yielding an augmented model with Markovian rewards\. Finally, we formalize that any policy achieving the maximum expected return of 1 under these rewards is guaranteed to satisfy the STL specification with probability 1\. We describe each step in detail in the following subsections\.

### V\-AOne\-Clock Alternating Timed Automata

Our procedure begins by translating a given specification to an OCATA with a Büchi acceptance condition \(repeated reachability\) as in\[[23](https://arxiv.org/html/2608.13625#bib.bib23)\]444Although this construction is presented for MITL, it applies directly to STL as well\.\. OCATAs are timed automata with a single clock variable that allow for disjunctive and conjunctive transitions\. We first introduce the grammar of clock constraints used in the OCATA construction\. LetKKbe the finite set of clock\-constraint formulas generated by

κ≔¢<c\|¢≤c​∣¬κ∣​κ1∧κ2\\displaystyle\\kappa\\coloneqq\\ \\cent<c\\ \\mid\\ \\cent\\leq c\\ \\mid\\ \\neg\\kappa\\ \\mid\\ \\kappa\_\{1\}\\wedge\\kappa\_\{2\}\(3\)where¢\\centdenotes the single clock variable, andc∈ℚ≥0c\\in\\mathbb\{Q\}\_\{\\geq 0\}is an arbitrary nonnegative rational number\. Other relations \(\{\>,≥,=,≠\}\\\{\>,\\geq,=,\\neq\\\}\) and logical operators \(∨,⟹,⊤\\vee,\\implies,\\top\) can be derived as usual\.

In a deterministic one\-clock timed automaton, receiving an inputα∈Σ\\alpha\\in\\Sigmaunder a satisfied clock constraintκ∈K\\kappa\\in Ktriggers a unique transition from a current locationl∈Ll\\in Lto a destinationl′∈Ll^\{\\prime\}\\in LwhereΣ\\Sigmais a finite alphabet andLLis a finite set of locations\. Each transition is additionally labeled with a reset flag／​¢∈\{⊤,⊥\}\\mathchoice\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\displaystyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\textstyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 2\.625pt\\kern\-4\.45831pt$\\scriptstyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 1\.875pt\\kern\-3\.95834pt$\\scriptscriptstyle\\not$\\hss\}\{\\cent\}\}\}\\ \\in\\\{\\top,\\bot\\\}indicating whether the clockxxis reset with the transition\. In an OCATA, however, a\(l,α,κ\)\(l,\\alpha,\\kappa\)triple may induce not only a single transition but also disjunctive \(∨\\vee\) and conjunctive \(∧\\wedge\) combinations of transitions\. To represent such branching behavior, we define a finite set of destination formulasDDusing the grammar

d≔\(l,／​¢\)​∣d1∧d2∣​d1∨d2,\\displaystyle d\\coloneqq\\ \(l,\\mathchoice\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\displaystyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\textstyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 2\.625pt\\kern\-4\.45831pt$\\scriptstyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 1\.875pt\\kern\-3\.95834pt$\\scriptscriptstyle\\not$\\hss\}\{\\cent\}\}\}\)\\ \\mid\\ d\_\{1\}\\wedge d\_\{2\}\\ \\mid\\ d\_\{1\}\\vee d\_\{2\},\(4\)wherel∈Ll\\in Lis a destination location and／​¢∈\{⊤,⊥\}\\mathchoice\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\displaystyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\textstyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 2\.625pt\\kern\-4\.45831pt$\\scriptstyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 1\.875pt\\kern\-3\.95834pt$\\scriptscriptstyle\\not$\\hss\}\{\\cent\}\}\}\\ \\in\\\{\\top,\\bot\\\}is the clock\-reset flag\. We now provide the definition of an OCATA:

###### Definition 3

An OCATA is a tuple𝒜=\(L,l0,Σ,K,D,δ,F\)\\mathcal\{A\}=\(L,l\_\{0\},\\Sigma,K,D,\\allowbreak\\delta,F\), whereLLis a set of locations,l0∈Ll\_\{0\}\\in Lis the initial location,Σ=2Λ\\Sigma=2^\{\\Lambda\}is an alphabet whereΛ\\Lambdais a predicate set from \([1](https://arxiv.org/html/2608.13625#S3.E1)\),KKis a set of clock constraints defined by \([3](https://arxiv.org/html/2608.13625#S5.E3)\),DDis a set of destination formulas defined by \([4](https://arxiv.org/html/2608.13625#S5.E4)\),δ:L×Σ×K→D\\delta:L\\times\\Sigma\\times K\\to Dis a total transition function, andF⊆LF\\subseteq Lis a set of accepting locations\.

An OCATA starts in the initial locationl0l\_\{0\}with a clock valuex=0x=0, and makes transitions as observations from the SMDP are received\. An OCATA state is determined by a pairq=\(l,v\)q=\(l,v\), wherel∈Ll\\in Lis the current location andv∈ℝ≥0v\\in\\mathbb\{R\}\_\{\\geq 0\}is the current clock valuation\. After observingσ⁡\[t\]=\(st,τt\)\\sigma\[t\]=\(s\_\{t\},\\tau\_\{t\}\)at time stepttin a locationll, the OCATA advances the clock value byτt\\tau\_\{t\}, computes the set of satisfied predicatesαt=\{μ∈Λ∣μ⁡\(st\)\>0\}∈Σ\\alpha\_\{t\}=\\\{\\mu\\in\\Lambda\\mid\\mu\(s\_\{t\}\)\>0\\\}\\in\\Sigma, and selects the clock constraintκv∈K\\kappa\_\{v\}\\in Kthat is satisfied under the updated valuationvv\. The OCATA then makes transitions according to the destination formulad=δ⁡\(l,α,κ\)d=\\delta\(l,\\alpha,\\kappa\), where the nature of the transitions is determined by the∨\\veeand∧\\wedgeoperators in the formuladd\. The disjunction operator∨\\veeinduces nondeterministic transitions \(existential choice\) where at least one transition should lead to acceptance\. In contrast, the conjunctive operator∧\\wedgespawns new threads of computations by creating different copies of OCATA states \(universal choice\) where each copy must lead to acceptance\.

The semantics of transitions are formally defined based on acceptance as follows\. An OCATA𝒜\\mathcal\{A\}in an automaton state\(l,v\)\(l,v\)accepts the timed suffixσ\[t:\]\\sigma\[t\{:\}\]with respect to a destination formuladdif and only if \(iff\) one of the following recursively holds:

- •d=d1∨d2d=d\_\{1\}\\vee d\_\{2\}and𝒜\\mathcal\{A\}in\(l,v\)\(l,v\)acceptsσ\[t:\]\\sigma\[t\{:\}\]ford1d\_\{1\}ord2d\_\{2\};
- •d=d1∧d2d=d\_\{1\}\\wedge d\_\{2\}and𝒜\\mathcal\{A\}in\(l,v\)\(l,v\)acceptsσ\[t:\]\\sigma\[t\{:\}\]ford1d\_\{1\}andd2d\_\{2\};
- •d=\(l′,／​¢\)d=\(l^\{\\prime\},\\mathchoice\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\displaystyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\textstyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 2\.625pt\\kern\-4\.45831pt$\\scriptstyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 1\.875pt\\kern\-3\.95834pt$\\scriptscriptstyle\\not$\\hss\}\{\\cent\}\}\}\)and𝒜\\mathcal\{A\}in\(l′,v′\)\(l^\{\\prime\},v^\{\\prime\}\)withv′=\[¬／​¢\]v\+\(τt\+1−τt\)v^\{\\prime\}=\[\\neg\\hskip\-1\.99997pt\\mathchoice\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\displaystyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\textstyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 2\.625pt\\kern\-4\.45831pt$\\scriptstyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 1\.875pt\\kern\-3\.95834pt$\\scriptscriptstyle\\not$\\hss\}\{\\cent\}\}\}\\hskip 1\.00006pt\]v\+\(\\tau\_\{t\+1\}\-\\tau\_\{t\}\)acceptsσ\[t\+1:\]\\sigma\[t\{\+\}1\{:\}\]with respect tod′=δ⁡\(l′,αt\+1,κv′\)d^\{\\prime\}=\\delta\(l^\{\\prime\},\\alpha\_\{t\+1\},\\kappa\_\{v^\{\\prime\}\}\);

where\[¬／​¢\]\[\\neg\\hskip\-1\.99997pt\\mathchoice\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\displaystyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\textstyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 2\.625pt\\kern\-4\.45831pt$\\scriptstyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 1\.875pt\\kern\-3\.95834pt$\\scriptscriptstyle\\not$\\hss\}\{\\cent\}\}\}\\hskip 1\.00006pt\]is00if／​¢=⊤\\mathchoice\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\displaystyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\textstyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 2\.625pt\\kern\-4\.45831pt$\\scriptstyle\\not$\\hss\}\{\\cent\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 1\.875pt\\kern\-3\.95834pt$\\scriptscriptstyle\\not$\\hss\}\{\\cent\}\}\}\\ =\\topelse11\. A run of an OCATA induced by a timed path is a computation tree, due to the threads spawned by conjunctive transitions\. Moreover, disjunctive transitions introduce nondeterminism, yielding multiple runs from which the OCATA may choose\. A run is accepting iff every infinite computational path visits some accepting location inFFinfinitely often \(the Büchi condition\)\. The OCATA accepts a timed path iff there exists an accepting run induced by that timed path\.

Fig\.[1](https://arxiv.org/html/2608.13625#S4.F1)illustrates an OCATA derived from an STL formula\. The formula intuitively requires that the target region, defined as the set of positions within distance11of the targetxfx\_\{\\textit\{f\}\}, is eventually reached and, thereafter, whenever this region is left, it must be returned to within11time unit\. The disjunction∨\\veeintroduces a nondeterministic choice between transitions tol0l\_\{0\}andl1l\_\{1\}\. Transitioning tol1l\_\{1\}corresponds to guessing that the target region has been reached and that any future deviation can be corrected within the required time bound; transitioning tol0l\_\{0\}represents the opposite guess\. When an observation indicates that the region is left, the conjunction∧\\wedgespawns two branches tol1l\_\{1\}andl2l\_\{2\}\. Thel2l\_\{2\}branch enforces the11\-time\-unit return condition by setting a timer via resetting the clock: if the region is re\-entered in time, the OCATA moves to the accepting sinkl3l\_\{3\}; otherwise, it moves to the rejecting sinkl4l\_\{4\}\. Thel1l\_\{1\}branch keeps the OCATA inl1l\_\{1\}to handle potential future departures, and its induced computation path is accepting asl1l\_\{1\}is an accepting location\. However, because∧\\wedgerequires universal acceptance, all computation paths generated by thel2l\_\{2\}branch must also be accepting, ensuring that the region is always returned to within11time unit\. Next, we explain how to construct an RM that reflects this OCATA acceptance condition\.

### V\-BReward Machine Construction

We construct RMs for given STL specifications based on the OCATAs derived from the specifications\. The main challenge is to design rewards that \(i\) encode the Büchi acceptance condition requiring some accepting locations to be visited infinitely often, \(ii\) handle the disjunctive and conjunctive transitions, and \(iii\) incorporate robustness to state perturbations\.

We adopt the state\-based rewarding and discounting scheme of\[[67](https://arxiv.org/html/2608.13625#bib.bib67)\]\. The idea is to provide a reward ofr∈\(0,1\]r\\in\(0,1\]whenever an accepting locationl∈Fl\\in Fis visited, and a reward of00for visiting other locationsl∈L∖Fl\\in L\\setminus F\. The future rewards are discounted with factors ofγ=1−r\\gamma=1\-rin accepting andγ′=1−r2\\gamma^\{\\prime\}=1\-r^\{2\}in non\-accepting locations, reflecting the fact that visiting non\-accepting locations is irrelevant to satisfying the Büchi condition\. Maximizing the expected return under these rewards and discount factors corresponds to maximizing the probability of satisfying the Büchi condition\[[67](https://arxiv.org/html/2608.13625#bib.bib67)\]\.

The nondeterminism in OCATAs due to the disjunctive transitions can be encoded asϵ\\epsilon\-actions in RMs that the RL agent can select during learning\. In such formulations, the expected return establishes a lower bound on the satisfaction probability in general; and if the OCATA is limit\-deterministic in a suitable way, then the lower bound becomes equality\[[65](https://arxiv.org/html/2608.13625#bib.bib65)\]\. To the best of our knowledge, it is not known whether STL \(or MITL\) formulas can always be translated into OCATAs that are limit\-deterministic in this way\. Accordingly, we focus on the lower\-bound guarantee rather than equivalence\.

In order to capture the conjunctive transitions, we keep track of the automaton states for each copy of the OCATA created by conjunctions in a memory list, and the average value of the rewards associated with each copy is provided as a joint reward\. This ensures that the maximization of the reward in each copy maximizes the joint return\. In order to establish a tractable probabilistic framework, we extend this formalism by associating each copy with a probability\. Specifically whenever two copies are spawned, they split the probability associated with their parent\. This allows us to keep a single copy for each clock valuation; the conjunctive splits are just going to affect the probabilities over locations if they do not reset the clock; only clock resets will trigger a copy\.

To handle conjunctive transitions, we track the automaton state for each OCATA copy spawned by conjunctions using a memory list\. We then provide a joint reward given by the average of the rewards across these copies\. This construction ensures that maximizing the return in each copy contributes to maximizing the joint return\. To obtain a tractable probabilistic representation, we associate each copy with a probability mass: whenever a conjunction spawns multiple copies, the parent probability is split among the children\. The conjunctive branching that does not reset the clock only redistributes probability mass over locations; in contrast, clock resets trigger the creation of a new copy \(i\.e\., a new memory entry\)\. This lets us maintain a single copy per clock valuation\.

Finally, we incorporate robustness by introducing pseudo\-perturbations in evaluations of STL predicates\. Concretely, we treat the predicate function outputμ⁡\(s\)\\mu\(s\)as if it were observed through additive noise, e\.g\., drawn from a normal or logistic distribution, inducing probabilities over predicates\. Following the idea of differentiable rewards for LTL in\[[24](https://arxiv.org/html/2608.13625#bib.bib24)\], we define the probability of satisfying a predicate for an observed statessasPr​\(μ\>0\)=h​\(μ​\(s\)\)\\textsc\{Pr\}\(\\mu\>0\)=h\(\\mu\(s\)\)wherehhis a cumulative distribution function \(CDF\) \(e\.g\., the sigmoid for logistic noise\)\. The probability of observing each input letterα∈Σ=2Λ\\alpha\\in\\Sigma=2^\{\\Lambda\}is then calculated as the product ofh⁡\(μ⁡\(s\)\)h\(\\mu\(s\)\)forμ∈α\\mu\\in\\alphaand1−h⁡\(μ⁡\(s\)\)1\-h\(\\mu\(s\)\)forμ∉α\\mu\\not\\in\\alpha, which corresponds to the probability of making a transition withα\\alpha\. We now formally define the STL\-RM:

###### Definition 4

An STL\-RM is a tupleℛφ=\(Q,q0,Δ,R\)\\mathcal\{R\}\_\{\\varphi\}=\(Q,q\_\{0\},\\Delta,R\)constructed for an OCATA𝒜φ=\(L,l0,Σ,K,D,δ,F\)\\mathcal\{A\}\_\{\\varphi\}=\(L,l\_\{0\},\\Sigma,K,D,\\allowbreak\\delta,F\)derived from an STL specificationφ\\varphi;Q=\(\[0,1\]\|L\|×ℝ≥0\)\+Q=\(\[0,1\]^\{\|L\|\}\\times\\mathbb\{R\}\_\{\\geq 0\}\)^\{\+\}is a memory list tracking location probabilities and clock valuations for each OCATA copy;q0q\_\{0\}is the initial memory list;Δ:Q×S×ℝ≥0×ℰ↦Q\\Delta:Q\\times S\\times\\mathbb\{R\}\_\{\\geq 0\}\\times\\mathcal\{E\}\\mapsto Qis the transition function that updates the memory list whereℰ\\mathcal\{E\}is the set ofϵ\\epsilon\-actions corresponding to nondeterministic transitions inδ\\delta; andR:Q↦\[0,1\]R:Q\\mapsto\[0,1\]is a reward function\.

The transition functionΔ\\Deltamodifies a memory listq∈Qq\\in Qas follows\. Let𝐪t=\(vt\(1\),𝐩t\(1\)\)​\(vt\(2\),𝐩t\(2\)\)​…​\(vt\(n\),𝐩t\(n\)\)\\mathbf\{q\}\_\{t\}=\(v\_\{t\}^\{\(1\)\},\\mathbf\{p\}\_\{t\}^\{\(1\)\}\)\(v\_\{t\}^\{\(2\)\},\\mathbf\{p\}\_\{t\}^\{\(2\)\}\)\\dots\(v\_\{t\}^\{\(n\)\},\\mathbf\{p\}\_\{t\}^\{\(n\)\}\)be the current memory list where𝐩t\(i\)=\{pt\(i,l\)\}l∈L\\mathbf\{p\}\_\{t\}^\{\(i\)\}=\\\{p\_\{t\}^\{\(i,l\)\}\\\}\_\{l\\in L\}denotes the probability vector such thatpt\(i,l\)p\_\{t\}^\{\(i,l\)\}is the probability of being in locationll; andvtiv\_\{t\}^\{i\}denotes the clock valuation in theii\-th copy at time steptt\. The RMℛφ\\mathcal\{R\}\_\{\\varphi\}starts with the initial memory list𝐪0=\(v0\(1\),𝐩0\(1\)\)\\mathbf\{q\}\_\{0\}=\(v\_\{0\}^\{\(1\)\},\\mathbf\{p\}\_\{0\}^\{\(1\)\}\)wherev0\(1\)=0v\_\{0\}^\{\(1\)\}=0andp0\(1,l\)p\_\{0\}^\{\(1,l\)\}is11forl=l0l=l\_\{0\}and00for alll≠l0l\\neq l\_\{0\}\. After each observation\(st,τt\)\(s\_\{t\},\\tau\_\{t\}\)from the SMDP along with anϵ\\epsilon\-actionεt\\varepsilon\_\{t\}provided by the RL agent,ℛφ\\mathcal\{R\}\_\{\\varphi\}advances each clock valuationvt\(i\)v\_\{t\}^\{\(i\)\}byτt\\tau\_\{t\}and makes a transition for each automaton state in the memory, i\.e\.,\(l,vt\(i\)\)\(l,v\_\{t\}^\{\(i\)\}\)for everyl∈Ll\\in Lwithpt\(i,l\)\>0p\_\{t\}^\{\(i,l\)\}\>0in each copyi=1,2,…,ni=1,2,\\dots,n, based onsts\_\{t\}andεt\\varepsilon\_\{t\}\.

The transitions are performed by handling probabilistic inputs, nondeterministic and conjunctive branching\. Specifically, for the observationsts\_\{t\}, the transition probabilitiespαstp^\{s\_\{t\}\}\_\{\\alpha\}associated with each inputα\\alphaare first computed as follows

pαst≔\\displaystyle p^\{s\_\{t\}\}\_\{\\alpha\}\\coloneqq∏μ∈αPr⁡\(μ≥0\)​∏μ∉αPr⁡\(μ<0\)\\displaystyle\\prod\_\{\\mu\\in\\alpha\}\\Pr\(\\mu\\geq 0\)\\prod\_\{\\mu\\notin\\alpha\}\\Pr\(\\mu<0\)=\\displaystyle=∏μ∈αh⁡\(μ⁡\(st\)\)​∏μ∉α\(1−h⁡\(μ⁡\(st\)\)\)\.\\displaystyle\\prod\_\{\\mu\\in\\alpha\}h\(\\mu\(s\_\{t\}\)\)\\prod\_\{\\mu\\notin\\alpha\}\\left\(1\-h\(\\mu\(s\_\{t\}\)\)\\right\)\.\(5\)The nondeterminism \(∨\\vee\) is then resolved by choosing the branches corresponding to theϵ\\epsilon\-actionεt\\varepsilon\_\{t\}provided by the RL agent\. Lastly, for the conjunctions \(∧\\wedge\), the probability of a source locationllis divided equally among the destinations\. For example, if there are two conjunctive destinationsl′l^\{\\prime\}andl′′l^\{\\prime\\prime\}without clock resets, the probability that flows fromlltol′l^\{\\prime\}\(or tol′′l^\{\\prime\\prime\}\) ispt\(i,l\)​pαst/2p\_\{t\}^\{\(i,l\)\}p^\{s\_\{t\}\}\_\{\\alpha\}/2\. However, if one of the transitions, sayl′l^\{\\prime\}, resets the clock, then the probabilitypt\(i,l\)​pαst/2p\_\{t\}^\{\(i,l\)\}p^\{s\_\{t\}\}\_\{\\alpha\}/2flows to a new entry added to the memory with a clock valuation of 0\. We note that the sum of all of the probabilities always remains equal to11due to the total transition function with respect to input letter, resolved nondeterminism, and equal probability splitting in conjunctions\. Lastly,R:Q↦\[0,1\]R:Q\\mapsto\[0,1\]is a reward function that maps a memory listqtq\_\{t\}to a rewardrt=r​∑i∑l∈FpFlr\_\{t\}=r\\sum\_\{i\}\\sum\_\{l\\in F\}p^\{l\}\_\{F\}\.

TABLE I:An Execution of STL\-RM for OCATA from Fig\.[1](https://arxiv.org/html/2608.13625#S4.F1)TimettObservation\(st,τt\)\(s\_\{t\},\\tau\_\{t\}\)ℰ\\mathcal\{E\}\-Actionεt\\varepsilon\_\{t\}Memory List\(vt\+1,𝐩t\+1\)\+\(v\_\{t\+1\},\\mathbf\{p\}\_\{t\+1\}\)^\{\+\}Rewardrt\+1r\_\{t\+1\}11\(⟨1\.4⟩,0\.7\)\(\\langle 1\.4\\rangle,0\.7\)111:\(1\.1,⟨0\.0,1\.0,0\.0,0\.0,0\.0⟩\)1\{:\}\\ \(1\.1,\\langle 0\.0,1\.0,0\.0,0\.0,0\.0\\rangle\)0\.10\.122\(⟨3\.1⟩,0\.6\)\(\\langle 3\.1\\rangle,0\.6\)001:\(1\.7,⟨0\.0,0\.8,0\.0,0\.0,0\.0⟩\)1\{:\}\\ \(1\.7,\\langle 0\.0,0\.8,0\.0,0\.0,0\.0\\rangle\)2:\(0\.0,⟨0\.0,0\.0,0\.2,0\.0,0\.0⟩\)2\{:\}\\ \(0\.0,\\langle 0\.0,0\.0,0\.2,0\.0,0\.0\\rangle\)0\.080\.0833\(⟨5\.0⟩,0\.9\)\(\\langle 5\.0\\rangle,0\.9\)001:\(2\.6,⟨0\.0,0\.6,0\.0,0\.0,0\.0⟩\)1\{:\}\\ \(2\.6,\\langle 0\.0,0\.6,0\.0,0\.0,0\.0\\rangle\)2:\(0\.9,⟨0\.0,0\.0,0\.1,0\.1,0\.0⟩\)2\{:\}\\ \(0\.9,\\langle 0\.0,0\.0,0\.1,0\.1,0\.0\\rangle\)3:\(0\.0,⟨0\.0,0\.0,0\.2,0\.0,0\.0⟩\)3\{:\}\\ \(0\.0,\\langle 0\.0,0\.0,0\.2,0\.0,0\.0\\rangle\)0\.070\.0744\(⟨3\.8⟩,0\.3\)\(\\langle 3\.8\\rangle,0\.3\)001:\(2\.9,⟨0\.0,0\.6,0\.0,0\.0,0\.0⟩\)1\{:\}\\ \(2\.9,\\langle 0\.0,0\.6,0\.0,0\.0,0\.0\\rangle\)2:\(1\.2,⟨0\.0,0\.0,0\.0,0\.1,0\.1⟩\)2\{:\}\\ \(1\.2,\\langle 0\.0,0\.0,0\.0,0\.1,0\.1\\rangle\)3:\(0\.3,⟨0\.0,0\.0,0\.0,0\.2,0\.0⟩\)3\{:\}\\ \(0\.3,\\langle 0\.0,0\.0,0\.0,0\.2,0\.0\\rangle\)0\.090\.09

An example execution of the reward machine \(RM\) constructed from the OCATA in Fig\.[1](https://arxiv.org/html/2608.13625#S4.F1)for the STL specification, is shown in Table[I](https://arxiv.org/html/2608.13625#S5.T1)\. We user≔0\.1r\\coloneqq 0\.1as the reward scaling factor,xf≔4x\_\{\\mathit\{f\}\}\\coloneqq 4as the target position, and

h⁡\(z\)≔max⁡\{0,min⁡\{1,0\.5\+z\}\},z≔1−\|x−xf\|,\\displaystyle h\(z\)\\coloneqq\\max\\\{0,\\min\\\{1,0\.5\+z\\\}\\\},\\;\\;z\\coloneqq 1\-\\lvert x\-x\_\{\\mathit\{f\}\}\\rvert,\(6\)as the CDF that determines perturbation probabilities\. This choice yields transition probability0\.50\.5at the boundaries of the target region\[3,5\]\[3,5\]\. The probability varies linearly in the near\-boundary bands\[2\.5,3\.5\]\[2\.5,3\.5\]and\[4\.5,5\.5\]\[4\.5,5\.5\], and saturates to11or00outside these bands\.

Att=1t=1, theϵ\\epsilon\-action commits to satisfying the “globally” component of the formula, moving all probability mass froml0l\_\{0\}tol1l\_\{1\}, regardless of the observation\. Att=2t=2, the observed position isx=3\.1x=3\.1, i\.e\., at distance0\.10\.1from the boundary\. This yields a probability0\.60\.6of remaining inl1l\_\{1\}\. The remaining mass \(0\.40\.4\) flows to the conjunction, corresponding to leaving the region under near\-boundary behavior due to perturbations\. This0\.40\.4splits evenly:0\.20\.2returns tol1l\_\{1\}and0\.20\.2transitions tol2l\_\{2\}in a newly created memory entry in which the clock is reset\. As a result, the first entry has total mass0\.6\+0\.2=0\.80\.6\+0\.2=0\.8inl1l\_\{1\}and the second has mass0\.20\.2inl2l\_\{2\}\.

Att=3t=3, the observation lies exactly on the boundary; thus, the induced transition probabilities are0\.50\.5\. For the first entry,0\.8⋅0\.5=0\.40\.8\\cdot 0\.5=0\.4remains inl1l\_\{1\}, while the other0\.40\.4flows to the conjunction; half of that \(0\.20\.2\) returns tol1l\_\{1\}and the other half \(0\.20\.2\) moves to a newly created third entry with a freshly reset clock\. For the second entry, because the clock valuation0\.90\.9is below the constraint1\.01\.0, no mass transitions to the rejecting sink\. Instead,0\.2⋅0\.5=0\.10\.2\\cdot 0\.5=0\.1remains inl2l\_\{2\}, and the remaining mass transitions to the accepting sinkl4l\_\{4\}according to the boundary\-induced probability0\.50\.5\.

Finally, att=4t=4, the observed position lies well inside the target region; therefore, the transition probabilities saturate to11and00\. In the first entry, this results in0\.60\.6mass remaining inl1l\_\{1\}\. In the second entry,0\.10\.1transitions to the rejecting sinkl4l\_\{4\}since the clock valuation1\.21\.2exceeds the threshold11, even though the observation is within the target region\. In the third entry, all mass \(0\.20\.2\) transitions to the accepting sinkl3l\_\{3\}since the clock valuation0\.30\.3is below11\. Rewards are computed at each step by summing the probabilities in the accepting locationsl1l\_\{1\}andl3l\_\{3\}and multiplying byr≔0\.1r\\coloneqq 0\.1\.

### V\-CProduct Construction for Markovian Rewards

An RM constructed for STL receives an observation from the SMDP, and anϵ\\epsilon\-action from the RL agent, and outputs a memory list and a scalar reward\. The memory list can be used to construct an augmented state, which makes the provided rewards Markovian\. This can be formalized by constructing a product as follows:

###### Definition 5

A product MDP is a tupleℳ×=\(S×,s0×,A×,P×,R×\)\\mathcal\{M\}^\{\\times\}\{=\}\(S^\{\\times\},s\_\{0\}^\{\\times\},\\allowbreak A^\{\\times\},P^\{\\times\},R^\{\\times\}\)composed of an MDPℳ=\(S,s0,A,P\)\\mathcal\{M\}\{=\}\(S,s\_\{0\},\\allowbreak A,P\)and an STL\-RMℛφ=\(Q,q0,Δ,R\)\\mathcal\{R\}\_\{\\varphi\}\{=\}\(Q,q\_\{0\},\\Delta,R\)such thatS×=S×ℝ≥0×QS^\{\\times\}\{=\}S\{\\times\}\\mathbb\{R\}\_\{\\geq 0\}\{\\times\}Qis the set of product states;s0×=⟨s0,0,q0⟩s\_\{0\}^\{\\times\}\{=\}\\langle s\_\{0\},0,q\_\{0\}\\rangleis the initial product state;A×=A×ℰA^\{\\times\}\{=\}A\{\\times\}\\mathcal\{E\}is the set of product actions;P×P^\{\\times\}is the probabilistic product transition function whereP×​\(⟨s′,τ′,q′⟩∣⟨s,τ,q⟩,⟨a,ε⟩\)≔P^\{\\times\}\(\\langle s^\{\\prime\},\\tau^\{\\prime\},q^\{\\prime\}\\rangle\\mid\\langle s,\\tau,q\\rangle,\\langle a,\\varepsilon\\rangle\)\\coloneqq

\{P\(s′,τ′∣s,a\)if​q′=Δ⁡\(q,s,τ,ε\)0otherwise;\\begin\{cases\}P\(s^\{\\prime\},\\tau^\{\\prime\}\\mid s,a\)&\\textnormal\{ if \}q^\{\\prime\}=\\Delta\(q,s,\\tau,\\varepsilon\)\\\\ 0&\\textnormal\{ otherwise \}\\end\{cases\};andR×:S×↦\[0,1\]R^\{\\times\}:S^\{\\times\}\\mapsto\[0,1\]is the product reward function whereR×​\(⟨s,τ,q⟩\)≔R⁡\(q\)R^\{\\times\}\(\\langle s,\\tau,q\\rangle\)\\coloneqq R\(q\)\.

The product MDPs constructed in this way are standard discrete\-time MDPs and can be readily used with off\-the\-shelf RL tools\. The effect of time durations on STL satisfaction is captured by the memory list, which is part of the product state\. The main challenge is the unbounded growth of the memory lists\. We believe this is fundamentally difficult to avoid because the observed durations are real\-valued, which, without additional assumptions, could require arbitrarily many entries in any approach\. Nevertheless, our approach is substantially more efficient than augmenting the state space with the entire sequence of visited states, as is often required for general unbounded formulas in existing works\. In effect, we store only the information needed to determine STL satisfaction from the observations\. The efficiency can be further improved by pruning entries that have fully transitioned into sink locations after accounting for their remaining cumulative future reward\. Another possible improvement is to store intervals rather than single clock valuations in the entries, especially when the sampling rate is high relative to the time intervals in the STL specifications\.

For simplicity, we assume the memory list has a fixed capacity ofNNentries\. Once the list is full, any newly created entry \(and its associated probability mass\) is discarded, which is equivalent to sending that mass to a rejecting sink state\. We now formalize that achieving the maximal expected return of11is only possible under a policy that satisfies the STL specification with probability11\.

###### Proposition 1

Given an SMDPℳ\\mathcal\{M\}and an STL specificationφ\\varphi, suppose there exists a product policyπ×\\pi^\{\\times\}that achieves the maximum expected return11in the product MDPℳ×=ℳ×ℛ×\\mathcal\{M\}^\{\\times\}=\\mathcal\{M\}\\times\\mathcal\{R\}^\{\\times\}, formed fromℳ\\mathcal\{M\}and the STL\-RMℛ×\\mathcal\{R\}^\{\\times\}constructed fromφ\\varphi\. Then, the induced policyπ\\piinℳ\\mathcal\{M\}satisfiesφ\\varphiwith probability11; i\.e\.,

𝔼σ×∼ℳπ××​\[G×​\(σ×\)\]=1⟹Prσ∼ℳπ​\(σ⊧φ\)=1,\\displaystyle\\mathbb\{E\}\_\{\\sigma^\{\\times\}\\sim\\mathcal\{M\}^\{\\times\}\_\{\\pi^\{\\times\}\}\}\\\!\\bigl\[G^\{\\times\}\(\\sigma^\{\\times\}\)\\bigr\]=1\\;\\Longrightarrow\\;\\textnormal\{Pr\}\_\{\\sigma\\sim\\mathcal\{M\}\_\{\\pi\}\}\(\\sigma\\models\\varphi\)=1,\(7\)whereσ×≔⟨s0,τ0,q0⟩​⟨s1,τ1,q1⟩​…\\sigma^\{\\times\}\\coloneqq\\langle s\_\{0\},\\tau\_\{0\},q\_\{0\}\\rangle\\langle s\_\{1\},\\tau\_\{1\},q\_\{1\}\\rangle\\dotsdenotes a product path sampled from the product Markov chainℳπ××\\mathcal\{M\}^\{\\times\}\_\{\\pi^\{\\times\}\}underπ×\\pi^\{\\times\}, andG×​\(σ×\)G^\{\\times\}\(\\sigma^\{\\times\}\)is its associated return\. Likewise,σ≔\(s0,τ0\)​\(s1,τ1\)​…\\sigma\\coloneqq\(s\_\{0\},\\tau\_\{0\}\)\(s\_\{1\},\\tau\_\{1\}\)\\dotsdenotes the timed path sampled fromℳπ\\mathcal\{M\}\_\{\\pi\}underπ\\pi\.

This follows from the one\-to\-one correspondence between product paths and timed paths due to the fact that the sequenceq0,q1,…q\_\{0\},q\_\{1\},\\dotsof additional memory\-list components along a product path can be uniquely determined by the update functionΔ\\Delta\. Now, the return of a product pathσ×\\sigma^\{\\times\}is11iff a full reward ofrris obtained at each time step \(with discount factorγ=1−r\\gamma=1\-r\)\. We note that, under the bounded\-memory assumption, newly created entries and their associated probabilities are discarded when the list is full, resulting in to permanent reward loss\. Therefore, a return of11requires that no entries are ever discarded and that, at each time step, the total probability mass11is distributed exclusively among accepting locations of the entries in the memory list\. This immediately implies that each successor of any conjunctive branching resides in an accepting location, thereby ensuring the Büchi condition in each computational thread and implying that the corresponding timed pathσ\\sigmasatisfies the STL formulaφ\\varphi\.

Fig\. 2:Learning curves of our approach and baselines across all environments\. Each method is evaluated every 5K environment steps over 100 episodes using the robustness score and satisfaction rate\. Curves and shaded regions show the mean and half the standard deviation, respectively, over five seeds\. For visualization, curves are smoothed with a max filter followed by a moving\-average filter with window size 5\.

## VIExperiments

In this section, we evaluate STL\-RM across a diverse set of control environments and compare it against standard history\-based RL baselines\. We first introduce the STL specifications considered throughout the experiments\. We then describe the evaluation environments, baselines, and implementation details, and finally present and discuss the experimental results\. Our code is available at[https://github\.com/alperkamil/stlrm](https://github.com/alperkamil/stlrm)\.

### VI\-ASTL Tasks

We consider STL specifications that combine representative temporal requirements\. Specifically, we define

φsequencing\\displaystyle\\varphi\_\{\\text\{sequencing\}\}≔F⁡\(a1∧F​a2\),\\displaystyle\\coloneqq F\(a\_\{1\}\\wedge Fa\_\{2\}\),\(8\)φstability\\displaystyle\\varphi\_\{\\text\{stability\}\}≔G⁡\(\(a1∨a2\)⟹F\[0,T\]​\(b1∧b2\)\),\\displaystyle\\coloneqq G\\left\(\(a\_\{1\}\\vee a\_\{2\}\)\\implies F\_\{\[0,T\]\}\(b\_\{1\}\\wedge b\_\{2\}\)\\right\),\(9\)φsafety\\displaystyle\\varphi\_\{\\text\{safety\}\}≔G​¬\(c1∨c2\),\\displaystyle\\coloneqq G\\neg\(c\_\{1\}\\vee c\_\{2\}\),\(10\)φpartial\\displaystyle\\varphi\_\{\\text\{partial\}\}≔φsequencing∧φsafety,\\displaystyle\\coloneqq\\varphi\_\{\\text\{sequencing\}\}\\wedge\\varphi\_\{\\text\{safety\}\},\(11\)φfull\\displaystyle\\varphi\_\{\\text\{full\}\}≔φsequencing∧φstability∧φsafety\.\\displaystyle\\coloneqq\\varphi\_\{\\text\{sequencing\}\}\\wedge\\varphi\_\{\\text\{stability\}\}\\wedge\\varphi\_\{\\text\{safety\}\}\.\(12\)
The three subformulas encode the following temporal behaviors:

- •Sequencing:φsequencing\\varphi\_\{\\text\{sequencing\}\}requires the agent to first visit the target region represented bya1a\_\{1\}and subsequently visit the target region represented bya2a\_\{2\}\.
- •Stability:φstability\\varphi\_\{\\text\{stability\}\}requires the agent to return to a designated central region, represented byb1∧b2b\_\{1\}\\wedge b\_\{2\}, withinTTtime steps after visiting either target regiona1a\_\{1\}ora2a\_\{2\}\.
- •Safety:φsafety\\varphi\_\{\\text\{safety\}\}requires the agent to avoid the unsafe regions represented byc1c\_\{1\}andc2c\_\{2\}at all times\.

Across all environments, the predicates are defined over a one\-dimensional signalxxextracted from the environment state\. The sequencing requirement asks the agent to first reach the positive target region\(3,∞\)\(3,\\infty\)and subsequently reach the negative target region\(−∞,−3\)\(\-\\infty,\-3\)\. After visiting either target region, the stability requirement requires the agent to return to the central region\(−2,2\)\(\-2,2\)withinT=30T=30time steps\. In addition, the safety requirement constrains the agent to remain within the safe interval\(−6,6\)\(\-6,6\)throughout the episode, thereby avoiding the unsafe regions\(6,∞\)\(6,\\infty\)and\(−∞,−6\)\(\-\\infty,\-6\)\.

The corresponding predicate functions are

μa1​\(s\)\\displaystyle\\mu\_\{a\_\{1\}\}\(s\)≔x−3,\\displaystyle\\coloneqq x\-3,μa2​\(s\)\\displaystyle\\mu\_\{a\_\{2\}\}\(s\)≔−\(x\+3\),\\displaystyle\\coloneqq\-\(x\+3\),\(13\)μb1​\(s\)\\displaystyle\\mu\_\{b\_\{1\}\}\(s\)≔x−2,\\displaystyle\\coloneqq x\-2,μb2​\(s\)\\displaystyle\\mu\_\{b\_\{2\}\}\(s\)≔−\(x\+2\),\\displaystyle\\coloneqq\-\(x\+2\),\(14\)μc1​\(s\)\\displaystyle\\mu\_\{c\_\{1\}\}\(s\)≔x−6,\\displaystyle\\coloneqq x\-6,μc2​\(s\)\\displaystyle\\mu\_\{c\_\{2\}\}\(s\)≔−\(x\+6\),\\displaystyle\\coloneqq\-\(x\+6\),\(15\)where each predicate is satisfied whenever its corresponding predicate function is nonnegative\.

We evaluate two variants of the STL task,φpartial\\varphi\_\{\\text\{partial\}\}andφfull\\varphi\_\{\\text\{full\}\}, which differ in the temporal information required for successful control\. The partial specification,φpartial\\varphi\_\{\\text\{partial\}\}, requires ordered visitation of the target regions while enforcing safety\. Since it contains only unbounded temporal operators, it abstracts away the precise timing of events and primarily requires the agent to retain their logical progression\. Consequently, the task can be represented by a small automaton consisting of, for example, an initial mode, a mode indicating thata1a\_\{1\}has been reached, a mode indicating that the sequence has been completed by subsequently reachinga2a\_\{2\}, and a rejecting mode entered upon reaching either unsafe regionc1c\_\{1\}orc2c\_\{2\}, thereby encoding progress through the specification\. The functionality of these modes may potentially be captured from a relatively short history of past observations\.

In contrast, the full specification,φfull\\varphi\_\{\\text\{full\}\}, additionally incorporates the bounded\-time stability requirement\. Whenever eithera1a\_\{1\}ora2a\_\{2\}is visited, the agent must not only remember that the event occurred but also retain its temporal context to ensure that the designated central region is reached withinTTtime steps\. Satisfying the full specification therefore requires memory that captures both the logical progression of events and their timing\. This explicit real\-time constraint is substantially more difficult to directly infer from a history of observations, motivating the structured memory mechanism provided by our STL\-RM approach\.

### VI\-BEnvironments

We evaluate STL\-RM on five benchmark control environments from Gymnasium\[[77](https://arxiv.org/html/2608.13625#bib.bib77)\]\. These environments span a broad range of control settings, from low\-dimensional discrete control to high\-dimensional continuous robotic manipulation:

- •CartPole:A classical control task with a discrete action space\. We use the horizontal position of the cart as the signal for evaluating the STL specification\.
- •Reacher:A continuous\-control robotic arm environment\. We use the horizontal position of the arm’s fingertip as the STL signal\.
- •Pusher:A higher\-dimensional continuous\-control manipulation task in which a robotic arm interacts with an object\. We use the horizontal position of the arm’s fingertip as the STL signal\.
- •Fetch:A continuous\-control robotic manipulation environment\. As in Reacher and Pusher, we use the horizontal position of the robot’s end effector as the STL signal\.
- •Adroit:A high\-dimensional dexterous manipulation environment\. We use the horizontal position of the robotic hand as the STL signal\.

All environments have continuous observation spaces, whereas their action spaces are continuous except for CartPole, which has a discrete action space\. Since the raw position ranges differ across environments, we normalize the selected signal so that its initial mean is zero and apply an environment\-specific scaling factor\. This transformation places the relevant signal values within a reachable range while allowing the same STL specification to be applied consistently across all environments\.

Each episode has a maximum horizon of500500time steps\. To ensure that learning is driven exclusively by the STL objective rather than by environment\-specific objectives, we remove the native reward functions of the environments\. We also disable their default early\-termination conditions, except for termination resulting from safety violations\.

### VI\-CBaselines and Implementation

We compare STL\-RM against two standard approaches for incorporating temporal information into RL:*observation stacking*and*recurrent policies*\. These baselines provide the policy with access to historical information without explicitly constructing a symbolic representation of the temporal specification\.

- •STL\-RM\(Ours\): We implement STL\-RM in Python\. For the specification defined above, we construct standard Büchi automata forφsequencing\\varphi\_\{\\text\{sequencing\}\}andφsafety\\varphi\_\{\\text\{safety\}\}\. The bounded\-time stability specificationφstability\\varphi\_\{\\text\{stability\}\}is represented using an OCATA together with the memory mechanism introduced in our method\. The memory\-list capacity is set toN=50N=50\. For transitions leading to accepting and rejecting states \(i\.e\., non\-accepting sink states\), we use the clipped functionshaccept​\(z\)=max⁡\{0,min⁡\{1,z\}\}h\_\{\\text\{accept\}\}\(z\)=\\max\\\{0,\\min\\\{1,z\\\}\\\}andhreject​\(z\)=max⁡\{0,min⁡\{1,1\+z\}\}h\_\{\\text\{reject\}\}\(z\)=\\max\\\{0,\\min\\\{1,1\+z\\\}\\\}, respectively, wherezzdenotes the distance between the transition boundary and the current signal value\. For simplicity, we set the discount factors to the PPO default values,γ=γ′=0\.99\\gamma=\\gamma^\{\\prime\}=0\.99\.
- •STL\-RM \(Discrete\)\(Ours\): This ablation is obtained by discretizing the transitions in STL\-RM\. Specifically, the CDF is replaced by the indicator functionh⁡\(z\)=𝟙z≥0h\(z\)=\\mathbbm\{1\}\_\{z\\geq 0\}, which evaluates to11whenz≥0z\\geq 0and to00otherwise\. This variant allows us to isolate the effect of the continuous robustness\-aware transition construction used in STL\-RM\.
- •Stacking: This baseline explicitly represents temporal history by concatenating a fixed number of previously observed signal values with the current environment observation\. We consider stack sizes of55,5050, and500500, corresponding to short, intermediate, and full\-episode histories, respectively\. These configurations allow us to examine how the amount of explicitly available history of observations affects the performance of a feedforward policy\.
- •Recurrent: This baseline uses a long short\-term memory \(LSTM\) network\[[78](https://arxiv.org/html/2608.13625#bib.bib78)\]to encode observation history\. Unlike observation stacking, which explicitly retains a fixed history window, the LSTM learns a latent representation of temporally relevant information\. We use a single LSTM layer with256256hidden units\.

To the best of our knowledge, existing RL methods for STL do not directly support the class of general formulas with arbitrarily nested temporal operators considered\. We therefore use these two history\-based approaches as generic baselines that work for entire STL for comparison\. We evaluate whether the explicit STL\-based memory and reward\-machine structure ofSTL\-RMprovide an advantage over learned representations of observation history via robustness scores\.

All methods use Proximal Policy Optimization \(PPO\)\[[79](https://arxiv.org/html/2608.13625#bib.bib79)\], implemented with Stable\-Baselines3\[[80](https://arxiv.org/html/2608.13625#bib.bib80)\], as the underlying RL algorithm\. The actor and critic networks consist of two fully connected hidden layers with256256units per layer\. The recurrent baseline additionally includes the256256\-unit LSTM layer described above\. All remaining PPO hyperparameters are set to their Stable\-Baselines3 default values\.

For bothStackingandRecurrent, we use dense\-time online STL robustness computed with RTAMT\[[81](https://arxiv.org/html/2608.13625#bib.bib81)\]as the reward signal at each training step\. This provides the baselines with a dense STL\-based learning signal while leaving the policy responsible for representing the temporal history required to satisfy the specification\.

During evaluation, we use the same metrics for all methods, includingSTL\-RM\. Specifically, we report the final average STL robustness score over 100 evaluation trajectories, together with the corresponding STL satisfaction rate, enabling a direct comparison of the methods based on their ability to satisfy the complete temporal specification\. For the STL specifications considered in our experiments, the maximum achievable robustness score is1\.51\.5, whereas the minimum is unbounded below\. To prevent large negative values from disproportionately affecting the reported averages, we clip negative robustness scores to zero\.

### VI\-DResults

Fig\.[2](https://arxiv.org/html/2608.13625#S5.F2)presents the learning curves, obtained over 400 K steps \(K=1,000\), of all methods across the five environments\. For the partial specificationφpartial\\varphi\_\{\\text\{partial\}\}, bothSTL\-RMandSTL\-RM \(Discrete\)rapidly converge to policies with a satisfaction rate of11\. The two variants of our approach outperform the baselines in terms of satisfaction rate across all environments exceptFetch, where the baselines achieve competitive performance\. Moreover,STL\-RMgenerally achieves higher robustness scores, indicating that its robustness\-aware transition construction encourages policies that satisfy the specification with larger margins\.

The baselines exhibit a substantial performance degradation when moving from the partial specificationφpartial\\varphi\_\{\\text\{partial\}\}to the full specificationφfull\\varphi\_\{\\text\{full\}\}\. This result highlights the difficulty of learning bounded\-time requirements from observation history using STL robustness alone as the reward signal\. In contrast,STL\-RMandSTL\-RM \(Discrete\)converge to optimal or near\-optimal policies in terms of satisfaction rate, whileSTL\-RMachieves higher robustness scores than the baselines\. The performance of both STL\-RM variants improves inFetchunder the full specification, suggesting that the additional stability requirement can provide a useful learning signal in this environment\.

The difference in satisfaction rate betweenSTL\-RMandSTL\-RM \(Discrete\)is generally small across environments\. However,STL\-RMtypically achieves higher robustness scores\. This observation suggests that although discretized automaton transitions may be sufficient to learn satisfying policies, incorporating continuous robustness information into the reward\-machine transitions through probabilistic transitions encourages trajectories that satisfy the specification more robustly\.

## VIIConclusion

This paper advances RL from general STL specifications by addressing the central challenge posed by their history\-dependent satisfaction semantics\. By compiling event\-based STL formulas into OCATAs and subsequently into STL\-RMs, our framework provides a compact memory representation and Markovian reward structure compatible with standard RL algorithms\. In doing so, STL\-RM avoids the computational burden of explicitly augmenting the state with observation histories while retaining the expressive power of STL beyond the restricted fragments considered in prior work\. We further incorporate robustness to observation perturbations into the reward construction and establish that policies maximizing the cumulative reward satisfy the specification almost surely\. Our empirical results demonstrate that STL\-RM achieves higher satisfaction rates and robustness scores than history\-based baselines trained directly with STL robustness rewards, indicating that automata\-based reward design provides a promising direction for model\-free control synthesis from expressive STL specifications\.

A fundamental limitation of the proposed approach is its finite memory capacity\. Although the STL\-RM memory is substantially more compact than explicitly storing past observations, the memory list may require a new entry for each temporally constrained condition that must be tracked\. Consequently, the memory capacity can become a bottleneck for specifications that generate many simultaneous temporal obligations\. An important direction for future work is therefore to develop more compact memory representations, for example by integrating interval\-based representations that aggregate multiple related memory entries rather than storing them individually\.

Another advantage of STL\-RM is that its reward\-machine formulation makes a broad range of existing reward\-machine extensions readily applicable\. For example, the framework could be extended with counterfactual reasoning techniques\[[76](https://arxiv.org/html/2608.13625#bib.bib76)\], as well as generalized to settings involving lexicographic objectives\[[82](https://arxiv.org/html/2608.13625#bib.bib82)\]and stochastic games\[[83](https://arxiv.org/html/2608.13625#bib.bib83),[84](https://arxiv.org/html/2608.13625#bib.bib84),[71](https://arxiv.org/html/2608.13625#bib.bib71)\]\. These directions provide opportunities to improve learning efficiency and extend STL\-based policy synthesis to richer multi\-objective and multi\-agent control environments\.

## References

## References

- \[1\]O\. Maler and D\. Nickovic, “Monitoring temporal properties of continuous signals,” in*International symposium on formal techniques in real\-time and fault\-tolerant systems*\. Springer, 2004, pp\. 152–166\.
- \[2\]A\. Donzé and O\. Maler, “Robust satisfaction of temporal logic over real\-valued signals,” in*International conference on formal modeling and analysis of timed systems*\. Springer, 2010, pp\. 92–106\.
- \[3\]D\. Gundana and H\. Kress\-Gazit, “Event\-based signal temporal logic synthesis for single and multi\-robot tasks,”*IEEE Robotics and Automation Letters*, vol\. 6, no\. 2, pp\. 3687–3694, 2021\.
- \[4\]F\. Pigozzi, E\. Medvet, and L\. Nenzi, “Mining road traffic rules with signal temporal logic and grammar\-based genetic programming,”*Applied Sciences*, vol\. 11, no\. 22, p\. 10573, 2021\.
- \[5\]A\. Mambakam, J\. I\. Requeno Jarabo, A\. Bakhirkin, N\. Basset, and T\. Dang, “Mining of extended signal temporal logic specifications with paretolib 2\.0,”*Formal Methods in System Design*, vol\. 62, no\. 1, pp\. 260–284, 2024\.
- \[6\]A\. Donzé, T\. Ferrere, and O\. Maler, “Efficient robust monitoring for stl,” in*International conference on computer aided verification*\. Springer, 2013, pp\. 264–279\.
- \[7\]J\. V\. Deshmukh, A\. Donzé, S\. Ghosh, X\. Jin, G\. Juniwal, and S\. A\. Seshia, “Robust online monitoring of signal temporal logic,”*Formal Methods in System Design*, vol\. 51, no\. 1, pp\. 5–30, 2017\.
- \[8\]N\. Mehdipour, C\.\-I\. Vasile, and C\. Belta, “Generalized mean robustness for signal temporal logic,”*IEEE Transactions on Automatic Control*, vol\. 70, no\. 3, pp\. 1949–1956, 2024\.
- \[9\]A\. Rodionova, L\. Lindemann, M\. Morari, and G\. Pappas, “Temporal robustness of temporal logic specifications: Analysis and control design,”*ACM Transactions on Embedded Computing Systems*, vol\. 22, no\. 1, pp\. 1–44, 2022\.
- \[10\]S\. A\. Seshia, “Combining induction, deduction, and structure for verification and synthesis,”*Proceedings of the IEEE*, vol\. 103, no\. 11, pp\. 2036–2051, 2015\.
- \[11\]V\. Raman, M\. Maasoumy, and A\. Donzé, “Model predictive control from signal temporal logic specifications: A case study,” in*Proceedings of the 4th ACM SIGBED international workshop on design, modeling, and evaluation of cyber\-physical systems*, 2014, pp\. 52–55\.
- \[12\]V\. Raman, A\. Donzé, D\. Sadigh, R\. M\. Murray, and S\. A\. Seshia, “Reactive synthesis from signal temporal logic specifications,” in*Proceedings of the 18th international conference on hybrid systems: Computation and control*, 2015, pp\. 239–248\.
- \[13\]L\. Lindemann, G\. J\. Pappas, and D\. V\. Dimarogonas, “Reactive and risk\-aware control for signal temporal logic,”*IEEE Transactions on Automatic Control*, vol\. 67, no\. 10, pp\. 5262–5277, 2021\.
- \[14\]M\. Charitidou and D\. V\. Dimarogonas, “Receding horizon control with online barrier function design under signal temporal logic specifications,”*IEEE Transactions on Automatic Control*, vol\. 68, no\. 6, pp\. 3545–3556, 2022\.
- \[15\]Y\. Yao, J\. Sun, and Y\. Zhang, “Multitask synthesis of hybrid systems via temporal logic,”*IEEE Transactions on Automatic Control*, vol\. 68, no\. 11, pp\. 6883–6890, 2023\.
- \[16\]D\. Aksaray, A\. Jones, Z\. Kong, M\. Schwager, and C\. Belta, “Q\-learning for robust satisfaction of signal temporal logic specifications,” in*2016 IEEE 55th Conference on Decision and Control \(CDC\)*\. IEEE, 2016, pp\. 6565–6570\.
- \[17\]D\. Muniraj, K\. G\. Vamvoudakis, and M\. Farhood, “Enforcing signal temporal logic specifications in multi\-agent adversarial environments: A deep q\-learning approach,” in*2018 IEEE Conference on Decision and Control \(CDC\)*\. IEEE, 2018, pp\. 4141–4146\.
- \[18\]H\. Venkataraman, D\. Aksaray, and P\. Seiler, “Tractable reinforcement learning of signal temporal logic objectives,” in*Learning for dynamics and control*\. PMLR, 2020, pp\. 308–317\.
- \[19\]K\. C\. Kalagarla, R\. Jain, and P\. Nuzzo, “Model\-free reinforcement learning for optimal control of markov decision processes under signal temporal logic specifications,” in*2021 60th IEEE Conference on Decision and Control \(CDC\)*\. IEEE, 2021, pp\. 2252–2257\.
- \[20\]S\. Wang, X\. Yin, S\. Li, and X\. Yin, “Tractable reinforcement learning for signal temporal logic tasks with counterfactual experience replay,”*IEEE Control Systems Letters*, vol\. 8, pp\. 616–621, 2024\.
- \[21\]P\. Varnai and D\. V\. Dimarogonas, “Prescribed performance control guided policy improvement for satisfying signal temporal logic tasks,” in*2019 American Control Conference \(ACC\)*\. IEEE, 2019, pp\. 286–291\.
- \[22\]W\. Liu, W\. Xiao, and C\. Belta, “Learning robust and correct controllers from signal temporal logic specifications using barriernet,” in*2023 62nd IEEE Conference on Decision and Control \(CDC\)*\. IEEE, 2023, pp\. 7049–7054\.
- \[23\]T\. Brihaye, G\. Geeraerts, H\.\-M\. Ho, and B\. Monmege, “Mightyl: A compositional translation from mitl to timed automata,” in*International Conference on Computer Aided Verification*\. Springer, 2017, pp\. 421–440\.
- \[24\]A\. K\. Bozkurt, C\. Belta, and M\. Lin, “Accelerated learning with linear temporal logic using differentiable simulation,” in*The Fourteenth International Conference on Learning Representations*, 2026\. \[Online\]\. Available:[https://openreview\.net/forum?id=zbdhhlIy8o](https://openreview.net/forum?id=zbdhhlIy8o)
- \[25\]X\. Yin, B\. Gao, and X\. Yu, “Formal synthesis of controllers for safety\-critical autonomous systems: Developments and challenges,”*Annual Reviews in Control*, vol\. 57, p\. 100940, 2024\.
- \[26\]Z\. Liu, J\. Dai, B\. Wu, and H\. Lin, “Communication\-aware motion planning for multi\-agent systems from signal temporal logic specifications,” in*2017 American Control Conference \(ACC\)*\. IEEE, 2017, pp\. 2516–2521\.
- \[27\]H\. Kress\-Gazit, M\. Lahijanian, and V\. Raman, “Synthesis for robots: Guarantees and feedback for robot behavior,”*Annual Review of Control, Robotics, and Autonomous Systems*, vol\. 1, no\. 1, pp\. 211–236, 2018\.
- \[28\]C\. Belta and S\. Sadraddini, “Formal methods for control synthesis: An optimization perspective,”*Annual Review of Control, Robotics, and Autonomous Systems*, vol\. 2, no\. 1, pp\. 115–140, 2019\.
- \[29\]V\. Kurtz and H\. Lin, “Mixed\-integer programming for signal temporal logic with fewer binary variables,”*IEEE Control Systems Letters*, vol\. 6, pp\. 2635–2640, 2022\.
- \[30\]X\. Yu, Y\. Zhao, X\. Yin, and L\. Lindemann, “Signal temporal logic control synthesis among uncontrollable dynamic agents with conformal prediction,”*Automatica*, vol\. 183, p\. 112616, 2026\.
- \[31\]J\. Zhang, P\. Lu, and G\. Chen, “Decomposition\-based mpc for uncertain systems with nested signal temporal logic specifications,”*IEEE Control Systems Letters*, 2025\.
- \[32\]D\. Sadigh and A\. Kapoor, “Safe control under uncertainty with probabilistic signal temporal logic,” in*Proceedings of Robotics: Science and Systems XII*, 2016\.
- \[33\]S\. Jha, V\. Raman, D\. Sadigh, and S\. A\. Seshia, “Safe autonomy under perception uncertainty using chance\-constrained temporal logic,”*Journal of Automated Reasoning*, vol\. 60, no\. 1, pp\. 43–62, 2018\.
- \[34\]S\. S\. Farahani, R\. Majumdar, V\. S\. Prabhu, and S\. Soudjani, “Shrinking horizon model predictive control with signal temporal logic constraints under stochastic disturbances,”*IEEE Transactions on Automatic Control*, vol\. 64, no\. 8, pp\. 3324–3331, 2018\.
- \[35\]H\. Chen, S\. A\. Smolka, N\. Paoletti, and S\. Lin, “An stl\-based approach to resilient control for cyber\-physical systems,” in*Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control*, 2023, pp\. 1–12\.
- \[36\]Y\. Yao, J\. Sun, and Y\. Zhang, “Model predictive control of stochastic hybrid systems with signal temporal logic constraints,”*Automatica*, vol\. 173, p\. 112038, 2025\.
- \[37\]R\. Ilyes, L\. Brudermüller, N\. Hawes, and B\. Lacerda, “Receding horizon control for signal temporal logic using robustness\-conserving partial formula evaluation,”*IEEE Robotics and Automation Letters*, 2025\.
- \[38\]L\. Lindemann and D\. V\. Dimarogonas, “Control barrier functions for signal temporal logic tasks,”*IEEE control systems letters*, vol\. 3, no\. 1, pp\. 96–101, 2018\.
- \[39\]G\. Yang, C\. Belta, and R\. Tron, “Continuous\-time signal temporal logic planning with control barrier functions,” in*2020 American Control Conference \(ACC\)*\. IEEE, 2020, pp\. 4612–4618\.
- \[40\]P\. Yu, X\. Tan, and D\. V\. Dimarogonas, “Continuous\-time control synthesis under nested signal temporal logic specifications,”*IEEE Transactions on Robotics*, vol\. 40, pp\. 2272–2286, 2024\.
- \[41\]Y\. V\. Pant, H\. Abbas, and R\. Mangharam, “Smooth operator: Control using the smooth robustness of temporal logic,” in*2017 IEEE Conference on Control Technology and Applications \(CCTA\)*\. IEEE, 2017, pp\. 1235–1240\.
- \[42\]L\. Lindemann and D\. V\. Dimarogonas, “Robust control for signal temporal logic specifications using discrete average space robustness,”*Automatica*, vol\. 101, pp\. 377–387, 2019\.
- \[43\]I\. Haghighi, N\. Mehdipour, E\. Bartocci, and C\. Belta, “Control from signal temporal logic specifications with smooth cumulative quantitative semantics,” in*2019 IEEE 58th Conference on Decision and Control \(CDC\)*\. IEEE, 2019, pp\. 4361–4366\.
- \[44\]N\. Mehdipour, C\.\-I\. Vasile, and C\. Belta, “Arithmetic\-geometric mean robustness for control from signal temporal logic specifications,” in*2019 American Control Conference \(ACC\)*\. IEEE, 2019, pp\. 1690–1695\.
- \[45\]Y\. Gilpin, V\. Kurtz, and H\. Lin, “A smooth robustness measure of signal temporal logic for symbolic control,”*IEEE Control Systems Letters*, vol\. 5, no\. 1, pp\. 241–246, 2020\.
- \[46\]Y\. Takayama, K\. Hashimoto, and T\. Ohtsuka, “Stlccp: Efficient convex optimization\-based framework for signal temporal logic specifications,”*IEEE Transactions on Automatic Control*, 2025\.
- \[47\]K\. Leung, N\. Aréchiga, and M\. Pavone, “Backpropagation through signal temporal logic specifications: Infusing logical structure into gradient\-based methods,”*The International Journal of Robotics Research*, vol\. 42, no\. 6, pp\. 356–370, 2023\.
- \[48\]Y\. Meng and C\. Fan, “Signal temporal logic neural predictive control,”*IEEE Robotics and Automation Letters*, vol\. 8, no\. 11, pp\. 7719–7726, 2023\.
- \[49\]E\. E\. Vlahakis, L\. Lindemann, P\. Sopasakis, and D\. V\. Dimarogonas, “Probabilistic tube\-based control synthesis of stochastic multi\-agent systems under signal temporal logic,” in*2024 IEEE 63rd Conference on Decision and Control \(CDC\)*\. IEEE, 2024, pp\. 1586–1592\.
- \[50\]R\. Das, S\. Choudhury, and P\. Jagtap, “Approximation\-free control for signal temporal logic specifications using spatiotemporal tubes,”*IEEE Control Systems Letters*, 2025\.
- \[51\]L\. Lindemann, C\. K\. Verginis, and D\. V\. Dimarogonas, “Prescribed performance control for signal temporal logic specifications,” in*2017 IEEE 56th Annual Conference on Decision and Control \(CDC\)*\. IEEE, 2017, pp\. 2997–3002\.
- \[52\]F\. Chen, M\. Sewlia, and D\. V\. Dimarogonas, “Cooperative control of heterogeneous multi\-agent systems under spatiotemporal constraints,”*Annual Reviews in Control*, vol\. 57, p\. 100946, 2024\.
- \[53\]S\. Liu, A\. Saoud, and D\. V\. Dimarogonas, “Controller synthesis of collaborative signal temporal logic tasks for multi\-agent systems via assume\-guarantee contracts,”*IEEE Transactions on Automatic Control*, 2025\.
- \[54\]X\. Yu, C\. Wang, D\. Yuan, S\. Li, and X\. Yin, “Model predictive control for signal temporal logic specifications with time interval decomposition,” in*2023 62nd IEEE Conference on Decision and Control \(CDC\)*\. IEEE, 2023, pp\. 7849–7855\.
- \[55\]T\. Yang, Y\. Zou, S\. Li, X\. Yin, and T\. Jia, “Signal temporal logic synthesis under model predictive control: A low complexity approach,”*Control Engineering Practice*, vol\. 143, p\. 105782, 2024\.
- \[56\]E\. Lai, R\. Bonalli, A\. Girard, and F\. Jean, “Continuous\-time nonlinear optimal control problem under signal temporal logic constraints,” in*2025 IEEE 64th Conference on Decision and Control \(CDC\)*\. IEEE, 2025, pp\. 1887–1892\.
- \[57\]B\. Recht, “A tour of reinforcement learning: The view from continuous control,”*Annual Review of Control, Robotics, and Autonomous Systems*, vol\. 2, no\. 1, pp\. 253–279, 2019\.
- \[58\]A\. Balakrishnan and J\. V\. Deshmukh, “Structured reward shaping using signal temporal logic specifications,” in*2019 IEEE/RSJ International Conference on Intelligent Robots and Systems \(IROS\)*\. IEEE, 2019, pp\. 3481–3486\.
- \[59\]P\. Varnai and D\. V\. Dimarogonas, “On robustness metrics for learning stl tasks,” in*2020 American Control Conference \(ACC\)*\. IEEE, 2020, pp\. 5394–5399\.
- \[60\]N\. Hamilton, P\. K\. Robinette, and T\. T\. Johnson, “Training agents to satisfy timed and untimed signal temporal logic specifications with reinforcement learning,” in*International Conference on Software Engineering and Formal Methods*\. Springer, 2022, pp\. 190–206\.
- \[61\]J\. Ikemoto and T\. Ushio, “Deep reinforcement learning under signal temporal logic constraints using lagrangian relaxation,”*IEEE Access*, vol\. 10, pp\. 114 814–114 828, 2022\.
- \[62\]S\. Wang, S\. Li, L\. Yin, and X\. Yin, “Synthesis of temporally\-robust policies for signal temporal logic tasks using reinforcement learning,” in*2024 IEEE International Conference on Robotics and Automation \(ICRA\)*\. IEEE, 2024, pp\. 10 503–10 509\.
- \[63\]D\. Tian, H\. Fang, Q\. Yang, Z\. Guo, J\. Cui, W\. Liang, and Y\. Wu, “Two\-phase motion planning under signal temporal logic specifications in partially unknown environments,”*IEEE Transactions on Industrial Electronics*, vol\. 70, no\. 7, pp\. 7113–7121, 2022\.
- \[64\]N\. Saxena, S\. Gorantla, and P\. Jagtap, “Funnel\-based reward shaping for signal temporal logic tasks in reinforcement learning,”*IEEE Robotics and Automation Letters*, vol\. 9, no\. 2, pp\. 1373–1379, 2023\.
- \[65\]E\. M\. Hahn, M\. Perez, S\. Schewe, F\. Somenzi, A\. Trivedi, and D\. Wojtczak, “Omega\-regular objectives in model\-free reinforcement learning,” in*International conference on tools and algorithms for the construction and analysis of systems*\. Springer, 2019, pp\. 395–412\.
- \[66\]M\. Hasanbeig, Y\. Kantaros, A\. Abate, D\. Kroening, G\. J\. Pappas, and I\. Lee, “Reinforcement learning for temporal logic control synthesis with probabilistic satisfaction guarantees,” in*2019 IEEE 58th conference on decision and control \(CDC\)*\. IEEE, 2019, pp\. 5338–5343\.
- \[67\]A\. K\. Bozkurt, Y\. Wang, M\. M\. Zavlanos, and M\. Pajic, “Control synthesis from linear temporal logic specifications using model\-free reinforcement learning,” in*2020 IEEE International Conference on Robotics and Automation \(ICRA\)*\. IEEE, 2020, pp\. 10 349–10 355\.
- \[68\]M\. Cai, H\. Peng, Z\. Li, and Z\. Kan, “Learning\-based probabilistic ltl motion planning with environment and motion uncertainties,”*IEEE Transactions on Automatic Control*, vol\. 66, no\. 5, pp\. 2386–2392, 2020\.
- \[69\]M\. Wen and U\. Topcu, “Probably approximately correct learning in adversarial environments with temporal logic specifications,”*IEEE Transactions on Automatic Control*, vol\. 67, no\. 10, pp\. 5055–5070, 2021\.
- \[70\]R\. Oura, T\. Ushio, and A\. Sakakibara, “Bounded synthesis and reinforcement learning of supervisors for stochastic discrete event systems with ltl specifications,”*IEEE Transactions on Automatic Control*, vol\. 69, no\. 10, pp\. 6668–6683, 2024\.
- \[71\]A\. K\. Bozkurt, Y\. Wang, M\. M\. Zavlanos, and M\. Pajic, “Learning optimal strategies for temporal tasks in stochastic games,”*IEEE Transactions on Automatic Control*, vol\. 69, no\. 11, pp\. 7387–7402, 2024\.
- \[72\]Y\. Kantaros and J\. Wang, “Sample\-efficient reinforcement learning with temporal logic objectives: Leveraging the task specification to guide exploration,”*IEEE Transactions on Automatic Control*, vol\. 70, no\. 5, pp\. 2873–2888, 2024\.
- \[73\]M\. Cai and C\.\-I\. Vasile, “Safety\-critical learning of robot control with temporal logic specifications,”*IEEE Transactions on Automatic Control*, 2025\.
- \[74\]K\. Dole, A\. Gupta, J\. Komp, S\. Krishna, and A\. Trivedi, “Event\-triggered and time\-triggered duration calculus for model\-free reinforcement learning,” in*2021 IEEE Real\-Time Systems Symposium \(RTSS\)*\. IEEE, 2021, pp\. 240–252\.
- \[75\]J\. Ouaknine and J\. Worrell, “On the decidability and complexity of metric temporal logic over finite words,”*Logical Methods in Computer Science*, vol\. 3, 2007\.
- \[76\]R\. T\. Icarte, T\. Q\. Klassen, R\. Valenzano, and S\. A\. McIlraith, “Reward machines: Exploiting reward function structure in reinforcement learning,”*Journal of Artificial Intelligence Research*, vol\. 73, pp\. 173–208, 2022\.
- \[77\]M\. Towers, A\. Kwiatkowski, J\. Terry, J\. U\. Balis, G\. De Cola, T\. Deleu, M\. Goulão, A\. Kallinteris, M\. Krimmel, A\. KG*et al\.*, “Gymnasium: A standard interface for reinforcement learning environments,”*arXiv preprint arXiv:2407\.17032*, 2024\.
- \[78\]S\. Hochreiter and J\. Schmidhuber, “Long short\-term memory,”*Neural computation*, vol\. 9, no\. 8, pp\. 1735–1780, 1997\.
- \[79\]J\. Schulman, F\. Wolski, P\. Dhariwal, A\. Radford, and O\. Klimov, “Proximal policy optimization algorithms,”*arXiv preprint arXiv:1707\.06347*, 2017\.
- \[80\]A\. Raffin, A\. Hill, A\. Gleave, A\. Kanervisto, M\. Ernestus, and N\. Dormann, “Stable\-baselines3: Reliable reinforcement learning implementations,”*Journal of machine learning research*, vol\. 22, no\. 268, pp\. 1–8, 2021\.
- \[81\]T\. Yamaguchi, B\. Hoxha, and D\. Ničković, “Rtamt–runtime robustness monitors with application to cps and robotics,”*International Journal on Software Tools for Technology Transfer*, vol\. 26, no\. 1, pp\. 79–99, 2024\.
- \[82\]A\. K\. Bozkurt, Y\. Wang, and M\. Pajic, “Model\-free learning of safe yet effective controllers,” in*2021 60th IEEE Conference on Decision and Control \(CDC\)*\. IEEE, 2021, pp\. 6560–6565\.
- \[83\]A\. K\. Bozkurt, Y\. Wang, M\. M\. Zavlanos, and M\. Pajic, “Model\-free reinforcement learning for stochastic games with linear temporal logic objectives,” in*2021 IEEE International Conference on Robotics and Automation \(ICRA\)*\. IEEE, 2021, pp\. 10 649–10 655\.
- \[84\]A\. K\. Bozkurt, Y\. Wang, and M\. Pajic, “Secure planning against stealthy attacks via model\-free reinforcement learning,” in*2021 IEEE International Conference on Robotics and Automation \(ICRA\)*\. IEEE, 2021, pp\. 10 656–10 662\.

![[Uncaptioned image]](https://arxiv.org/html/2608.13625v1/bozkurt.jpg)Alper Kamil Bozkurtreceived the B\.S\. and M\.S\. degrees in computer engineering from Bogazici University, Istanbul, Turkey, in 2015 and 2018, respectively\. He obtained a Ph\.D\. degree in computer science from Duke University, Durham, VA, USA\. He is currently a postdoctoral associate at Virginia Commonwealth University, Richmond, VA, USA\. Previously, he was a postdoctoral associate at University of Maryland, College Park, MD, USA\. His research interests lie at the intersection of machine learning, control theory, and formal methods\. In particular, he focuses on developing learning\-based algorithms that synthesize provably safe and reliable controllers for robotics and cyber\-physical systems\.![[Uncaptioned image]](https://arxiv.org/html/2608.13625v1/zhang.jpeg)Shangtong Zhangis an Assistant Professor in the Department of Computer Science at the University of Virginia, Charlottesville, VA, USA, directing the Sequential Intelligence Lab \(SIL\)\. His research focuses on both theoretical and empirical aspects of reinforcement learning, resulting in multiple scholarly articles in major AI venues, e\.g\., JMLR, NeurIPS, ICML, and ICLR\. He also regularly serves as Area Chair in major AI venues, e\.g\., NeurIPS, ICML, ICLR, Senior Area Chair in RL Conference, Action Editor in TMLR, and panelists and reviewers for major federal \(e\.g\., NSF\) and international \(e\.g\., Schmidt Sciences\) funding agencies\. He and his research are recognized by multiple awards and honors, including best paper awards at ICML workshop and AAMAS, NSF CAREER Award, AAAI New Faculty Highlights, Google Research Award, Cisco Faculty Research Award, Nvidia Academic Grant, Rising Star in AI, NeurIPS Top Area Chair, and IFAAMAS Victor Lesser Dissertation Award \(runner\-up\)\. He obtained his DPhil at the University of Oxford, Oxford, UK, MSc at the University of Alberta, Edmonton, AB, Canada, and BSc at Fudan University, Shanghai, China\.![[Uncaptioned image]](https://arxiv.org/html/2608.13625v1/motai.jpg)Yuichi Motaireceived the B\.Eng\. degree in instrumentation engineering from Keio University, Tokyo, Japan, in 1991, the M\.Eng\. degree in applied systems science from Kyoto University, Kyoto, Japan, in 1993, and the Ph\.D\. degree in electrical and computer engineering from Purdue University, West Lafayette, IN, USA, in 2002\. He is currently an Associate Professor of Electrical and Computer Engineering at Virginia Commonwealth University, Richmond, VA, USA\. His research interests include the broad area of sensory intelligence, particularly in data analytics, pattern recognition, computer vision, and sensory\-based robotics\.