About Time: Model-Free Reinforcement Learning with Timed Reward Machines

1 Introduction

Reinforcement Learning (RL) [Sutton and Barto, 2018] has become a foundational paradigm for sequential decisionmaking, enabling agents to learn optimal behavior through interactions with an environment. A crucial aspect of any RL problem is the reward specification, which defines the agent's learning objective. Traditionally, rewards are assumed to depend only on the current state and action, conforming to the Markov property. However, many real-world tasks require objectives that depend on the history of states and actions, such as completing a sequence of tasks or avoiding repeated errors. To address this, non-Markovian reward formalisms have been developed, with reward machines (RMs) emerging as a prominent approach.

∗ Part of this work was carried out while Rajarshi Roy was at the University of Liverpool, UK.

Reward Machines [Icarte et al., 2022] are finite-state automata that specify structured, history-dependent reward functions. They provide a compact and expressive way to encode high-level objectives and have been successfully integrated into RL frameworks, improving sample efficiency and interpretability. However, a critical limitation of existing RMs is their inability to express timing constraints, which are vital for time-sensitive applications such as robotics and autonomous driving [Mehdipour et al., 2023; Sadigh et al., 2018]. For instance, an AV might need to "slow down for 3 seconds to allow a pedestrian to cross" or "avoid an unsafe road for at least 10 seconds".

In this paper, we propose timed reward machines (TRMs) that enhance reward machines with fine-grained timing requirements. To this end, we augment reward machines with clocks that track elapsed time and use them to impose timing constraints, drawing inspiration from the timed automata (TA) literature [Alur and Dill, 1994]. TRMs thus allow reward functions to depend not only on the agent's history of states and actions, but also on the time intervals between events. Moreover, TRMs can assign costs and rewards to both states and transitions, incentivizing the agent to complete a task in a timely manner while optimizing the overall reward.

Example 1. To illustrate our setting, we define a simple TRM (Fig. 1b) on the standard Taxi domain (Fig. 1a). The TRM encourages a taxi agent to drive slowly, e.g., due to heavy traffic, by providing a higher reward when it delays at each step (enforced by a self-loop with timing constraint x > 1). Additionally, it imposes a deadline for picking up the passenger (enforced by a transition with timing constraint y ≤ 14). Finally, after pickup, the agent must reach the destination while driving slowly. Such time-sensitive objectives, involving delays and deadlines, can be naturally captured by TRMs.

We interpret TRMs over Markov decision processes (MDPs) to model stochastic environments (Section 3). To express timing constraints, we augment the MDP action set with explicit delay actions. We then study two standard timing interpretations-digital-clock (Section 4) and real-time (Section 5)-also known as integer-clock and dense-time interpretations in TA literature [Henzinger et al., 1992]. For each setting, we devise tabular Q-learning algorithms on product MDPs obtained by integrating the TRM in the environment.

In the digital-clock case, the product construction is straightforward: integer clock valuations are directly included in the MDP state space. In the real-time case, we consider two approaches: (i) discretized time for continuous delays, and (ii) a corner-point abstraction based on region construction of timed automata, which encourages agents to pick delays that are very close to integers. We further enhance these algorithms with novel counterfactual imagining (CI), inspired by [Icarte et al., 2022], to incorporate alternative clock valuations and timing delays. We also provide a detailed theoretical analysis of all the presented settings, including guarantees of convergence to (ε-)optimal policies.

Figure 1: An illustration of TRM on Gym Taxi domain.

Our algorithms based on TRMs, as opposed to standard reward machines (without delay actions), can enforce timing constraints and therefore obtain higher rewards that may depend on precise timing. We demonstrate this in Fig. 1c for our running example under both digital and real-time interpretations. Our detailed experiments, involving several TRMs over standard RL benchmarks (Section 6) reveal clear differences between the digital and real-time settings: in scenarios requiring substantial delays, the corner-point abstraction often yields better returns. Moreover, we consistently observe higher returns from our CI heuristics.

Related Work. We contrast our work with existing approaches, presenting them in order of relevance.

RL with Timed Specifications. To our knowledge, only a handful of works consider time-sensitive logical reward specifications for RL. [Xu and Topcu, 2019] optimize Metric Temporal Logic (MTL) objectives by translating them into (simple) timed automata, considering only the digital-clock setting. [Dole et al., 2021; Dole et al., 2023] study subclasses of Duration Calculus that compile to variants of timed automata. Both lines of work use timed automata as monitors (reward 1 for accept, 0 for reject) to maximize satisfaction.

Unlike declarative specifications, TRMs give designers fine-grained control over reward logic, including state-based delay costs and transition-based rewards, while retaining standard Markovian rewards on MDPs. We also study both digital-clock and real-time variants, together with several heuristics, theoretically and experimentally. Finally, sparse terminal rewards frommonitors are often ineffective in longhorizon tasks, see [Roy et al., 2026, Sec. 7.3] for justification.

RL with Non-Markovian Rewards. To specify nonMarkovian rewards, the most widely used formalisms are temporal logics and finite-state machines (FSMs). Among temporal logics, there has been particular focus on Linear Temporal Logic (LTL) [Camacho et al., 2019; Hasanbeig et al., 2019; Bozkurt et al., 2020; Jothimurugan et al., 2021; Shao and Kwiatkowska, 2023]. Most of these approaches focus on translating formulas into FSMs, which are the operational structures used to guide learning.

FSMs are central to non-Markovian RL due to their compositional structure. Reward machines (RMs) [Icarte et al., 2022] provide a general means of defining rewards in the FSM structure. Reward machines have been extended widely: stochastic transitions [Corazza et al., 2022], ω-regular properties [Hahn et al., 2023], partial observability [Icarte et al., 2019], multi-agent settings [Neary et al., 2021] and continuous-time MDP [Falah et al., 2023; Falah et al., 2025].

None of these works addresses fine-grained timing constraints as considered in this paper.

Timed Automata in Control and Planning. Timed automata [Alur and Dill, 1994] are a well-established formalism for modeling and verifying systems with time-dependent behavior [Bozga et al., 1998; Larsen et al., 1997]. Quantitative variants of TA, such as priced timed automata [Behrmann et al., 2001; Bouyer et al., 2004a] and weighted timed automata [Alur et al., 2001], which are extensions with costs or rewards, have been used in strategy synthesis [Behrmann et al., 2007; David et al., 2015] and planning [Bouyer et al., 2004b; Bouyer et al., 2008; Tollund et al., 2024].

Most of these works are model-based, using deductive methods (e.g., symbolic synthesis or game-theoretic techniques) to compute optimal strategies or plans. In contrast, we show that timed reward structures can be operated in a model-free RL setting using statistical methods.

2 Preliminaries and Background

Markov Decision Process. A (labeled) Markov Decision Process (MDP) [Sutton and Barto, 2018] is a tuple M = (S, A, T, R, γ, AP, L), where S is a finite set of states, A is a finite set of actions, T : S ×A×S → [0, 1] is a probabilistic transition function, R : S × A × S → R is a reward function for the immediate rewards, γ ∈ [0, 1) is a discount factor, and L : S × A → 2AP is a labeling function that maps each state-action to a set of propositions AP.

A policy for an MDP is a mapping π : (S×A)∗S → ∆(A) that assigns a distribution over actions for a given history of states and actions. For Markovian rewards, it suffices to consider deterministic and positional policies π : S → A. The expected cumulative reward for a policy π is defined as: V π (s) = Eπ [∑∞t=0 γ tR(st, at) | s0 = s] , where st is the state at time t, at is the action taken at time t.

Also, in this paper, we assume a fixed initial state sin of the MDP, and denote the value of a policy as V π = V π (sin).

Q-learning. Reinforcement learning (RL) learns policies that maximize discounted reward in MDPs. In model-free RL, the agent samples the environment without explicit transition or reward models. Q-learning, a standard model-free method, learns the optimal action-value function Q : S × A → R, the expected return of taking a in s and then following the optimal policy. The Q-update rule is given by: Q(s, a)←Q(s, a) + α[R(s, a) + γ max a′ Q(s′ , a′ )-Q(s, a)],

where α is the learning rate, R(s, a) is the immediate reward received for action a in state s, and s′ is the next state.

3 ProblemFormulation

3.1 Timed RewardMachine (TRM)

We extend classical timed automata with reward functions for the RL setting. For the reward machine formalism, we follow [Icarte et al., 2018]. In our formalism, reward machines are augmented with a set of clocks X which can assume values in the time domain T. We consider two different time settings: (1) a digital-clock setting, where T = N; and (2) a real-time setting, where T = R≥0.

A guard is a conjunction of constraints of the form ϕ := x ▷◁ c, where x ∈ X is a clock, ▷◁ ∈ {<,≤,=,≥,>} is a comparison operator, and c ∈ N is a non-negative constant. We denote the set of all guards over X by Φ(X). Given a set of clocks X, propositions AP, a TRM is a finite state machine defined as a tuple A = (U, u0, F, ∆u, ∆r), where:

• U is a finite set of states, u0 ∈ U is the initial state, and F ⊂ U is the set of terminal (sink) states;
• ∆u ⊆ U ×2AP ×Φ(X)×2X ×U is the transition relation defining the next state given the current state, active propositions in the current state, a guard over clocks, and the clocks to reset. We denote a transition using θ.
• ∆r =∆ur ∪∆θr , where ∆ur : U → [S →R] is the statebased reward function and∆θr : ∆u → [S×A×S →R] is the transition-based reward function.

While our TRM formalism is inspired by priced timed automata, it is generalized for RL frameworks, allowing general Markovian reward functions over both states and transitions.

In our setting, one can consider negative rewards to be costs. A timed word w = (d0, l0)(d1, l1) . . . (dn, ln) ∈ (T × 2AP)∗ is a sequence in which di ∈ T is a time delay at position i and li ∈ 2AP is the set of propositions observed after that delay at position i. A run Aw of a timed reward machine A on w is a sequence (u0, v0) d0,θ0,r0 -----→ (u1, v1) d1,θ1,r1 . . . dn,θn,rn

-----→ -----→ (un+1, vn+1), where, for each i, ui ∈ U is the state of the TRM, vi ∈ T|X| is the clock valuation, ri is the reward function, and θi is the transition at that position. The above run satisfies the following conditions:

• u0 is the initial state, v0(x) = 0 for all x ∈ X.
• let θi = (ui, li, ϕi, ρi, ui+1) ∈ ∆u, then the clock valuations satisfy the following condition: vi + di satisfies the guard ϕi, and vi+1 = [ρi](vi + di), where [ρi] is the reset function that resets the clocks in ρi to 0 and keeps the others unchanged.
• ri[0] = ∆θr (θi) and ri[1] = ∆ur (ui) are the transitionand state-based reward functions at position i, resp.

A TRMA is deterministic, if for every state u ∈ U, every set of propositions l ∈ 2AP, and every pair of guards ϕ1, ϕ2 ∈ Φ(X) such that (u, l, ϕ1, ρ, u′ ) ∈ ∆u and (u, l, ϕ2, ρ′ , u′′ ) ∈ ∆u, it holds that ϕ1 ∩ ϕ2 = ∅. As is a common assumption in the literature on reward machines [Icarte et al., 2018], we only consider deterministic TRMs.

Interpretation of TRM onMDPs. We model the environment as an MDP M = (S, A′ , T, γ, L, AP)1 , which extends the standard labeled MDP definition by including timing delays in action space: A′ = T×A. Here, the agent has the option to either act immediately or wait for a chosen amount of time, referred to as delay, before taking the next action. Augmenting the agent with delay actions is analogous to standard settings in timed control and games [Bouyer et al., 2004b; Behrmann et al., 2001].

In our setting, the agent's trajectory takes the form of a sequence ζ = s0 · (d0, a0) · s1 · (d1, a1) · · · (dn, an) · sn+1 ∈ (S × (T × A))∗ × S, where si ∈ S is the MDP state, di ∈ T is the delay chosen, and ai ∈ A is the action taken. Since RL algorithms typically operate on sampled finite trajectories, we

restrict attention to bounded-horizon trajectories in this work. A trajectory ζ induces a timed word wζ = (d0 +

1,L(s0, a0)) . . . (dn + 1,L(sn, an)), which serves as input to the TRMA. The +1 offset in the delays represents the execution duration of an action in the environment. Our choice of a unit offset aligns better with the definitions of reward machines; setting all delays di = 0 yields a standard untimed word. One could, however, easily consider the action duration to be any constant c ∈ R offset. By doing so, we allow general real-time interpretation of MDPs.

On a timed word wζ , the TRM A produces a run Aζ : (u0, v0) d0+1,θ0,r0 -------→ (u1, v1) d1+1,θ1,r1 -------→ . . . dn+1,θn,rn -------→ (un+1, vn+1). We now define the discounted cumulative reward for a trajectory ζ. This definition follows the standard treatment of discounting in decision processes with sojourn times, as presented in [Puterman, 1994, Eq 11.3.1].

Following that framework, each decision point occurring at time ti contributes a discounted reward of γ ti · Ri to the total return, where Ri denotes the total reward accumulated during the transition from state si to si+1 after taking action ai. The reward Ri consists of two parts: the lump-sum reward rθ i (si, ai, si+1) obtained from the transition θ in A and the state-based reward ru i (si) obtained from the state u in A, accrued over the interval [ti, ti+1]. Formally, the total discounted cumulative reward is defined as:

1 We here drop the Markovian reward R as it is given by a TRM.

• rθ i =∆θr (θi) is the transition-based reward at point i.

We calculate the state-based reward ru i differently for the digital and real-time settings, following standard interpretations [Puterman, 1994]. In the digital clock setting, it is accumulated at each timestep during the delay period, whereas in the real-time setting, it is integrated over the delay interval.

Example 2. To explain the definitions, consider the environment and the TRM in Fig. 2. The environment has two features, p and q, which denote moving into states s1 and s3, resp. Starting at s0, the TRMA requires the agent first to observe p and then q, while satisfying simple clock constraints.

We illustrate two trajectories, ζ1 and ζ2, for this example in Table 1. The figure also summarizes, for each trajectory, the induced timed words, the TRM runs, and the resulting discounted returns. Both trajectories use the same environment actions but differ in their delay choices, which leads to different behavior under the TRM. For instance, ζ1 waits in a "good" state s1, whereas ζ2 waits in a "bad" state s2, incurring a higher cost. Consequently, in the digital-clock setting with γ = 0.9, ζ1 attains a higher discounted return (Gζ1 ≈ 6.4) than ζ2 (Gζ2 ≈ 5.1). The exact ordering holds in real-time with the same delays (≈ 6.6 vs. ≈ 5.4).

Properties of TRM. We now make some observations about trajectories and rewards in TRMs. As in classical timed automata, a trajectory in TRMs can induce arbitrarily large clock values and delays. However, one can bound them to reason about the expected cumulative reward. As standard [Alur and Dill, 1994], we rely on the maximum constant M appearing in the guards of the TRM A. Formally, v[x] = v[x] if v[x] ≤ M else v[x] = ∞ for all x ∈ X, where ∞ denotes the clock values beyond M following the usual comparison semantics, e.g., ∞ > 2 and ∞ ̸≤ 3. We also define bounded delays as d = d if d < M else d = M.

We extend this definition to trajectories: for a trajectory ζ = s0·(d0, a0) · · · (dn, an)·sn+1, we define a delay-bounded trajectory ζ = s0 · (d0, a0) · · · (dn, an) · sn+1. We can show that the delay-bounded trajectory induces a "similar" run in a TRMA to the original trajectory ζ. This follows from the fact that any clock value v[x] beyond M has the same behavior with any guards on x; see [Roy et al., 2026] for more details.

Moreover, under certain reasonable conditions, bounding the delays can improve the discounted reward. These include inducing costs for delaying in states rather than rewarding, and providing a high terminal reward for completing all tasks. Formally, the state-reward function always has negative values, i.e., ∆r(u) < 0 for every u ∈ A, and we search for "good" trajectories ζ where Gζi > 0 for all decision points i, Gζi being the discounted return from i onward. Trajectories as ζ can occur, e.g., when terminal rewards along ζ are sufficiently large. The following lemma presents this idea.

Lemma 1. Let A be a TRM, ζ be a trajectory of A and ζ be its delay-bounded trajectory. If (1) ∆ur (u) < 0 for all u ∈ U; and (2) Gζi > 0 for all 0 ≤ i ≤ n, then Gζ ≥ Gζ .

Based on the assumptions of Lem. 1, we can bound the delay space to D = T ∩ [0,M]. In our setting, policies are defined as π : (S ×D×A)∗S → D×A, which map a trajectory to a bounded delay and an action. We call such policies delay-discounted policies, as the reward functions defined in Eq. 1 incorporate the discount factor to delays as well.

The expected cumulative reward of a policy π is then the expected discounted sum of rewards over all possible trajectories following π from state s: V π (s) = Eζ∼π[Gζ | ζ[0] = s]. A policy π is optimal (resp., ε-optimal) if V π = V ∗ (resp., V π ≥ V ∗ - ε), where V ∗ = supπ V π (s).

Problem 1. Given a TRM A and a MDP M, find a delaydiscounted (ε-) optimal policy π∗ .

In the following sections, we propose algorithms for Problem 1, both in the digital-clock (dc) and real-time (rt) settings.

4 The Digital Clock Setting

Cross-product space. Themost important aspect of our approach is the construction of a cross-product between the underlying MDP M and the TRM A. The cross-product MDP M⊗dc = M⊗ A is similar to what is done for classical reward machines, except that one needs to keep track of the clock values as well. For this, we again consider the maximum constant M appearing in the guards of clock x ∈ X of A and use the symbol ∞ for clock values that go beyond M.

The cross-product M⊗dc = (S⊗,A⊗, T ⊗,R⊗) is defined as: S⊗ = S ×U ×V , where S and U are the set of MDP and the TRMstates, resp., and V = ({0, . . . ,M}∪{∞})|X| is the set of bounded clock values, A⊗ = D×A is the set of actions, T ⊗ : S⊗ ×A⊗ ×S⊗ → [0, 1] and R⊗ : S⊗ ×A⊗ ×S⊗ → R are the transition and the reward functions, resp., defined as:

for all x ∈ X, (v+d+1)[x]=v[x]+d+1 if v[x]+d+1 ≤ M, otherwise ∞; ru = 1-γ d 1-γ ∆ur (u), and rθ =∆θr (θ).

Theorem 1. An optimal positional deterministic delaydiscounted policy exists for the cross-product MDPM⊗dc .

Trajectory

ζ1: s0 ·(2, -→ )·s1 ·(1, -→)·s2 ·(0, -→ )·s3

Timedword wζ1: (2+1, {p})(1+1, ∅)(0+1, {q})

Digital case Gζ1: [5 + (-2)(1 + γ 1 )] + γ 3 [0 + (-1)] + γ 5 [10 + 0]≈6.4

Real case Gζ1: [5 + (-2)∫ 2 0 γ t dt] + γ 3 [0 + (-1)∫ 1 0 γ t dt] + γ 5 [10 + 0]≈6.6 Gζ2: [5 + (-2)∫ 2

Table 1: Description of trajectories ζ1 and ζ2 from Example 2 under digital and real-time semantics (γ = 0.9).

Due to finite state and action spaces of M⊗dc , the proof holds using standard results for MDPs [Puterman, 1994].

Q-learning on the cross-product. We adapt Q-learning to the cross-product space by modifying the Q-value updates:

where R is the reward returned by the TRM for the transition from (s, u, v) to (s′ , u′ , v′ ) under delay d and action a. Note that, unlike standard Q-learning, here in the update rule the discounting γ d+1 accounts for the delay.

The convergence follows from [Watkins and Dayan, 1992], since M⊗dc is a valid finite MDP with probabilities p((s′ , u′ , v′ )|(s, u, v), (d, a)) = p(s′ |s, a).

Theorem 2. Q-learning on the cross-product M⊗dc converges to an optimal policy under standard assumptions: every state and action pair is visited infinitely often; and the learning rate αt satisfies ∑∞t=0 αt = ∞ and ∑∞t=0 α2 t <∞.

4.1 Counterfactual Imagining for Delays

The delay actions expand the action space, so we use counterfactual imagining to efficiently explore timing alternatives. In addition to varying the RM state as usual in an untimed setting [Icarte, 2022], we also vary clock values and delays.

Formally, during the Q-learning process, given a realized transition in the cross-product MDP M⊗dc ⟨(s, u, v), (d, a), r, (s′ , u′ , v′ )⟩, we synthesize counterfactual experiences by varying the TRM states, clock values, and delays: 〈(s, ¯u, ¯ v), ( ¯ d, a), ¯ r, (s′ , ¯u′ , ¯ v′ )〉, where

Varying values ¯ v and delays ¯ d over all possibilities requires adding several alternatives due to potentially large clock range {0, . . . ,M}. To keep the number of counterfactuals manageable, we restrict attention to promising alternatives. We consider only clock values ¯ v close to the realized value v, i.e., ∥¯ v - v∥∞ ≤ rCI for a fixed radius rCI (typically < 5). We further consider only delays ¯ d that enable satisfaction of guards in the alternative TRM state ¯u under ¯ v; specifically, we include delays ¯ d for all transitions θ = (¯u, L(s, a), ϕ, ρ, ¯u′ ) such that ¯ v + ¯ d+1 |= ϕ.

5 The Real-Time Clock Setting

In the real-time case, clock values and delay actions can be real-valued, and delays can be chosen from the continuous range [0,M], enabling more precise timing of actions. This allows for more possible policies, often leading to better rewards, which we illustrate through the following example.

Example 3. Consider the example in Fig. 3. In the realtime setting, there exists a positive-valued policy, which can be seen from the trajectory: ζ1 = s0 · (0.1,-→) · s1 · (0,-→) · s2, which achieves a discounted reward of [5 + (-1)(1 -γ 0.1 )/-ln(γ)] + γ 1.1 [7] ≈ 11.13 for γ = 0.9. In contrast, there is no positive-valued policy in the digital-clock setting. For instance, similar trajectories in this setting, ζ2 = s0 · (0, -→) · s1 · (0, -→) · s2 and ζ3 = s0 · (1, -→) · s1 · (0, -→) · s2 will achieve discounted rewards of -10 + γ 1 [7] ≈ -3.7 and [5 + (-1)(1 - γ 1 )/(1 - γ)] + γ 2 [-10] ≈ -4.1, resp.

Moreover, in contrast to the digital-clock case, in the realtime setting, optimal policies may not exist, as stated below.

Theorem 3. An optimal delay-discounted policy may not exist in the real-time setting.

For instance, in Fig. 3, the best sequence (d,-→)(0,-→), 0 < d < 1, yields return Gζ = [5+ (1-γ d ) - ln(γ) (-1)] + γ (1+d) [7]. This achieves a supremum of 11.3 as d → 0+, but this is

unattainable since d = 0 violates the guard.

Therefore, our focus is on ε-optimal policies. However, the usual cross-product MDP M⊗rt has infinite state and action spaces. Thus, to apply tabular RL, we design finite, discrete abstractions and focus on deterministic positional policies.

Uniform Discretization. A typical approach to approximating real-time is to uniformly discretize time using a step size 0 < 1κ < 1, κ > 1 ∈ N. In this setting, the clock valuations would be the set Vκ = {v ∈ ([0,M]∪{∞})|X| | v[x] = c/κ or v[x] =∞ for c = 0, ...,M ·κ, for all x ∈ X} and the delay action space Dκ = {c/κ ∈ [0,M] | c = 0, ...,M · κ}. The corresponding finite cross-product MDP M⊗ud is constructed as in the digital-clock case, with the modifications to the state and action spaces. Q-learning from Sec. 4 can then be applied, yielding similar convergence guarantees.

To improve the approximation quality, one would require a larger step size κ. However, this substantially increases the size of the valuation and delay spaces, |Vκ| = (Mκ + 1)|X| and |Dκ| =Mκ+1, limiting scalability.

5.1 Corner-Point Abstraction for TRMs

To address the challenges of discretizing real-time, we adopt principled abstractions of clock values from the timed automata literature. Specifically, we adapt the corner-point abstraction based on region abstraction [Alur et al., 1992]. While previously used for priced timed automata [Bouyer et al., 2004a], we adapt it to an RL setting, interpreting TRMs over MDPs with discounted rewards.

On an intuitive level, regions partition the infinite set of clock values into finitely many equivalence classes that behave identically w.r.t. guards. Region corners, on the other hand, are the integral boundary points of a region. Typically, an RL agent is incentivized to choose delays near region corners to obtain higher returns (as in the example from Fig. 3).

To formalize these ideas, let us briefly recall the region abstraction and define region corners. Given a set of clocks X and a max-constant M, a region is a tuple (h, [X0, . . . ,Xp]), where h : X → {0, . . . ,M}, and (Xi)pi=0 is a partition of X such that for all i > 0, Xi ̸= ∅ and h(x) = M implies x ∈ X0. A valuation v is in a region if the following conditions hold: (i) ∀x ∈ X, ⌊v(x)⌋ = h(x), (ii) ∀x ∈ X, x ∈ X0 iff {v(x)} = 0 (i.e., v(x) = h(x)), and (iii) ∀x, y ∈ X, {v(x)} ≤ {v(y)} ⇐⇒ x ∈ Xi, y ∈ Xj, i ≤ j, where ⌊c⌋ and {c} denote the integer and fractional parts of c, resp. For example, the valuation v with v(x) = 1.2, v(y) = 0.5 lies in the region R = ({x : 1, y : 0}, [{}, {x}, {y}]).

Two valuations v, v are region-equivalent, denoted v ∼ v, if they belong to the same region. For a valuation v, [v] denotes the region to which it belongs. Region-equivalence can be naturally extended to trajectories and policies.

A corner point of a region R is a valuation v ∈ {0, . . . ,M}|X| with integral values for each clock and belongs to the (topological) closure of R, e.g., the corner points of the example region above are (1, 0), (1, 1), and (2, 1).

We here exploit region corners to search for policies in M⊗rt that yield higher rewards, namely corner policies. Intuitively, such policies choose delays so that the clock valuations encountered along each possible trajectory lie at region corners. The following lemma formalizes the benefits of corner policies. For a technical exposition, see [Roy et al., 2026].

Lemma 2. Given ε > 0 and any policy π in M⊗rt , there exists a region-equivalent corner policy ˆπ in M⊗rt such that V ˆπ > V π - ε for some discounting γ < 1.

This lemma restricts the search space to corner policies; however, it still remains infinite. To address this, instead of searching over the real-time cross-product MDPM⊗rt , we construct a 'finite' abstractionM⊗ca utilizing region corners.

Cross-Product for Corner-Point Abstraction. We first describe how a corner configuration (R, α) of the cornerabstraction of A, where R is a region and α is its corner point, evolves under elapsing time. Here, the agent, in addition to a delay d ∈ D = {0, . . . ,M}, chooses a region successor σ ∈ S = {-2|X|, . . . , 0, . . . , 2|X|} that assigns which region to move to associated with a corner 2 . Intuitively, applying a delay-successor tuple (d, σ) to a configuration (R, α) leads to a new configuration (R′ , α′ ) obtained as follows:

2 Some successors may be invalid or not distinct for some (R, α).

first shift both R and α by d time unit, and then choose the σth successor region associated with that corner. Formally, (R, α) ⊕ (d, σ) is the new configuration (R′ , α′ ) defined as: α′ = α + d, R′′ [h] = R[h] + d and R′ is the σth successor region of R′′ associated with α′ .

Example 4. Consider a corner configuration (R = ({x : 1, y : 0}, [{x}, {y}]), α = (1, 0)). This region contains valuations such as v(x) = 1, v(y) = 0.1. Applying delay (1, 0) leads to (R1 = ({x : 2, y : 1}, [{x}, {y}]), α1 = (2, 1)), which is the same region and corner pair offset by +1. This region contains valuations such as v(x) = 2, v(y) = 1.1. Alternatively, applying delay (1, 1) leads to (R2 = ({x : 2, y : 1}, [{}, {x}, {y}]), α2 = (2, 1)), which is the region successor of R1 associated with the same corner. This region contains valuations such as v′ (x) = 2.1, v′ (y) = 1.2. We graphically illustrate this example in [Roy et al., 2026].

We then define the cross-product MDP M⊗ca = (S⊗,A⊗, T ⊗,R⊗) as follows: S⊗ = S × U × R × C, where R is the set of regions of A, and C is the set of corner points associated with the regions; A⊗ = D × S × A, where D = {0, 1, . . . ,M} and S = {-2|X|, . . . , 0, . . . , 2|X|}; and T ⊗ : S⊗ ×A⊗ ×S⊗ → [0, 1] and R⊗ : S⊗ ×A⊗ ×S⊗ → R are defined as follows:

The required operations on regions for this construction are standard and can be computed efficiently [Alur et al., 1992].

Hence, standard Q-learning can be applied on the cornerpoint abstraction MDP M⊗ca to obtain an optimal policy. Moreover, we can prove that an optimal policy in M⊗ca can be "lifted" to an ε-optimal region-equivalent corner policy in the original real-time MDPM⊗rt . Thus, we can show that:

Theorem 4. Given ε > 0, our algorithm via Q-learning on the corner-point abstractionM⊗ca returns an ε-optimal policy π∗ for the real-time MDPM⊗rt for some discounting γ < 1.

We also design counterfactual imagining for the corner abstraction, analogous to the digital-clock setting (Section 4.1).

6 Evaluation

We implemented all proposed algorithms in Python 3 3 by extending [Icarte et al., 2022]. All TRM-specific components, including corner-abstractions, were developed from scratch.

To improve learning performance, we employ several heuristics for interpreting TRMs. First, we reduce the valuation space V using clock-specific maximum constants Mx for each x ∈ X, as is standard in timed automata. Second, we bound the delay space D by the largest constant Md appearing in guards of the form x ▷◁ c with ▷◁∈ {>, ≥, =}. There is no loss of optimality, since delays beyond Md only add cost.

3 See https://github.com/ritamraha/Timed-Reward-Machines.

Experimental Results. We address two key research questions: RQ1, the performance gains from counterfactual imagining; and RQ2, the performance differences across time interpretations. As TRMs are novel to the RL framework, there are no direct baselines to compare; we expand on the conceptual difference with other settings in [Roy et al., 2026, Sec. 7].

Our evaluation uses standard Gym [Towers et al., 2024] environments: (i) the Taxi domain, as in Fig. 1a, with propositions indicating colored pick-up locations and whether the passenger is in the taxi or at the destination; and (ii) Frozen Lake (default 8×8), augmented with three goals (a, b, c) and ten holes (h), with action success probability 0.8. Further details, including the precise TRMs, environments, and additional experimental statistics, are given in [Roy et al., 2026].

We use Q-learning with per-episode parameter decay 0.999, initial rate α0 = 0.9, initial exploration ε0 = 0.9, initial Q-values Q0 = 10, γ = 0.999 and maximum global steps of 300 K. For counterfactual imagining (CI), we select the top 15 by rewards per transition. We averaged the results of each experiment over 10 independent runs.

RQ1. We demonstrate the gain of using CI on Taxi domain with TRM1 and on Frozen Lake with TRM2. TRM1 requires the Taxi agent to pick up a passenger, visit a green location, and drop them at the destination, while satisfying several timing constraints. TRM2 requires the Frozen Lake agent to satisfy three objectives, a, b, c, sequentially, while avoiding falling into the holes, and it must also move slowly.

Fig. 4a shows that CI yields significantly higher discounted rewards in both settings by exploring additional ways to satisfy timing constraints. Fig. 4b shows that CI also significantly reduces episode time, allowing agents to be faster.

RQ2. We evaluate the performance of different timing interpretations: (i) digital-clock setting, (ii) uniform discretization with 1/κ ∈ {0.2, 0.5}, (iii) corner-point abstraction, and (iv) reward machines (RM). Note that RMs cannot choose delay actions, as it is not designed for timed specifications. We demonstrate this comparison on Taxi domain with TRM3 and Frozen Lake with TRM4. These TRMs are similar to those in the previous experiment, but with different timing constraints.

Fig. 5a shows that the corner-point abstraction consistently outperforms the other interpretations in terms of discounted return. This advantage is due to selecting delays that lie close to the guards. Fig. 5b shows that RMs lead to the shortest episodes; however, this behavior is undesirable, as completing episodes too fast violates several timing constraints.

7 Conclusion

We studied model-free RL for timed reward machines (TRMs), a formalism that augments reward machines with clocks for timing constraints. We interpreted TRMs over MDPs under digital and real-time semantics and devised abstractions for efficient RL. Our experiments show which abstractions and heuristics perform well for RL with TRMs.

This work is a step towards improving time-sensitive reward specification in RL. There are numerous avenues ahead, e.g., extending TRMs to CTMDPs [Falah et al., 2025], adapting deep RL [Fujimoto et al., 2018] to real-time, etc.

Ethical Statement

This research develops algorithms for reinforcement learning with timed reward machines. It is theoretical and involves no human subjects, personal data, or ethically sensitive experiments. While the algorithms have no direct implications for human welfare or rights, their deployment in AI systems should consider relevant ethical guidelines and societal impacts.

Acknowledgements

Rajarshi Roy, David Parker and Marta Kwiatkowska received funding from the ERC under the European Union's Horizon 2020 research and innovation programme (grant agreement No.834115, FUN2MODEL). Rajarshi Roy was also partly funded by the European Union (RobustifAI project, ID 101212818). Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or the European Health and Digital Executive Agency (HADEA). Neither the European Union nor the granting authority can be held responsible for them. Anirban Majumdar was supported by the Department of Atomic Energy, Government of India, under project no. RTI4014. We also thank Anne-Kathrin Schmuck for insightful discussions.