Regret-Free Reinforcement Learning for Temporal Logic Specifications
Authors: R Majumdar
Mahmoud Salamati
Sadegh Soudjani
Venue: ICML 2025 poster (2025)
Keywords: Markov decision process
regret-free algorithm
reinforcement learning
temporal logic tasks
formal specifications
Primary area: theory->online_learning_and_bandits
TL;DR: We provide the first regret-free reinforcement learning algorithm for satisfying high-level temporal specifications.

Abstract: Learning to control an unknown dynamical system with respect to high-level temporal specifications is an important problem in control theory. 
We present the first regret-free online algorithm for learning a controller for linear temporal logic (LTL) specifications for systems with unknown dynamics.
We assume that the underlying (unknown) dynamics is modeled by a finite-state and action Markov decision process (MDPs).
Our core technical result is a regret-free learning algorithm for infinite-horizon reach-avoid problems on MDPs.
For general LTL specifications, we show that the synthesis problem can be reduced to a reach-avoid problem once the graph structure is known.
Additionally, we provide an algorithm for learning the graph structure, assuming knowledge of a minimum transition probability, which operates independently of the main regret-free algorithm. Our LTL controller synthesis algorithm provides sharp bounds on how close we are to achieving optimal behavior after a finite number of learning episodes.
In contrast, previous algorithms for LTL synthesis only provide asymptotic guarantees, which give no insight into the transient performance during the learning phase.

Regret-Free Reinforcement Learning for Temporal Logic Specifications
Rupak Majumdar' Mahmoud Salamati Sadegh Soudjani" 12
Abstract
the temporal specification is satisfied (Icarte et al., 2018; Camacho et al., 2019; Hasanbeig et al., 2019; Kazemi et al., 2022; Hahn et al., 2019; Oura et al., 2020; Cai et al., 2021; Bozkurt et al., 2021: Sickert et al., 2016; Alur et al., 2022;
Learning to control an unknown dynamical sys- tem with respect to high-level temporal specifi- cations is an important problem in control the- ory. We present the first regret-free online algo- rithm for learning a controller for linear temporal logic (LTT.) specifications for systems with un- known dynamics. We assume that the underlying (unknown) dynamics is modeled by finite-state and action Markov decision process (MDP). Our core technical result is a regret-free learning algo- rithm for anfinite-horizon reach-avoid problems on MDPs. For general LTL specifications, we show that the synthesis problem can be reduced to a reach-avoid problem once the graph structure is known. Additionally, we provide an algorithm for learning the graph structure, assuming knowl- edge of a minimum transition probability, which operates independently of the main regret-free al- gorithm. Our LTL controller synthesis algorithm provides sharp bounds on how close we are to achieving optimal behavior after a finite number of learning episodes. In contrast, previous algo- rithms for LTL synthesis only provide asymptotic guarantees, which give no insight into the tran- sient performance during the learning phase.
Fu & Topeu, 2014; Voloshin et al., 2022). In the limit, the approximations converge to the optimal policy.
In practice. it is not enough to know that approximations converge in the limit; would prefer to know how close our current policy is to the optimal one, and to stop learning when the policy is close optimal. One way to quantify this is through regret minimization (Auer et al., 2008; Agarwal et al., 2014; Srinivas et al., 2012; Dann et al., 2017). For an online learning algorithm, intuitively, regret is defined as the difference between the accumulated rewards collected by an optimal policy and the algorithm during learning. A learning algorithm is called regret-free if the regret grows sublinearly with the number of episodes.
In this paper, we propose the first regret-free learning algo- rithm for policy synthesis against LTL objectives. We con- sider the class of systems whose dynamics can be captured by finite-state and action Markov decision process (MDP) with unknown transition probabilities and fixed initial state Sinit The objective is to synthesize policy that maximizes the probability of satisfying a given LTT. specification yo. Let n² denote an optimal policy, meaning that applying x² maximizes the satisfaction probability for p. Our online algorithm produces a sequence of policies TT, T....., one per episode. Let u² (Sinit) and (Sinie) denote, respectively, the satisfaction probabilities of n= and mi when starting from Sinit. After passing K >> episodes, define the regret as R(K) := >>=nn lated difference between the satisfaction probabilities under the optimal and learned policy. Our algorithm ensures that limx- R(K)KK =
1. Introduction
We consider the problem of learning an optimal control pol- icy for stochastic system, whose dynamics are unknown, with respect to linear temporal logic (LTL) specifications. This is a core problem in control and robotics, with a rich body of existing techniques. A fundamental approach to the problem to apply reinforcement learning (RL): the agent maintains a model of the world learned through ex- ploration, and computes sequence of approximations to optimal control policy that maximizes the probability that
(i(niit)) ), the accumu-
We first state our algorithm for reach-avoid specifications, the subset of LTT. specifications that require set of goal states must be visited while avoiding hitting set of bad states. In every episode, our algorithm (1) computes an interval MDP (iMDP) by taking all the collected state ob- servations into account; (2) finds an optimistic policy over the computed iMDP to solve the reach-avoid problem; and (3) executes the computed policy before an ppisode-spectfi deadline reached. We prove that the regret of our al-
'MSS-WWS, Kaiserslauter, Germany University of Birming- ham, Birmingham. UK. Correspondence to: Mahmoud Salamati <msalamati @ mpp-sws.oo sopor....org>...
Proceedings of the nnnd International Conference Machine Learning. Vancouver, Canada. PMLR 267, 2025. Copyright 2025 by the author(s).

---

Regret-Free Reinforcement Learning for Temporal Logic Specifications
Ponti
it regret-free. We utilize a reset mechanism that enables a systematic trade-off between exploration and exploitation, and can be applied to non-communicating MDPs. This is unlike the previous work by Tarbouriech et al. (2020), which is limited to strictly positive cost structures and prop- erties with satisfaction probability one, and surpasses the limitations of UCRL2-like algorithms, which require the un- derlying MDP to be communicating, The ability to handle non-communicating MDPs is key since the product of an MDP and an automaton for the temporal specification makes in general the product MDP to be non-communicating.
Graph identificution (Alg.5 5)
Alg.
6
Regret-free policy synihesis
ITk
Agent
17
(Alg. 1)
Rc+1
T(-
&e, (+,)))
Eq. (10)
State observations
Figure I: Overview of the approach: the LTL specification o0 along with the graph learned through the application of Alg. are used reduce the general synthesis problem into reach-avoid problem. The confidence parameter d (0, 1) and the lower bound on the minimum transition probability Pmiin E (0, 1) are used to compute the regret bound for Alg. 1 and the sample complexity for Alg. 5, respectively. Applying Alg. yields a policy Ty (using Alg. 2) and an episode length H3 (using Eq. (7)), both of which are passed to the agent for execution in episode 2 1. The agent, mod- eled as finite MDP with transition function T, executes the policy Te for at most H3 time steps starting at state sinit, and passes the observed transitions back to the policy.
We have implemented our algorithm with empirical eval- uation on reach-avoid specifications in a gridworld envi- ronment reported in App. C. In particular, we compare the performance and convergence of our algorithm to the sam- ple complexity and convergence of PAC-MDP algorithm for LTL. (Perez et al., 2024), and show that our algorithm convergences faster within smaller number of episodes.
2. Related Work
We discuss existing results in four related domains.
Reinforcement Learning for LTL Specifications With- out Guarantees: In recent years, substantial research has focused on the policy synthesis problem for systems mod- eled as finite MDPs with unknown transition probabilities, where the objective is to satisfy tasks specified by LTL for- mulas. Early results focused only on finite-horizon LTL specifications. Icarte et al. (2018) introduced reward ma- chines, which use finite state automata to encode finite- horizon specifications along with specialized (deep) Q- learning algorithms. Camacho et al. (2019) later formal- ized the automatic derivation of reward machines for finite- horizon LTL specifications. The development of good-for- MDP automata, such as limit deterministic Büchi automata (LDBA), for representing LTL formulas has led to signif- icant advances in reinforcement learning for the full class of LTL specifications, including the -oriitee ones (Sickert et al., 2016; Hahn et al., 2020; Kazemi et al., 2022; Hasanbeig et al., 2023). Typically, one has to first trans- late the given LTL formula into an appropriate automaton, such as an LDBA, and then compute the product of this automaton with the MDP to formulate the final (discounted) learning problem. This formulation ensures that, with a suffi- ciently large discount factor (depending on system dynamics and the specification). applying standard RL algorithms will lead the policy to converge asymptotically to the optimal one (Kazemi et al., 2022; Bozkurt et al., 2021; Oura et al., 2020). Translation of the LTL formula to an average objec- tive for RL using the automaton construction is also studied by Kazemi al. (2025). However, these methods do not provide a finite-time performance, and the required discount factor is not known in advance.
gorithm grows sublinearly with respect to the number of episodes.
Next, for general LTL specification, we show that the syn- thesis problem can be reduced to a reach-avoid problem if we know the graph structure of the MDP. Finally, we pro- vide a polynomial algorithm for learning the graph structure of the MDP based only on having a positive lower bound on its non-zero transition probabilities. Fig. 1 provides an overview of our proposed online policy learning algorithm. Policy learning can be stopped after k* 2 1 episodes if the average regret R(k*) )/k" becomes sufficiently small, indi- cating that the learned policy's 's satisfaction probability is nearly optimal on average, with confidence at least - 8. This can be verified using our proposed regret bounds.
There exist regret-free algorithms for solving infinite- horizon policy synthesis problems, but they cannot be ap- plied to our problem as we will discuss in more detail in Sec. 2. Our primary objective is to minimize the regret with respect to an optimal policy that maximizes the satisfaction probubility of a specification. The regret for each episode naturally bounded by one, which gives the regret bound of O(K) for any arbitrary learning algorithm. To achieve regret-free algorithm, we define an episode-specifie dead- line that categorizes learning episodes as fast or slow, We prove that the number of slow episodes exceeding the dead- line grows sublinearly. The deadline is set such that the regret from fast episodes also grows sublinearly. Thus, the total regret of our algorithm increases sublinearly, making
2

---

Regret-Free Reinforcement Learning for Temporal Logic Specifications
Reinforcement Learning for LTL Specifications With Guarantees: The two most popular metrics for evaluating the performance of learning algorithms are probably ap- proximately correct (PAC) and regret bounds. Fu & Topeu (2014) have provided a PAC learning algorithm for synthe- sizing policies to satisfy finite-horizon LTL specifications over finite MDPs with unknown transition probabilities. However, the sample complexity of the algorithm scales explicitly with the horizon length, rendering it unsuitable for infinite-horizon LTL specifications. Subsequently, surprising negative result was established: full L.T. is not PAC-Icarnable (Yang et al., 2022; Alur et al., 2022). A closer analysis reveals that this result primarily stems from the assumption of an unknown minimum transition proba- biliiy. By instead assuming known minimum transition probability, Voloshin al. (2022) proposed PAC-learnable policy synthesis method that relies access to generative model capable of sampling from any arbitrary state-action pair. In many realistic scenarios, this is impractical since initializing the MDP at arbitrary states is not feasible. Our proposed algorithm does not require access to a generative model. Recently, Perez et al. (2024) have also proposed another PAC learning algorithm that does not rely on gen- erative model. However, there is still no regret-frec online algorithm for policy synthesis to satisfy LTL. specifications.
proposed by Tarbouriech et al. (2020) provides sublinear regret bounds for the accumulated cost in MDPs, assuming that (1) there exists a proper policy under which the system reaches the goal with probability one, and that (2) all costs are positive. The authors argue that these two restrictions can be relaxed by assuming the knowledge of an upper bound on the accumulated cost and by perturbing the costs. However, none of these workarounds can be applied to our setting, we are interested in computing the regret bounds with respect to the satisfaction probability under an optimal policy. Nevertheless, relaxing the aforementioned restrictions results in the algorithm by Tarbouriech et al. (2020) giving a regret bound of O(K2/3), which is strictly larger than our regret bound of (K11/2) with K' being the number of episodes.
3. Preliminaries
Notation: For matrix X E Rm we de- fine the infinity norm of the matrix by || mo = maxişism Σj=1 (i, For a vector I E I", we de- fine the & and fo norms as ||<|| = Σ [=(() and |||| == maxisign [zz(t),, respectively. Given two in- tegers a, b with a S b, we denote the set of integers {a, a+1...... b3 by (a; bj. For a set S, we denote by S+ the set of all non-empty finite sequences from the elements of S. Let @ denote the empty set. For sequence a E Stt we define the corresponding last element by last(a). The set of positive integers is denoted by N and the set of non-negative integers by No. We use |A| to denote the cardinality of set A (i.e., the number of its elements).
Regret-Free Reinforcement Learning for Communicat- ing MDPs: UCRL and UCRL2 are well-known regret-free learning algorithms developed for communicating MDPs (Auer et al., 2008; Auer& & Ortner, 2007). The definition of regret in the context of communicating MDPs is par- ticularly well-suited to our objective: it is evaluated over an infinite sequence of states without discounting future observations, which aligns closely with the requirements of infinitehhorizon L.T. specifications. A key advantage of learning in communicating MDPs is that it can proceed indefinitely without requiring environment resets. However, in the setting we consider, even if the underlying MDP is communicating, its product with the automaton representing the specification may result in a non-communicating MDP (Kazemi et al., 2022). Fruit et al. (2018) address this by proposing a regret-free algorithm for non-communicating MDPs where the initial state lies within a non- con-transient subset of states. In contrast, our setting assumes a fixed initial state from a transient subset, rendering algorithms like UCRL2-which are tailored for communicating MDPs- inapplicable.
MDPs: For set X, we write A A(X) for the set of probabil- ity distributions over X. Let AP be a fixed set of atomic propositions. A labeled MDP M (S, A, T,, Sinit L, AP) consists of finite set S of states, finite set A of actions, transition function T: S x A + ASS), an initial state Sinit E S, and a labeling function L: S + 2AP that maps states to subsets of atomic propositions AP. The underly- ing graph of an MDP M is defined as x(M) = (S, A, F), where (s, a, s') E if and only if T(s'ss, a) >
An iMDP is defined similarly to MDP, but instead of single transition probability, each transition is specified by an interval of possible probabilities. Formally, an iMDP is a tuple M = (S, A,T, Sinit; L, AP), where T: S x A + ((S) is an interval transition function, and I(S) denotes the set of mappings that assign to each s' E S a closed interval [1(s'), u((")) S [0, 1], such that Eves 1(s) 5 $14 S Eves u(s")
Regret-Free Reinforcement Learning for Non- Communicating MDPs: Goal-oriented reinforcement learning is key class of problems in RL, often formulated as a shortest path problem (SPP) for MDPs with unknown transition probabilities. Recent theoretical results include the works by Tarbouriech et al. (2020) and Rosenberg et al. (2020). In particular, the online learning algorithm
A policy for the MDP is mapping : S + A(A) that gives probability distribution T(σ) E A(A) for select- ing the next action depending on a E St, which is the nonempty finite sequence of states representing the past
3

---

Regret-Free Reinforcement Learning for Temporal Logic Specifications
history. A policy æ is memoryless if T(o) (s) for all S ending in and for all E S. Let IT denote the set of all deterministic positional policies over M, that is the set of functions :: S + A. By fixing a policy π E II, the MDP M reduces to a Markov chain C = (S, P, Sinit, I., A AP), where P : S - A(S) is formed by composing the pol- icy т with the transition function T.
We define the regret of the learning algorithm as
K
R(K)= = Σ (sinit) - 2 (Pinit)))
(I)
where K is the number of episodes, and the normalized regret as
A key concept for checking satisfaction of specifications is maximal end components (MECs) of the MDP (Baier & Katoen, 2008). These components are sub-MDPs that are probabilistically closed, meaning that (1) there exists a positional policy under which the probability of reaching any state from any other state in the MEC is equal to one, and (2) the MEC cannot be exited under any positional policy. An MDP is said to be communicating if consists of single MEC that includes all states.
R(K) K
Ra (K)
A learning algorithm called regret-free if its regret R(K) grows sublinearly with respect to the number of episodes K, i.e., if R. (K) - 0 as K + co. A regret-free algorithm can achieve arbitrary small values of normalized regret. Suppose we fix a threshold ε E (0, 1) and terminate the learning algorithm once the corresponding normalized regret goes below E. We can consider the smallest number of episodes ke E N after which R, (k*) < & with confidence 8 as a complexity metric for the proposed learning algorithm with parameters 6, E (0, 1).
Linear Temporal Logic: We consider specifications in Lin- car Temporal Logic (LTL) (Baier & Katoen, 2008). Formu- las in LTL are constructed inductively over a set of atomic propositions AP according to the syntax
s : : - th A 22 OOb| 1/1 U U/2
4. Regret-Free Learning for Until Formulas
where p AP. The semantics of LTL is defined on infinite sequences of elements from 24P. Let
We first consider the special case of regret-free learning for MDPs with unknown (but fixed) transition function and until formulas that correspond to reach-avoid specifications.
0o. o..... be an infinite sequence of elements from 24" and define ofi]] = dj, 01t1.... for any i E No. Then the satisfaction relation between a and a property v/. expressed in LTL, is denoted by a + th. We have a - pf E og- Furthermore, - v1 and l/2. For next operator, a + OO holds if o[1] + vh The until operator a = wh U 1/2 holds if 7i E No ali] == 422 and Vj- E J < i, oا } v/1 We define derived operators such as disjunction (V), eventually (0),
For two distinct atomic propositions Goal and Avoid, we consider the until formula (also called reach-avoid for- mula) of the form 9 = -Avoid U Goal. Let M, (S, A, T, Sinit, L, { Goal, Avoid }) be the MDP obtained by making states satisfying Goal and Avoid absorbing. We use G and B to denote the sets of states which satisfy the atomic propositions Goal and Avoid, respectively. For notational convenience, write M instead of M, for the remainder of this section.
= - if j and a + 1 1/2
and globally (O) in the usual way.
Maximum Probability of Satisfaction: Take an MDP M and an LTL specification yp. A path 80, 81,... of M with F= p. For every policy π, the set of paths starting at Sinit that satisfy yp is measurable. Thus, we can define pr. (1)), the probability that M under policy π satisfies so, where with abuse of notation, we write yp for the set of paths satisfying yp. Define the optimal probability of satisfying yp with u² (sinit) sup, I oi (Sinit) = P satisfiable with positive probability, i.e., 0² (Sinit) > 0. This without loss of generality since any learning algorithm for the case 8² (Simit) = 0 has zero regret.
Problem 1. [Regret-Free Learning for Until Formulas] Given an MDP M with an unknown transition function, an until formula o = AAvoi Goal, a confidence pa- rameter 8 E (0, 1). and minimum transition probability Pmin E (0, 1), find an online learning algorithm such that with confidence at least (1 -1-0 6), the regret defined by
50 Sinit satisfies yp if ((
Eq. (1) grows sublinearly with the number of episodes K.
Aint (v)), and let n=" denote the optimal policy, i.e.,
swa (v)). We assume that the specification is
4.1. Methodology
Alg. 1 shows our learning algorithm. It uses the paradigm of optimism in the face of uncertainty. Learning takes place over consecutive environmental episodes. Each episode is finite sequence $1, Q1, $2, .., that starts from the initial state of M, i.e., $1 = sinit and ends if either an absorbing state in G is reached, meaning that sy E G, or an episode-speciffc deadline is reached.
Regret Analysis: Our aim is to learn the optimal policy n² that maximizes 1p= (Φ). Learning takes place over consec- utive episodes. In episode k we learn a policy Tg. and write uk (sinit) = I (4)). which is the probability of satisfying the specification j under the policy Tg.
4

---

Regret-Free Reinforcement Learning for Temporal Logic Specifications
Algorithm 1 Regret-free algorithm for until formulas
Algorithm 2 Extended value iteration (EVI)
(ZeroReg)
State and action sets S and A, sets G and B, set of plausible transition functions TE, start time of the h episode tg. minimum transition probability Priin
Input:
Input: State and action sets S and A, initial state Sinit
sets G and B, confidence parameter E (0, 1), minimum transition probability Pmin
Set = 0, (o(s) = 0 for s & G and Po(s) = for 8 E G
Initialization: Set t = 81 = Sinit
repeat
for episodes 1 1, .... do
1 < [++1 for s S do
Construct iMDP M₁:
lA Set as) = 1[t < tx: 8 = 5, =
for a E A do
(T(.(s,a) InnerMax a, Thi 111-1)
For all s, E S and a E A compute the empirical transition function
end for **(8) = arg max Eves Ta (,, a))
(s) Eves Ta(s' (1)
Te(5'18,a) = 1 9t s, = a, 81+1 = s')
end for
max (1, Ns(ss,))
until || - 1 < min 1
25x Priin
Define the iMDP M₁ = (S, A, Tk, Sinit; I., AP) with the set of transition functions Ta satisfying Eq. (3) Compute policy ææ:
Construct the MDP Mr = (S, A, Tk. Sinits L, AP) Results: (M,, *x) EVI (S, A, G, B, The lk: Punin)
Use Alg. 2 to find an optimistic MDP Mr and a policy Tg. i.e. (M₃ f&) = EVI(S, A, G, B, Te, the Penin) Execute policy T&: Compute the deadline H2 using Eq. (7) while & G and (t - 1x) < H& do
particular, we define M₁ = A, Tk. Sinit: L) as the iMDP with interval transition function Tr. such that, with proba- bility at least (1 8/3), every transition function F E Ti satisfies
if 9, & B then
|F(1,, Ta(-1s,))ll Ba(s,a),
(3)
Observe the next state 81+1 by executing 7x (8t)
else
where
St+1 Sinit end if t +-+ ++1
Bx(s,0) 8|51 log (2) A a)))
(4)
N (s,
end while end for
and N (s, a) := max(1, (N, o)). Intuitively, we pick the confidence bound 5 on the right hand side of Eq. (3), such that the corresponding inequality holds with high confidence. More concretely, have the following result.
Each episode proceeds follows: (1) construct iMDP from observations such that it contains the true MDP with high confidence; (2) identify an optimistic MDP and com- pute an optimistic policy; and (3) execute the policy and collect data until termination. We describe each of these steps in detail below.
Lemma 4.1. Let & = 1 (M E Ma)- Then TP(E) 2 8/3.
The above lemma states that the true MDP M lies within the iMDP MM, constructed from observations, with high prob- ability. Next, describe the policy synthesis procedure based on ME.
Constructing an iMDP from observations: The main ob- jective of this step is to use the collected data-namely, the visited state-action pairs (st, 0z) and the corresponding transitions (st, at, St+1 - compute an empirical transition function and construct an iMDP that contains the true MDP with high confidence.
Computing optimistic policy: from the observations in the previous step, an optimistic MDP is a specific MDP selected from the uncertainty set- defined by interval transition probabilities- maximizes the probability of reaching G while avoiding B. This op- timistic MDP is then used derive an optimistic policy that guides exploration by assuming the most favorable dy- namics permitted within the uncertainty bounds. In every episode & E N, we use a modified version of extended value iteration (EVI) to compute theoptimistic MDP M₁ E My and the optimistic policy गे. Alg. 2 illustrates our EVI al- gorithm. We initialize the vector Ao E [0, 1]|s] by assigning
Given an iMDP constructed
Let (0, 1) be given confidence parameter, ty be the time point at which th episode begins, and NN(ss, a) de- note the number of times the state-action pair (s, a) has been visited before the start of the h episode. Let T. and M₁ denote the empirical transition function and the set of statistically plausible MDPs, respectively, both computed using the observations before the start of the t.th episode. In
5

---

Regret-Free Reinforcement Learning for Temporal Logic Specifications
Algorithm 3 Computing optimistic MDP in Eq. (5)
denotes an integer, and Q (((SI-IG) is substochastic matrix defined over the set of states S \ G as follows:
where g >
(InnerMax)
Inputs: State-action pair (s, a). interval transition func- tion Tæ. and value vector iA
Compute (Gls, a) and d(ss, a) as the center and E radius of (- a), respectively
ss
4 B and s' E &S E
Qx(s, =
8 E B and 8' = Sinit
(8)
Sort the states according to their value in fr, and get S"
0
s E B and s' + Sinit-
{s} { t with (x(5() 2 (1s) 2 ... (s,)s)
if j= = 1 then
Note that we intentionally set the transition probability from B to Sinit to to account for the reset mechanism. Addi- tionally, since QR is substochastic, lim || = 0, ensuring that H₃ is finite for every episode & E N.
p(5)) as, a, 8/)) + a(s
else
)(5)) = (s, 83y
end if
As described in Alg. 1, the hthh episode terminates either upon reaching state in G when its duration reaches the deadline Hμ. During the episode, state-action pairs (st, at) along with the resulting transitions (st, Qe, St+1). These transitions are then used to construct the iMDP at the beginning of the next episode, as previously explained.
j f-11 n while E , ((())) > do
record the visited
p(())
max max Σ ExGES p($)))
j end while
Set (s, a, 25)) = =((])) ) for every 5 E S'. S'. Results: Tr(.ss.a) a) = InnerMax(s, a, Tk. F1)
Regret bound analysis: The following theorem states that Alg. 1 is regret free.
1 to states in G and 0 to all other states. At the tth iteration, we update the value vector μr by applying the following Bellman operator:
Theorem 4.2. With probability at least (1 - (0-20), Alg. has regret
(x()) CupAL11
[2][|Kox
R(K) (
8 8|A[Kax log
max max FF(s'ss A FETN
(5)
8
S'ES
6(Kax)²
+ 2 2Kax log
where the inner maximization is computed by running Alg. 3.
+ ax + (og(Kak))
We note that termination of Alg. 2 requires convergence L
2
of the value vector, i.e., ||ā 1l < min( 2t, P 1i where 1 E No denotes the iteration number of the EVI algorithm. This condition is guaranteed due to the contrac- tion property of the Bellman operator defined in Eq. (5) (see Sec. 3.3 in (Bertsekas, 2012)). Once EVI algorithm is terminated, setting Ük- = jr. follows that for every s S.
1 (
+ 2Kak log
(2(axx)
+ +2 + 2
2Kak log
(9)
(s) + min(
p (s),
(6)
where ax maxigRgK Hy.
2th
Remark 4.3. The quantity og grows at most logarithmically with respect to the number of episodes K (see Lem. 4.4).
where o" and ün denote the vectors containing probabilities of reaching G, when policies 7h and n²" are followed on MDPs M2 and M, respectively (see Thm. 7 in (Auer et al., 2008).).
Therefore, the regret bound in Eq. (9) grows sublinearly with respect to the number of episodes.
Executing the policy and collecting data: Once policy is computed, it will be executed throughout the episode for a specified duration, referred to as the deadline. After constructing M₁ and computing the corresponding policy 2 for episode k we determine the deadline HR, which is defined as
4.2. Proof Sketch for Thm. 4.2
Every episode starts at Sintt and ends by either (i) exceed- ing the deadline, corresponding to slow episodes, or (ii) by reaching one of the MECs in G, corresponding to fast episodes. It is important to note that every visit to states within MECs in B triggers an artificial reset action, which sets Sinit as the next immediate state.
H = min (n > 1 1 l S k }
6

---

Regret-Free Reinforcement Learning for Temporal Logic Specifications
To bound the total accumulated regret R(K), we define R(K) Σx=1 As, where AR = o" (simit) - vy (sinit). Our analysis partitions episodes into slow and fast, correspond- ing to episodic regrets A and 4.. respectively. Note that for fast episode, A and for slow episode, A 0.
end, we decompose the into two parts, Σ A and > k=1 k and show that both grow sublinearly in K. To bound =k=1 A&, we prove that (1) ox grows sublinearly with K (Lem. 4.4), and (2) Σ A grows sublinearly with K and linearly with the maximum episode length ox (Lem. 4.5). To complete the bound on Σ A/. we show that Ek=1 A also grows sublinearly (Lem. 4.6). Next, show that the sum over the slow episodes. Σi=1 Ai, is sublinear in K, since (1) the number of slow episodes grows only sublinearly with K (Lem. 4.7), and (2) each A S 1 by definition. Combining all these bounds, we conclude that the total regret satisfies R(K) OVVK).
f2
For the slow episodes, we use the obvious upper bound
A S 1.
For the fast episodes, since it is possible that ends in one of MECs in B before reaching G, we need to define reset transition which takes the states in B to Sinit- Therefore, every episode can be broken to T E N intervals such that the first 4 - 1 intervals start from Sinit and end at B, and the 1 interval starts from Sinit and ends G.
The following lemma provides an upper bound on the maxi- mum episode length, which grows logarithmically with the episode number.
We denote the 1th interval of the R4th episode during which the policy it. is applied by Pk,s, and define the correspond- ing value as
Lemma 4.4. With probability at least (1 -6/6), we have
αk S 3Alog(2VK)
(11)
{
if lass( E G if last(pp,)) B.
Uk (iitt)
(10)
where = |S|
log(6/6)
log(1 -p P Pmcc
We use the fact that v" (Sinit) 2n (Simit S [o Uk (Sinit) (since & 2 1) and define
Now, we proceed by showing why Ek= A grows sublin- early with K.
1 S (sSinit)) - ux (sinit)
Lemma 4.5. With probability at least (1- - 56/6), we have
2d (Sinit) (Siii)
/2|||Kax
A k S
4|5|
8 8) log
+ Uk.i (8iiiii (Sinit).
[((ax)²)
+ 2
2Kax log
5
To obtain an upper bound on Af we overapproximate the difference o² (Ninie) vx (Sinie) in every episode, since the exact values of v" (sinit) and Eg (Sintt) are not known. This is achieved by leveraging ideas from upper confidence bound algorithms, such UCRL2, and by relating un (Sinit) to the cumulative sum E i=l U,,n
1
2 ax + log(Kak)).
(12)
In order to prove the sublinear bound over Σk= A we make use of the Azuma-Hoeffüiee inequality (see Lem. B.2). The following lemma provides sublinear bound over the sum of A@
We define the decomposed regret terms
Lemma 4.6. With probubility at least (1 - 8/6), we have
fl
"" (Mimtt) - (iiiit)
1 8 2Kax log
F2
(13)
and
A F2
Uk (Sinie) - (Siii)))).
Note that knowing that oK grows logarithmically with K (Lem. 4.4), we have that Σx= A and Σ A and therefore ΣK A/ grow sublinearly with K.
The proof sketch for our regret analysis proceeds as follows. We first show that the sum Σk= Af. grows logarithmically with the number of episodes (Lems. 4.4 4.6). To this
The next lemma states bound over the accumulated regret associated with the slow episodes.
7

---

Regret-Free Reinforcement Learning for Temporal Logic Specifications
Lemma 4.7. With probability at least (1 - -),, we have
In App. A, we show polynomial algorithm for learning the underlying graph of the MDP M, i.e., x(M), using the knowledge of Pmin (see Alg. 5). Knowledge of x(M) directly gives the graph for the product MDP Mp, that is x(M₂) = (5%, AX, Bx), where ((8, q). a, (s', E EX if and only if
K
2 (2(Kax)²
A 3 2V
+ V2/ 2Kak log
8
[2]
+ | 8|A|Kax log
(14)
((s. a, (d' +
5. Regret-Free Learning for LTL
(s, 8') E E and of L
(15)
In this section, we study the policy synthesis problem for MDPs with an unknown transition function against LTL specifications.
Let D C S denote the set of states of a specific MEC C within Mg. We say C is accepting maximal end component (AMECs) within Mp if and only if
Problem 2. [Regret-Free Learning for General L.TL For- mulas] Given an MDP M with an unknown transition function, minimum transition probability Pmin E (0, 1), an LTL specification s,, and a confidence parameter 8 E (0, find an online learning algorithm such that with confidence at least (1 - 6) the resulting regret de- fined by Eq. (1) grows sublinearly with respect to the number of episodes K.
D UnUsxit 0, and D Dnl x=1
Us i=1
S x J. =0. (16)
We denote the set of all states corresponding to the accept- ing and non-accepting MECs within M, by Gx and B% respectively.
Alg. 4 outlines our proposed online regret-free algorithm for solving the policy synthesis problem against LTL specifica- tions. First, we compute a DRA 2 that accepts sp. We can run Alg. 5 and use Eq. (15) to get the underlying graph of M and Mp. respectively. Once we know the graph of Mp. we can use Algorithm 47 from (Baier & Katoen, 2008) to characterize all of the MECs M.. Next, we include the states within accepting and non-accepting MECs into Gx and 8% resepectively. Finally, we run Alg. I to maximize the probability of reaching G while avoiding Bx using confidence parameter 5/2, state set Sx action set AX, and initial state s The following theorem states that Alg. 4 is regret-free.
We transform the policy synthesis problem for general LTL specifications into a synthesis problem for an until (reach- avoid) formula, for which one can use the regret-free online algorithm proposed in Sec. 4.
Given an LTL formula ş. one can construct a deterministic Rabin automaton (DRA) whose language corresponds to all infinite sequences of system behaviors satisfying sp. This automaton, denoted by 2 = (Q, 7, Tinit; F), consists of a finite set of states Q, a finite alphabet Σ = 24P,
7,
transition function y: Q x Σ + Q, an initial state Ginit and an accepting condition F = {(J,, K,) ii= .....,m. consisting of subsets J; and K, of Q. An infinite sequence a accepted by A if there exists at least one pair (J F such that [ = 0 and inf(o) K # 9. where (n) is the set of states that appear infinitely often in a.
Theorem 5.1. With probability at least (1 -). Alg. has regret R(K) OVVK).
6. Discussion and Conclusions
For a given LTL specification and an MDP, the corre- sponding optimal policy, in general, belongs to the class of (deterministic) non-positional policies, that are map- pings from the finite paths over the MDP into the set of actions. One can restrict the set of policies to positional policies by constructing the corresponding product MDP, obtained as the product between the MDP M and the au- tomaton 2... Given an MDP M = (S,A,T sinit, L, AP) and a DRA 21p = (Q, X, Tinit, F), we denote the product
In this paper, we proposed a regret-free algorithm for the control policy synthesis problem over unknown MDPs against infinite-horizon L.T. specifications. The defined regret quantifies the accumulated deviation from the opti- mal probability of satisfying the LTL specification. We first propose a regret-free algorithm for until (reach-avoid) for- mulas, and then extend this approach to solve the synthesis problem for general LTL specifications by leveraging the knowledge of a minimum transition probability. This proba- bility is used to design efficient graph-learning algorithm with arbitrary precision.
MDP by the tuple M. = (SX A Txx xx LX, AP*),
where Sx = S x Q. A
A. s (Sinit: )init),
AP* AP. LX (s, q) + L(s) for every (s.g) E S.Sx SXQ.
and T : Sx
+ A(Sx) taking the form
A Acknowledgements
(*((g)), a, (s' ('))
[(s, a 8))
d'= (=g, otherwise.
This research is supported by the following grants: EIC 101070802, ERC 101089047, DFG project 389792660 and
0
8

---

Regret-Free Reinforcement Learning for Temporal Logic Specifications
Algorithm 4 Regret-free learning algorithm for general LTL specifications
for Undiscounted Reinforcement Learning, pp. 49-56. The MIT Press, September 2007.
Input: State and action sets S and A, initial state Sinit LTL specification s, confidence parameter 8 E (0,1), minimum transition probability pmin E 1)
Auer, P., Jaksch, T., and Ortner, R. Near-optimal regret bounds for reinforcement learning. Advances in neural information processing systems, 21, 2008.
Construct a DRA 21p = (Q, 2. Pnni: F) which accepts
Baier, C. and Katoen, J.-P. Principles of model checking. MIT press, 2008.
Run Alg. 5 get the connection graph x(M), i.e.,
x(M) = GraphLearn(S, A, Sinit; 8/2, (/nin)
Bertsekas, D. P. Dynamic Programming and Optimal Con- trol, Volume 2. Athena Scientific, Belmont, MA, 4th edition, 2012.
Compute the graph x(Mp) using Eq. (15) Compute MECs within Mp using Alg. 47 in (Baier & Katoen, 2008)
GO +-0 0
Bozkurt, A. K., Wang, Y., Zavlanos, M. M., and Pajic, M. Model-free reinforcement learning for stochastic games with linear temporal logic objectives. In 2021 IEEE Inter- national Conference on Robotics and Automation (ICRA), pp. 10649-10655. IEEE Press, 2021.
8x 4 0
for MEC C' inside M, with state space do Use Eq. (16) check if C is an AMEC
if C is AMEC then
G + G UD
else
Cai, M., Xiao, S., Li, B., Li, Z., and Kan, Z. Reinforce- ment learning based temporal logic control with maxi- mum probabilistic satisfaction. In 2021 IEEE Interna- tional Conference on Robotics and Automation (ICRA), pp. 806-812. IEEE Press, 2021.
Bx + B UD
end if
end for
Run Alg. 1 with state and action sets Sx and AX, initial state $iit sets Gx and Bx confidence parameter 6/2, and minimum transition probability Pmin. to compute and update the policy over Mp
Camacho, A., Iearte, R. T., Klassen, T. Q., Valenzano, R. A., and Mcllraith, S. A. LTL and beyond: Formal languages for reward function specification in reinforcement learn- ing. In International Joint Conference on Artificial Intel- ligence, 2019.
TRR 348-CPES
Dann, C., Lattimore, T., and Brunskill, E. Unifying PAC and regret: uniform PAC bounds for episodic reinforce- ment learning. In Proceedings of the 31st International Conference on Neural Information Processing Systems, NIPS' 17, pp. 5717-5727, Red Hook, NY, USA, 2017. Curran Associates Inc.
Impact Statement
This paper presents work whose goal is to advance the field of Machine Learning. Our work is mathemattiall/lggrittt- mic. While there may be many potential societal conse- quences of our work, we feel none of them must be specifi- cally highlighted here.
Fruit, R., Pirotta, M., and Lazaric, A. Near optimal exploration-exploitatio in non-communicating Markov decision processes. In Proceedings of the 32nd Inter- national Conference on Neural Information Processing Systems, NIPS' 18, pp. 2998 0088008, Red Hook, NY, USA, 2018. Curran Associates Inc.
References
Agarwal, A., Hsu, D., Kale, S., Langford, J., Li, L.,, and Schapire, R. Taming the monster: A fast and simple algorithm for contextual bandits. In Proceedings of the 31st International Conference on Machine Learning, vol- ume 32 of Proceedings of Machine Learning Research, pp. 1638-1646, Bejing, China, 22-24 Jun 2014. PMLR.
Fu, J. and Topeu, U. Probably approximately correct MDP learning and control with temporal logic constraints. In Robotics: Science and Systems X. University of Califor- nia, Berkeley, USA, July 12-16, 2014, 2014.
Alur, R., Bansal, S., Bastani, O., and Jothimurugan, K. A framework for transforming specifications in reinforce- ment learning. In Principles of Systems Design: Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday, pp. 604-624. Springer, 2022.
Hahn, M., Perez, M., Schewe, S., Somenzi, F., Trivedi, A.. and Wojtezak, D. Omega-regular objectives in model-free reinforcement learning. In Tools and Algorithmss for the Construction and Analysis of Systems: 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019,
Auer, and Ortner, R. Logarithmic Online Regret Bounds

---

Regret-Free Reinforcement Learning for Temporal Logic Specifications
Proceedings, Part pp. 395-412, Berlin, Heidelberg, 2019. Springer-Verlag.
Rosenberg, A., Cohen, A., Mansour, Y., and Kaplan, H. Near-optimal regret bounds for stochastic shortest path. In International Conference on Machine Learning, pp. 8210-88 8219. PMLR, 2020.
Hahn, E. M., Perez, M., Schewe, S., Somenzi, F., Trivedi, A., and Wojtczak, D. Good-for-MDPs automata for prob- abilistic analysis and reinforcement learning. In Interna- tional Conference on Tools and Algorithmss for the Con- struction and Analysis of Systems. pp. 306-323. Springer, 2020.
Sickert, S., Esparza, J., Jaax, S., and Křetúnský, J. Limit- deterministic büchi automata for linear temporal logic. In Computer Aided Verification, pp. 312-332, Cham, 2016. Springer International Publishing.
Hasanbeig, H., Kroening, D., and Abate, Certified rein- forcement learning with logic guidance. Artificial Intelli- gence, 322:103949 2023.
Srinivas, N., Krause, A., Kakade, S. M., and Seeger, M. W. Information-theoretio regret bounds for gaussian process optimization in the bandit setting. IEEE Transactions on Information T'heory 58(5):3250-322 2012.
Hasanbeig, M., Kantaros, Y., Abate, A., Kroening, D.,, Pap- pas, G. J., and Lee, I. Reinforcement learning for tempo- ral logic control synthesis with probabilistic satisfaction guarantees. In 2019 JEEE 58th Conference on Decision and Control (CDC), pp-
Tarbouriech, J., Garcelon, E., Valko, M., Pirotta, M., and Lazaric, A. No-regret exploration in goal-oriented rein- forcement learning. In Proceedings of the 37th Interna- tional Conference on Machine Learning, volume 1 119 of Proceedings of Machine Learning Research, pp. 9428- 9437. PMLR, 13-18 Jul 2020.
IEEE Press, 2019.
Icarte, T., Klassen, T. Q., Valenzano, R. A., and Mcllraith, S. A. Using reward machines for high-level task specifi- cation and decomposition in reinforcement learning. In International Conference Machine Learning, 2018.
Voloshin, C., Le, H. M., Chaudhuri, S., and Yue, Y. Policy optimization with linear temporal logic constraints. In Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurlPS 2022, New Orleans, LA, USA, November 28- December 9, 2022.
Kazemi, M., Perez, M., Somenzi, F., Soudjani, S., Trivedi, A., and Velasquez, A. Translating omega-regular speci- fications to average objectives for model-free reinforce- ment learning. In Proceedings of the l International Conference on Autonomous Agents and Multiagent Sys- tems, AAMAS 22, pp. 732-741, Richland, SC, 2022.
Yang, C.. Littman, M. L., and Carbin, M. On the (in)tractability of reinforcement learning for Itl objec- tives. In Proceedings of the Thirty- International Joint Conference on Artificial Intelligence, IJCAI-22, pp. 3650-3658. International Joint Conferences on Artificial Intelligence Organization, 2022.
Kazemi, M., Perez, M., Somenzi, F., Soudjani, S., Trivedi, A., and Velasquez, A. Average reward reinforcement learning for omega-regular and mean mean-payoff payoff objectives. arXiv preprint 2505: 2025.
Kearns, M. and Singh, S. Near-optimal reinforcement learn- ing in polynomial time. Machine Learning, 49:209-232, 2002.
Latouche, G. and Ramaswami, Introduction to Matrix Analytic Methods in Stochastic Modeling. Society for Industrial and Applied Mathematics, 1999.
Oura, R., Sakakibara, A., and Ushio, T. Reinforcement learning of control policy for linear temporal logic speci- fications using limit-deterministic generalized büchi au- tomata. IEEE Control Systems Letters, 4(3):761-766, July 2020. ISSN 2475-1456.
Perez, M.. Somenzi, F., and Trivedi, A. A PAC learning al- gorithm for LTL and omega-regular objectives in MDPs. In Proceedings of the Thirty-Eighth AAAI Conference Artificial Intelligence and Thirty-Sixth Conference on Innovative Applications of Artificial Intelligence and Fourteenth Symposium on Educational Advances in Arti- ficial Intelligence, AAAT24/AAAA244/AAA AAAI Press, 2024.
10

---

Regret-Free Reinforcement Learning for Temporal Logic Specifications
Algorithm 5 Graph learning algorithm (GraphLearn)
Input: State and action sets S and A, initial state Sinit, confidence 8 (0, 1), minimum transition probability Pmin E (0,1) 1, F 0, n((s, a) 0 for every (s,a) E S A, and N(s, a, 8') 0 for every (s, E Ax
Initialization:
Compute a lower bound for n²* using Eq. (17)
Set = S
log(5/6) m
Compute policies:
for E S Sinit do
Compute a policy x(*) under which is reachable from Sinit with positive probability: x(*) Rea A, 8, 6, Pmin)
end for for
(s. E 5 x A do of
(s)(s) f- a
Collect enough samples by executing the computed policies: while n(s,a) a) < n² do
St Sinit
for 1 S < L do
Execute the action ar πt (st) and observe the next state $1+1
n(st, 0z) + n(s), +1
(8t, 0r, 8141) + (8t, Ce, 8141)
f - ++1
8; = s then break end if end for end while Verify existence of transitions: for s' E 5 do
if N a, s') > 0 then
E E as))
end if end for end for
Results: x(M) = GraphLearn(S, A, Sinit, 8, Pmisn)
A. Graph Identification
In this section, show how to leverage the knowledge of the minimum transition probability Puni (0, of given MDP M to identify its underlying graph with desired level of confidence. The following lemma provides a bound on the minimum number of samples required to verify the existence of a specific transition in M.
Lemma A.1. (Voloshin al., 2022) For any transition (s, a, E S S let F (s')s, a) denote the empirical estimation of transition rrobability-ssociatted associated with the actual transition probability T's' [ss'|s,, a)-after observing (s, for times. Given positive lower bound over the minimum transition probability Pmii (0, 1) and confidence parameter E (0. 1),
we have (s, a,,5 s & E with confidence at least (1 - 8/2) if F.,. (8'18, a) 0, for
n" > x (pmin),
(17)
where ((n) = V3((m) I((n), and ((n) - log ( if 1.
Alg. 5 outlines our proposed algorithm to learn the graph for given MDP. We leverage Pmin and å to compute the minimum number of required samples n² using Eq. (17), and a horizon L E N, after which the execution of episodes is stopped. The process consists of two main steps: (1) for every state s E S, we apply Alg. 6, that is inspired by the wPPAC algorithm (Perez et al., 2024), to obtain policy z(+), under which is reachable from Sinit with positive probability; (2) for each action a E A, we execute (+) until the pair (s, a) has been visited at least n² many times. Upon reaching (s, a), we collect

---

Regret-Free Reinforcement Learning for Temporal Logic Specifications
Algorithm 6 Reachability policy synthesis for graph learning (Reach)
Inputs: State and action sets and A, target state probability Punin E (0,1)
(Sinit). confidence parameter å (0, 1). minimum transition
n(s, a) <- 0 for every (s,a) E ES A
(s, s², +- 0 for every (s, a, 8¹) E S x A
Compute C33 and H using Eq. (20)
G {
while True do
for (s,a) E S x A do
if i a) then
=
Otherwise
G+ GU{s}
else
(ssass T(s,a,8) = (((aa)
end if end for
M = (S, A, f, Sinie: i., AP), with AP {Goal), and i(s*)= { Goal] } and f.(s) if + 8* Compute optimal policy ((6)) for M by solving the corresponding linear program (see Sec. 10.6.1 in (Baier & Katoen, 2008))
For M, compute SH S S as the set of states that are reachable from Sinit within 2HH time steps if ns, a) 2 C3 for every (s, a) E SH x A then
break
end if
81 f- Sinit
for 1 S S 2H do
Execute the action 04 x1101 and observe the next state 8141
n(5t, az) + n(s;,
N N(s ae, S141) + N(s,, 04. s141) +
end for end while
Results: x(=")_ Reach((,, A, 8", 5,, P.min)
the resulting outgoing transitions by simulating the MDP. Since the initial state of the MDP is fixed at Sinit * s, we use (()) to reach s, enabling us to observe the outgoing transitions from (s, a). Additionally, the horizon L is used to prevent unlimited exploration if the sample trajectory is trapped in one of the MBCS containing Once niss, a) n², verify whether the transition (s, s') belongs to E, by checking if N [(s, a, s') 0 for every s' E S.
Sample complexity analysis. To provide a sample complexity for Alg. 5, we need to (1) provide bound over the minimum number of samples required by the method used for finding (*) to enable providing a bound over the minimum number of required samples, and (2) calculate the horizon such that it offers a formal bound on the length of trajectories before getting stuck an MEC. For (1), we must use undiscounted RL formulations such as E (Kearns Singh, 2002) and trade-off. For (2), given a certain confidence level, we can derive upper bound on the number of steps after which, with high confidence, one of the MECs is reached and every state within that particular MEC is explored. The following theorem quantifies the sample complexity of Alg. 5.
w-PAC (Perez et al., 2024), which explicitly handle the
Theorem A.2. Let the horizon for an MDP M be defined as the smallest time t E N such that with probability at least (1 - (1-8/6) trajectory of length starting from the initial state Sinit visits every state in some MEC within M. Also, let C denote the minimum number of time steps after which the graph learned by Alg. 5 correct with confidence at least (1 6). We have
12

---

Regret-Free Reinforcement Learning for Temporal Logic Specifications
L S [S] log(6/6) and
(18)
log(1 -mmma)
C $ |S|C| + |
(19)
where
18C3|S|1A| 162(Ca|S[|A) log(6/12))
C1 = H max
and
SI Pmin
Pmin
C₂ = min
t N|
(1' (1*)
( 22min
n (
P 1s
Pman
t-n
2
with
-9log(6/12/5 -910g(//2//$1144
and H = -1| log(p 1S|
min! /18)
C3
(20)
Pmm
|8|
log(1 p pmmn)
Proof. Using the same reasoning in the proof of Lem. B.1, we have L S |S| log(6/6)
log(1 (1p(1_) where the confidence level is set to (1 (1-d) (1-6/6. Regarding the sample complexity for computing policies (( for every E S, we note that either G is not reachable, the minimum reachability probability is pl9l Thus, ensure that s is reachable with positive probability, the p
computed policy must be e-optimal with < pusin By setting the confidence to (1 (1-6 5/66) and the precision to E = 18 we can directly apply the sample complexity result from w-PAC (Perez et al., 2024) to obtain C1 (see Thm. in (Perez et al.,
2024)). This ensures that the resulting policy achieves a positive reachability probability (greater than pmstn /2) after C₁ time steps. Since we need to compute reachability policies for every state & E S, this takes | time steps.
Next, C2 gives the minimum number of trials after which the probability of visiting a specific state s at least n² ttimes is at least (1 5/6). For every state-action pair (s, [S] A), we must run episodes length L, which requires |S]|A|CC2 time steps.
Since the confidence for computing L, C1, and C2 is (1 8/6), and for n" it is (1 8/2), the overall confidence becomes (). Therefore, the total number of samples required to achieve an overall confidence of (1-8) is |S]C2+|8]|A]444
B. Proofs
B.1. Proof of Lem. 4.1
We adopt notation similar to that used in the proof of Lem. 3 in (Tarbouriech al., 2020) to improve clarity. We want to bound the probability of the event gº U (M & M&)- Let (, a) be the -bll centered at T (-1s, a) with radius 3& (s(s, a), where (s,a) is visited least times before episode k. Then, E C U(..a) U [T( s, a) & (s, Using Boole's inequality, we get P(EC)= < E(s,a) o P(T(-ss,)) a) & a)).
For n 2 0, define e.. (x, == V n (z=))))
2)/8), where n == max(n, 1). Following (Tarbouriech al., 2020) and Weissman's ''s inequality, we have 6, (s, (n(s, a) almost surely, and for 2 1: P(T(-Is,,) B, (s, a)) < (/(5))]|A[n))) and equals zero for n = 0.
Thus, P(E9)= < E(s,a) Ex iilli|aa
x² 5 8/3. This concludes the proof.
B.2. Proof of Lem. 4.4
In order to prove Lem. 4.4, we need to first ensure the existence of (high-probabilitt)) bound on the number of steps required to reach G from states in 5 \ B, when we enable reset. Note that the set B also includes every MEC whose intersection with is empty. In App. A, we discuss details of an algorithm for learning the MDP graph x(M up to any desired confidence, using the knowledge of the minimum transition probability Pmin- Given x(M), we can efficiently
13

---

Regret-Free Reinforcement Learning for Temporal Logic Specifications
identify all MECs within M that do not intersect with G and include them in B. The following lemma provides an upper bound for the time required to reach G from any state in S \ B, when a reset transition is enabled upon visiting states in B. Lemma B.1. Let (s) denote the time to reach G from state in an (artificial) MDP M obtained by connecting B to Sinit with probability in MR. Then, with confidence at least (1 8/6), we have for every S X, B that
log (ōg66/6)
(s(s) S = |S
(21)
log( Pmin
Proof. First, note that by including every state from which G is unreachable into B, is guaranteed that policy (s)))) takes every 8 E 5 B to G. with probability at least Pinen This is ensured by Eq. (6), since v*(s) 2 P P for every s E S B. Now, enabling the reset transition from B to Sinit with probability 1, under Tg. G becomes reachable from every state s E S with probability 1. the worst-case scenario, every state in the corresponding Markov chain must be visited at least once. Visiting every state requires following path of length at most |S), which occurs with probability Pminn After I then 10
attempts of traversing this path, the probability of success at least once is given by (1 - p ) If log(1-
(o/()/6)
1 - (1- --mii y 21 - 6/6. Finally, since each of the 7 attempts takes |S| steps in the worst case, the total number of steps is bounded by |S| [ |S|
log(5/6)
Furthermore, since M,g is chosen optimistically, the time to reach G in Mr. is no p
greater than that in the true MDP M. Therefore, with probability at least (1 5/6), we have that (s S A.
Now, we are ready to prove Lem. 4.4, First, using the Markov's inequality (since x + x" is a non-decreasing mapping for non-negative reals), we have
(()x(() 2 H - 1) < E| [))
(H 1)"
Now, we note that by Lem. 15 in (Tarbouriech et al., 2020), we have if (s) I X for every s E EE and X 2 2, then
B()x(s))) - 2(rA)",
for any r 2 Therefore, substituting À with A (defined in Eq. (21)), we will have
P(Ac(8) 2 H 1) 2(rA) Note that there exists E 5 such that
(22)
(H₃ 1)"
I1 - =1 H4 2) P()x(v) H 22).
(23)
By definition of Hy have ||0Ha-21l 1/VT.. Combining this with Eqs. (22), (23) yields
2(rA)" HH - 1)" > 1/Vk,
which implics that
H <
By selecting = [log(2/R)] we get
H 1< (L)(((2)))) Beaeavt <
3A loggoo((/)))
Hence
ak < 3A log((22V))
Since (s(s) < A holds with confidence at least (1 - 5/6). the overall confidence is also maintained at a level at least - 8/6).
14

---

Regret-Free Reinforcement Learning for Temporal Logic Specifications
B.3. Proof of Lem. 4.5
In order to prove Lem, 4.5, we make use of the Azuma-Hoefiding inequality, which is stated below for the sake of completeness.
Lemma B.2 (Azuma-Hoefrding
Hoeffding inequality, Hoeffding 1963). Let X2....... be a martingale difference sequence with [Xi] S e for all I. Then for all y > 0 and n E N,
P
x1 S exp(
2nc )
Now, we are ready to prove Lem. 4.5. We proceed by showing why Σk=1 A grows sublinearly with K. In order to reformulate the regret, we define the following reward function r: - {0, 1}
0
s $
r(s)
(24)
1 G.
Further, for the time step h within episode we define
Ha,z, (8)-1
(K,A == 0z (sk.))
Σ r(sk,t
where Ia: [1; Hu] + [4] maps the time points in episode into the corresponding interval, and H& denotes the length of the 8th interval within the ktth episode for s S I and H = 1. Therefore, we have
+ H (Sk,
Let us further define
K = (s(Sk,441)
Epl sk,hv Hu (skN)))))(())) DES
(25)
where -(-l..)) corresponds to the transition probability in the true MDP M. Similarly, we denote by P& (.)...) for the transition probability in the optimistic MDP Mr. Note that for 8k.h GU B. have (s,,(5 O. For 8k,6 GUG.R B, we have
Σ
r(she) S (e0u((8,h)) +
Σ
r(sk,)
Σ poly Sk,hs TN (sk.N))) EN r(sk.h)
Σ
r(su.)
VES
Σ (p skin Tx(, - ply ski tu (xx,N)))
yES
Ha
Σ ply Sk. (ALA))((S + +
Σ
r(sp.))
BES
+=
< (3 (sk,N))
1+ E
p(y
skkh Tn ((( oy (sk,N+1))
yES
Ha
+ + (ix ($n.Nttt11
Σ r(sk,))
hh+1
#s((),))) (3.(sn... Pu.b
Ek Ox. (
15

---

Regret-Free Reinforcement Learning for Temporal Logic Specifications
where the first inequality follows from the termination condition of Alg. 2, the fact that r(sg,t) 0 for every shtt & GUUD B for the second equality, (x(y) for every y E S for the third equality, definition of 3r (Eq. (4)) for the second inequality, and definition of &R (Bq. (25)) for the last inequality. Also, note that By telescopic sum we get
Ha,
He, (Sk, He,,
(ON,A(SE,n) (Sk.41)) O -e. (S6,
H1,4112
( + PA.A + + O
11,
Σ
23x ( (x(,))))) +
Σ
DEA + H4,
where used the arguments made in the previous step of the proof establish the first inequality, the fact that θk, Hk,Ha, ( (sk, 0 by definition as 5k.12.442-1 E G U B for every S i S la for the last inequality, By summing over all of the episodes we have
K
HR. (Sk,He,.)
H
K
1
Hap-1
LEA
Σ
+
Hysk
(26)
1=
k=
k=1
In order to bound the first term, we note that
K
H
K fu+1 -1
PKA
Pk.h-
h=
k=1
Therefore, we can write
K t+41
K Ha) log
2 2 H2)2
IP
Pk 2 2
2(
8
k=tt
k=1
1441-1
2n
P
Φ 2
2 2n 2n log
H
Let Gg denote the history of all random events up to (and including) step h of episode ks i.c., q have (E( Gy) 0, and furthermore Ha is selected at the beginning of episode k, and it is adapted with respect to Gy. Hence &R, is a martingale difference with | < 1. Therefore, by Azuma- huuma-Hoeffding's inequality, we have with probability
=
k--1 Σ Hy h. We
6 Ha
Σ
PR. 2
2
Σ
H
log
k=1
Now, we proceed to bound the second term in Eq. (26). We can write
H
ΣΣ A=1
1
ΣΣΣ
<
2//SI
Σ
(*,
22//1//A
Ne (SK,N (x(s))))
k=1
Therefore, obtain
K H
22/A|t
Ba(Sk. #a(sk.)) s 2|15|
8) A|Att log
8
A=
Aml
16

---

Regret-Free Reinforcement Learning for Temporal Logic Specifications
Finally, we bound the last term in Eq. (26).
K
Tx.1
OK
Ha
S
1
[1+log([k)) (1+oo((aa)),
2
2
where ÆgK = maxisksk Hg. Putting everything together yields that incquality (12) holds with probability at least 1-55 55/6.
B.4. Proof of Lem. 4.6
We define XR, == uk (Sinit) (n,ii(iintt) Note that (xx)) = 0 and Xx,il I 1 for every 1 5 k S K and 1 S S 4x. We have
It
Ix
A
F2
2k (Sinit) (Sinie))
Xk.i-
Therefore by application of the Azuma-Hoeflding lemma and using the fact that Kay 2 >E La we get
K
2k log( (
- log (log(()) (g) 8/6.
Σ
A f2 2
V
22Ka log 5)
S exp
S exp
>Σ Ix
In Lem. 4.4, we have already shown that ok grows logarithmically with K which proves that Σ A grows sublinearly with K with confidence at least (1 8/6).
B.5. Proof of Lem. 4.7
Let Fx Ek =k=1 Ai and d and dS denote the hitting times of policy 7e in the true and optimistic models, respectively, We define
(sR()) = 1M ((A((().)))
Hs h).
Note that we have
K FK Σ 12 (sk1)) Σ P(Aa > H2 -1).
K
Let -1.-- denote the transition probability in the optimistic model My (that is the optimistic MDP constructed from Mr by connecting states in B into s.it). Similarly, let ('(...) denote the transition probability in the MDP M (that the MDP constructed from M, by connecting states in B into Sinit). Since for 1 S I H3 1, (e(e = (1) we have
(5R = H -
Σ Py(y sk, ( > HP - -h
yES
( Σ
Pl sk. sk, (x(sk))) - p' sk. F2(SKN)) > H h 1)
DES
-E'(v E' P H: - 1-1
yES
1Mllsn)))) 2 (sk.h)) Σ E'y SkM (((eN)) > H4 - h
DES
- + thR. + 2, R (sk,)))))
where we established the first inequality by adding and subtracting the term p' 88,6 Tx (Ax Hs the second inequality by using the definition of B4 (Eq. (3)), and the last equality by using the following definition
1),
VkS ((A((s).)11)) > Ha - h 11-1) 1) - Σ p'(y (yl Sk. (x(s > Hr - h 1).
VES
17

---

Regret-Free Reinforcement Learning for Temporal Logic Specifications
Also, we have
1 16 10 RG 0. Ta, (s), = (e(e,,,, )=0 (P > 0)) (e(e,,,g))0 Mu(s,, 20)
Using the telescopic sum get
He-1
Hy-1
He (a #x (SK,)))
(8,,()
Σ
(TK,ASK,,)) (RAAI + I (sk, S
Σ
1h, + +
A=1
h=1
h=1
where the last inequality is achieved by knowing BR (SK,H.) = 0. Therefore, by summing over all episodes we get
H
K H
K
FK
URA +
Σ
+ Σ (SAiit)) > Hs - 1).
Let Gg denote the history of all random events up (and including) step h of episode k. i.e., q= = = Hs + h. We have E(bx, Go) O, and furthermore H& is selected at the beginning of episode k, and so it is adapted with respect to g Hence & is martingale difference with | S 1. Therefore, using similar arguments as in proof of Lem. 4.5, by Azuma-Hoeffdiing' inequality, we have with probability 26
k-
K
H
k
3 k- H₂)a
3(Kax)
VR
S
2
2
Σ
H
log
< 221/ 2Kax log
1=1
A=1
Further, in the same vein proof of Lem. 4.5 we have
K H
2 2aK
Be(sk,h. (b(sk)))) s 2|51 K| log
8
Rm
1 h=1
Now, we need bound Σ ((iit)))t) H: 1). Using Thm. 2.5.3 in (Latouche Ramaswami, 1999), we have
((Aa(6int)) H2 1) Σ
O
where 1, denotes the |S| 1-sized one-hot vector at the position of state E S. Finally, from Holder's inequality, we have
K
P (Aaainnn > Hx 1)
1 Shi
2
H
km
1m
1 smx 11111//1--111 11100
Σ
110
11loc-
k=1
Therefore, by the choice of H₂ min
11 S vx.
11 we get
1
((Aa(sintt) H 1) <
22
k=1
Putting everything together yields that inequality (14) holds with probability at least 1 - 6.
B.6. Proof of Thm. 4.2
Let yU.)), y(122), and y)t) denote the events under which Eqs. (12), (13), and (14) hold, respectively. By Lems. 4.5 and 4.6, we have (P())()1)) n ((t22)) 2 - 56/6 6/6 1 - 8. Moreover, from Lem. 4.7, we know that IP())(=)) > - 8.
Now, let D,, denote the event under which inequality (9) holds. Since y(uI) n po(:2) n yoss) C D,. follows that P()))) 8 ==1 28.
18

---

Regret-Free Reinforcement Learning for Temporal Logic Specifications
G
Sinit
Figure 2: Map of the gridworld example with 1 6. The blue and green cells define the initial state (Sinit) and target state (G), respectively. The red cells correspond walls. The objective of the agent is reach G without hitting the walls.
1.0
0.8
Normalized regret
0.1
0.2
0.0
2000
4000
6000
8000
10000
Spisode number
Figure 3: Variations of the empirical normalized regret, R(K)/K, when our proposed algorithm is applied to the gridworld example with / = 6.
B.7. Proof of Thm. 5.1
Let V/ and Vr denote the events, under which the learned graph is correct, and the bound over the regret given by
Eq. (9) holds (after substituting S,A, with Sx A* ,*, respectively). From the results of Thms. 4.2 and A.2, we have P(V))) P(),) 2 1 5/2. Then,
POGN),) = P(), U. 2 6/2- - 6/2 = 1
C. Experimental Evaluation
In this section, we evaluate an implementation our algorithm. The experiments are performed on a laptop with core i7 CPU at 10HG,H with 8GB of RAM. We implement Alg. 1 obtain the results, assuming that the underlying graph structure is known. This assumption is justified by the fact that, for fixed system dynamics, Alg. 5 needs to be executed only once to learn the corresponding graph with the desired confidence. The resulting graph can then be reused for verifying any L.TI. specification.
We considered a reach-avoid policy synthesis problem in the gridworld example described in Fig. The world characterized by E N>1 that denotes the number of cells per column and row. The agent can move using the cardinal directions, i.e., A right, left, up, down }. Movement along an intended direction succeeds with probability 0.9 and fails
19

---

Regret-Free Reinforcement Learning for Temporal Logic Specifications
1.9
ZeroRoy FAC
0.3
Normaliee tegrel.
0.2
0.9
10000
15000
25000
Episode number
Figure 4: Comparison of the empirical normalized regret between our proposed regret-free algorithm and the w-PAC algorithm (Perez et al., 2024) for the gridworld example with =
with probability 0.1. In case of failure, the agent does not move. Walls are considered to absorbing. i.e., the agent will be able to move after hitting wall. We have conducted experiments (I) evaluate the empirical performance of our algorithem, (2) observe how episode length vary throughout the run of our algorithm, and (3) assess the sample complexity of our method.
Empirical performance: Fig. 3 illustrates the variations of empirical mean for the normalized regret R(K)/K for our regret-free algorithm which is run for the gridworld example with / = 6. We set 6 = 0.1 over 10 runs Furthermore, we group all of the cells associated with the wall into an absorbing state B, such that we have |S| = 17 and |A| = 4. The considered specification y = Avoid U Goal, where is marked as Goal and walls are marked as Avoid. It can be observed that the empirical mean of the regret drops very quickly, which implies that the algorithm successfully finds an optimal policy within the few first episodes.
We also compare the performance of our proposed method with the w-PAC algorithm of (Perez et al., 2024), which is the only existing method that supports guaranteed policy synthesis against infinite-horizon temporal specifications. The w-PAC algorithm takes confidence parameter ó E (0, 1) and a precision parameter e E (0, 1) and provides a policy which has e-optimal satisfaction probability with confidence (1 - 8). Fig. 4 illustrates that our proposed algorithm converges much faster. We believe that this because our algorithm uses the intermediate confidence bounds, while the w-PAC algorithm waits until enough many samples are collected, and only then updates its policy.
Episode length variations: Fig. 5 illustrates the variations in H3 for different episodes. Initially, algorithm assigns very small values to H3, since the expected time to reach G in the optimistic MDP is small. As the empirical transition probabilities become more precise, the estimation over the expected time to reach G takes more accurate values.
Sample complexity: Although our method and w-PAC algorithm provide different guarantees, we relate them through definition of a related complexity metric. The sample complexity of the w-PAC algorithm characterized with that the number of learning episodes with non-s-optimal satisfaction probability. We define k;,g(8,
(8, =) as the smallest number of episodes & for which regret- free algorithm satisfies It(k) < with confidence (1 (-5), Furthermore, define (6, e) as the minimum number of episodes after which the w-PAC algorithm satisfies Cs < E with confidence (1 - 6). Fig. illustrates the variations of ki (0.1, 0.1) and A 10. 0.1) for gridworld example with 4 < S 16. Note that changes in I influences the size of the state space (IS) (I 2) + 1) and also the (minimum) E-recurrence time T, (2 2) 1, which is required by the w-PAC algorithm. Furthermore, set Pmin 0.01. It can be observed that our algorithm provides tighter bound specially for the larger examples.
&
20

---

Regret-Free Reinforcement Learning for Temporal Logic Specifications
2-
2000
40000
6000
80OC
10000
Episode number
Figure 5: Variations of the computed deadline, Hg, when proposed algorithm is applied to the gridworld example with
1 1= 6.
1e11
ZareReg
w PAC
Requiced punulees sampless
3.3
2.3
1.9
0.3
0.0
100
150
Figure 6: Comparison of the theoretical sample complexities for proposed algorithm and the w-PAC algorithm (Perez et al., 2024) for the gridworld example with various sizes (4 < I < 16).
21


Reviews:
[{"review_id": "QvUF4vZ0qa", "reviewer": "Reviewer_ZtQ1", "summary": "This paper proposes a regret-free online RL algorithm for learning policies that satisfy infinite-horizon LTL specifications in unknown MDPs. The core contribution is an algorithm that, for reach-avoid specifications (a subclass of LTL), builds a sequence of optimistic policies using *interval* MDPs and extended value iteration, ensuring that the average regret—defined as the difference in satisfaction probabilities between the learned and optimal policies—converges to zero. The authors then extend this to general LTL specifications by transforming the original problem into a reach-avoid problem over a product MDP composed with a deterministic Rabin automaton, using an auxiliary algorithm to learn the graph structure of the unknown MDP given a known lower bound on transition probabilities. They provide theoretical regret bounds and claim sublinear regret in the number of episodes, supported by a regret decomposition analysis. Experimental results in the appendix in a gridworld domain are presented to suggest improved sample efficiency over a prior PAC-MDP approach.", "questions": "", "limitations": "", "rating": 2, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank you for the detailed and useful feedback! We plan to improve our paper taking your comments into account. Our response to your specific questions are summarized as follows.\n \n**Assumptions used in the paper:**\nWe do not assume the SSP-communicating property for MDPs. Instead, we **only** make a weaker assumption of knowing a non-zero lower bound over minimum transition probability $p_{min}$, which enables application of our method to the general non-communicating MDPs​. To relax the communicating assumption in Tarbouriech et al. (2020), we leverage $p_{min}$​ to compute $\\Lambda(s)$, which represents an upper bound on the minimum expected time required to reach $G$ from state $s$ in the (artificial) MDP $\\mathcal{M}'$, constructed by connecting $B$ to $𝑠_{𝑖𝑛𝑖𝑡}​$. Note that $p_{min}$ can be used to compute the underlying graph to any desired accuracy, enabling us to check whether $G$ is reachable (which implies the boundedness of $\\Lambda(s)$). These details are discussed in Lemma 4.2 and Remark 4.3. In particular, our results require **no** assumption other than knowing $p_{min}$. Also, it should be noted that assuming knowledge of $p_{min}$ is strictly weaker than the assumption of SSP-communication.\n\n\n**Presentation of Algorithm 1:**\nRegarding referencing other algorithms and equations, we would like to highlight that Section 4.1 is specifically dedicated to explaining various components of the main algorithm (Algorithm 1). In particular, the following components of Algorithm 1 are discussed in detail: (1) the application of Equation (4) for “computing confidence intervals”, which are then used to construct interval MDPs from the observed data; (2) the operation of our proposed “Extended Value Iteration” method (Algorithm 2); and (3) the use of Equation (9) to compute “episode-specific deadlines”. These explanations are provided in the respective subsections of Section 4.1. That said, we appreciate the reviewer’s comment and will, in the final version of the paper, provide additional intuitive explanations of our Extended Value Iteration (Algorithm 2), include a brief description of Algorithm 3, and define the notation \\#{.}, which denotes set cardinality.\n \n\n**Clarity of Lemma 4.1:**\nIn Lemma 4.1, the event $\\mathcal{E}$ refers to the scenario where the actual MDP lies within the interval MDP computed during the $k^{th}$ episode of learning. The notation $\\mathbb{P}(\\mathcal{E})$ represents the probability that this event occurs. The notation $Pr_{s_{init}}^{\\pi}[\\varphi]$ is explicitly defined in Section 3 under the heading “Maximum Probability of Satisfaction”, and refers to the probability of satisfying a given LTL specification $\\varphi$, starting from the initial state $s_{init}$ and following policy $\\pi$. In the camera-ready version of our paper, we will ensure that the notation $\\mathbb{P}(.)$ is clearly explained, replace instances of $Pr[.]$ by $\\mathbb{P}(.)$, and we will explicitly reference the relevant lemma adapted from (Tarbouriech et al., 2020, Lemma 3). \n \n\n**Comment on missing explanation for Equation (4):**\nEquation (4) is used for computing confidence intervals necessary for constructing interval MDPs, and it is derived in earlier work (see Lemma 1). Specifically, the derivation relies on well-known probabilistic inequalities, and $ max(1, N_k(s,a))$ serves to prevent division by zero, where $N_k(s,a)$ represents the number of visits to the state-action pair $(s, a)$. In the final version, we will include Equation (4) within the body of Lemma 4.1 and provide a brief explanation of the terms in Equation (4). \n \n **Proposed changes based on comments of reviewer 1:**\n- Provide additional intuitive explanation of our EVI (Algorithm 2), and give a brief explanation of Algorithm 3\n- Integrate Equation (4) into Lemma 4.1, and provide a brief explanation of the terms within Equation (4)\n- Explain the notation $\\mathbb{P}(.)$ under the notations section\n- Define the notation \\#{.}\n- Provide citations for the definition of MDPs and interval MDPs (IMDPs), maximal end components (MECs), extended value iteration (EVI), and refer to the specific lemma from (Tarbouriech et al., 2020) for Lemma 4.1\n- Define optimistic MDPs", "claims_and_evidence": "While the paper presents a complete pipeline and claims theoretical guarantees, the mathematical formulation and algorithmic descriptions are occasionally imprecise, and the overall presentation order may obscure key assumptions or derivations. Hence, the writing and proofs provided in support of the claims are not clear and convincing.", "methods_and_evaluation_criteria": "Yes.", "theoretical_claims": "- Lemma 4.1. (Tarbouriech et al., 2020) is unclear since:\n  - It is unclear what is the specific Lemma/Theorem from Tarbouriech et al. (2020) that is being restated here.\n  -  $\\mathbb{P}(\\mathcal{E})$ is undefined (note that the authors generally use the notation $Pr$ to refer to probability distributions).\n\n-  The proofs of most of the Lemmas and Theorems use the results of Tarbouriech et al. (2020), but that means the authors must assume that the MDPs are SSP-communicating. However, this assumption is not stated in the paper (neither in *Problem 1* nor *Problem 2* statements). It is unclear what other specific assumptions are made but not stated.", "experimental_designs_or_analyses": "N/A", "relation_to_broader_scientific_literature": "The paper builds on prior work in reinforcement learning with temporal logic specifications, particularly extending ideas from PAC-MDP and UCRL2 frameworks by aiming for regret bounds rather than asymptotic guarantees. It distinguishes itself from earlier approaches by handling non-communicating MDPs and providing better finite-time performance guarantees (regret of $O(K^{1/2})$) than the closest related prior work (regret of $O(K^{3/2})$).", "essential_references_not_discussed": "The paper extensively covers related works.", "other_strengths_and_weaknesses": "The paper provides a comprehensive number of algorithms and theoretical results. However, it is extremely unclear in its writing making it hard to follow and evaluate its correctness.\n\n- The algorithms are not clearly explained. For example, at the start of Section 4.1 the authors mention \"Alg. 1 shows our learning algorithm.\". But Alg. 1 cannot be understood at that point since it references Alg. 2, Eq. 4, and Eq. 9 which only appear later (where Alg. 2 and Eq. 4 are also not clearly explained). Additionally, it is unclear what the notation #$\\\\{t < t_k : s_t = s, a_t = a\\\\}$ means (same for  #$\\\\{t < t_k : s_t = s, a_t = a, s_{t+1}=s'\\\\}$). Is it a set of only one Boolean value (the result of $t < t_k$)? \n\n-  Alg. 2 and  Alg. 3 are not clearly explained. In fact,  Alg. 2 uses  Alg. 3, but  Alg. 3 is not even referenced in the text. It would have helped if the authors clearly explained their extended value iteration, and how exactly they obtain a policy that maximizes the probability of reaching G. \n\nFinally, this makes even the main algorithm (Alg. 4) unclear since it uses Alg. 1, and makes the correctness of the corresponding main theorem (Theorem 5.1) hard to evaluate. Hence, while I think the problem this paper attempts to solve is very relevant, and the paper offers numerous interesting algorithms and theoretical results, its presentation is currently too unclear.\n\n# Post Rebuttal\n\nThe authors rebuttal did help a bit clarify the assumptions they make in this paper, their definition of $\\mathbb{P}(.)$ (how it differs from $Pr$), where Lemma 4.1 comes from, and the explanation for Equation (4). Unfortunately, I still have reservations regarding the clarity of the paper (listed below). However, I can see that the other reviewers feel positive about the paper, so it is possible that I missed something.\n\n- It is still unclear how the authors can simply use Lemma 3 from Tarbouriech et al. (2020) if the authors are not assuming SSP-communicating MDPs. Perhaps I am misunderstanding the assumptions of that Lemma. Additionally, it is unclear how that Lemma is the same as Lemma 4.1 when:\n\n    - $\\mathcal{E}$ from Lemma 4.1 is defined differently from $\\mathcal{E}$ in Tarbouriech et al. Lemma 3. If one follows from the other, no explanation is given on how.\n    - For a given $\\delta \\in(0,1)$, the bound from Tarbouriech et al. Lemma 3 is $\\mathbb{P}(\\mathcal{E})\\geq1-\\frac{\\delta}{3}$ but the one in Lemma 4.1 is $\\mathbb{P}(\\mathcal{E})\\geq 1-\\delta$.\n\n- If the authors are not assuming SSP-communicating MDPs or the existence of a proper policy, then it seems like $\\Lambda(s)$ and $\\lambda^*(s)$ can be unbounded for some $s$, invalidating Lemma 4.2. For example, Consider a simple MDP with a state set $S = \\set{s_{\\text{init}}, s_1,s_2, G}$ and a singleton action set $A=\\\\{a\\\\}$. The transition probabilities are $T(s_{\\text{init}}, a, G) = p_{min}$, $T(s_{\\text{init}}, a, s_1) = 1-p_{min}$, $T(s_1, a, s_2) = 1-p_{min}$, and $T(s_2, a, s_1) = p_{min}$. Then $\\Lambda(s)$ and $\\lambda^*(s)$ are unbounded.\n\n- The authors still did not clarify the notation #{.} in their rebuttal (they did not even confirm or denied the interpretation I gave), and in general they did not clarify my concerns with Algorithm 1. As I already highlighted in my review, I didn't find the presentation of Algorithm 1 nor the explanations given Section 4.1 entirely clear. Hence it did not help when they simply referred me back to Section 4.1 without an attempt to clarify at least some of those concerns (e.g. regarding how their EVI is able to find a policy that maximizes the probability of reaching G).\n\nIn general, I think the paper makes sense at a high level, and the specific algorithms are very interesting and do look like they work. However, given the focus of this paper theoretical guarantees, the impreciseness and potentially incomplete assumptions are problematic. Hence, I am maintaining my score for the moment but I am happy to update it if the other reviewers feel differently about these outstanding concerns.", "other_comments_or_suggestions": "- No explanation is given for the right hand side of Equation 4 (not even an intuitive/brief one). E.g Why $8|S| log(2|A|k/3δ)$ in the numerator? Why $max (1,N_k(s, a))$ in the denominator? Why the square-root?\n- It is unclear what is an optimistic MDP $\\mathcal{\\tilde M}\\_k \\in \\mathbf{\\mathcal{M}}\\_k$ . Please define it. \n- Remark 4.3. says \"One may notice that the set B also includes every MEC whose intersection with G is empty.\". How can this be true given that B is a set of states and a MEC is an MDP (from the definition in Sec 3)?\n- Cite the definition of MDPs used in the preliminaries section, or explicitly mention how it is different from a typical definition (cite).\n- cite maximal end components (MEC) \n- Cite extended value iteration (EVI)\n- Define and cite what is an Interval Markov Decision Processes \n- Line 410 should use $T^\\times : S^\\times \\times A^\\times \\times S^\\times$ instead of  $T^\\times : S^\\times$", "questions_for_authors": "Please refer to my weaknesses and comments above.", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "AtZmBImtR5", "reviewer": "Reviewer_b3Pt", "summary": "This paper tackles the problem of reinforcement learning (RL) for satisfying linear temporal logic (LTL) specifications in unknown environments modeled as Markov Decision Processes (MDPs). The authors propose what they claim is the first regret-free online RL algorithm for LTL objectives​. The approach centers on a specialized RL algorithm for infinite-horizon reach-avoid tasks (LTL “until” formulas), which is then extended to general LTL specifications by reducing them to reach-avoid problems using automata-based techniques. A separate sub-algorithm is provided to learn the underlying state-transition graph (needed for the LTL product automaton) under the assumption of a known minimum transition probability. The main contributions include rigorous finite-episode performance guarantees – in particular, a proof that the algorithm’s regret (difference in satisfaction probability compared to an optimal policy) grows only sublinearly with episodes, achieving $O(\\sqrt{K})$ regret over $K$ episodes​. This translates to sharp high-confidence bounds on how close the learned controller is to optimal after a finite number of learning episodes​. In contrast to prior methods that only guarantee eventual convergence, this work provides insight into transient performance during learning. Experimentally, the paper demonstrates the algorithm on a gridworld scenario with an LTL reach-avoid goal, showing that it quickly learns an optimal policy (regret per episode drops near zero) and significantly outperforms a recent PAC-learning baseline in terms of learning speed​. Overall, the paper’s algorithmic contributions lie in combining model-based RL (optimistic exploration, episodic resets) with formal methods (automata translation of LTL) to yield the first online LTL controller synthesis method with provable regret guarantees.", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for appreciating the depth and technical strength of our results. We plan to improve our paper taking your comments into account. Our response to your specific questions are summarized as follows.\n\n**Computational complexity:**\n\nThe primary computational steps in Algorithm 1 involve two key tasks: (1) executing the EVI algorithm, and (2) calculating $H_k$. The computational complexity of these tasks, respectively, scales quadratically and cubically, with the size of the state space. As a result, the overall computational complexity of Algorithm 1 is cubic with respect to $|S^\\times| = |S| \\times |Q|$, where $S$ is the state space of the MDP, and $Q$ is the state space of the DRA that corresponds to the given LTL specification.\n\n**Discussion on the practicality of known lower bounds for transition probabilities:**\n\nWe agree with the reviewer that in a practice deriving $p_{min}$ might be challenging. However, all we need is to know a positive lower bound for the minimum transition probability, and not its exact value. Further, the assumption of knowing $p_{min}$ is strictly weaker than the other typical assumptions such as knowing the underlying connection graph of MDP, and there are already negative results in the literature regarding the consequences of not knowing $p_{min}$ for learning against infinite-horizon specifications. Consider a simple MDP with a state set $S = \\set{s_{\\text{init}}, G}$ and a singleton action set $A = \\set{a}$, where the only outgoing transition from the initial state $s_{\\text{init}}$ has transition probability $T(s_{\\text{init}}, a, G) = \\varepsilon$. It is easy to observe that, while the optimal value is one, selecting any $p_{min} > \\varepsilon$ results in learning an MDP where the optimal value becomes zero. Hence, knowledge of $p_{min}$ is crucial for effectively learning in infinite-horizon tasks. In practice, domain-specific knowledge of the target system can be helpful in order to choose a sensible value for $p_{min}$.\n\n\n**Experimental results:**\n- Clarification regarding the implementation: We implemented only Algorithm 1 to obtain the results presented in the Appendix, assuming that the underlying graph structure is known. This assumption is justified by the fact that, for a fixed system dynamics, Algorithm 5 needs to be executed only once to learn the corresponding graph with the desired confidence. The resulting graph can then be reused for verifying any LTL specification. We will ensure that this assumption and its justification are stated explicitly in the final version of the paper.\n\n- Faster convergence compared to the $\\omega$-PAC method: We believe that this is because our algorithm uses the intermediate confidence bounds, while the $\\omega$-PAC algorithm waits until enough samples are collected, and only then starts updating its policy.\n\n- Scalability against more complex LTL specifications: As explained in Section 5, model checking for general LTL specifications over finite MDPs reduces to a reach-avoid problem over the corresponding product MDP. Therefore, regardless of the specific LTL specification, the final step always involves solving a reach-avoid problem in the product space. In response to the reviewer’s concern, we conducted an additional experiment using the same gridworld example described in the Appendix, but with a new LTL specification: \"visit $G$ infinitely often while avoiding the walls\". The performance of our method remained consistent with the results reported in Figures 3, 4, and 5. Accordingly, we plan to revise the manuscript to replace the current reach-avoid task with this LTL specification. We will also include the corresponding Deterministic Rabin Automaton (DRA) and the structure of the resulting product MDP in the appendix. Finally, we would like to emphasize that the primary contribution of this paper is the development of the first regret-free controller synthesis algorithm. The experiments are primarily intended to provide insight into various aspects of the approach, including empirical performance, the gap between practical and theoretical sample complexity, and the effect of different episode lengths.\n\n**Initialization for $H_1$:**  \n\nActually, we compute $H_1$, rather than starting with a choice. This is because we first run EVI to get an optimistic policy $\\tilde \\pi_1$ and an optimistic MDP $\\mathcal{\\tilde M}_1$. A DTMC with transition probability matrix $\\tilde{P}_1$ is induced by fixing $\\tilde \\pi_1$ over $\\mathcal{\\tilde M}_1$, and then we use Equation (10) to derive $\\tilde{Q}_1$. Finally, we use $\\tilde{Q}_1$ to compute $H_1$ by using Equation (9).\n\n\n**Proposed changes based on comments of reviewer 2:**\n- Include a remark on challenges related to estimating $p_{min}$ in practice\n- Explicitly mention that the reported experimental results correspond to run of Algorithm 1\n- Replace the current reach-avoid task with a more complex LTL specification and report the results, DRA and product MDP", "claims_and_evidence": "The key claims of the paper are generally well-supported by the content. The claim of being the “first regret-free online algorithm” for LTL specifications appears justified. All major claims (novelty of the approach, sublinear regret, reduction to reach-avoid, need for known minimum transition probability, improved transient performance over previous methods) are either mathematically proven or empirically demonstrated. We did not find over-claiming: for instance, the authors openly acknowledge assumptions like known minimum transition probability, which has been used in previous work for identifying MECs/AMECs.", "methods_and_evaluation_criteria": "The methodology is well-chosen for the problem setting. The authors build on established RL techniques for unknown MDPs (optimistic model-based exploration in an episodic framework) and tailor them to the LTL context. In each learning episode, their algorithm constructs an interval MDP using collected data and computes an optimistic policy for a reach-avoid objective (using dynamic programming over that model)​. Importantly, they introduce an episode-specific deadline $H_k$ that serves as a maximum horizon for that episode’s execution​. This deadline mechanism, combined with a reset whenever the agent encounters a trapping state that would prevent reaching the goal, is a sensible methodological choice to handle non-communicating MDPs and ensure the agent can continue learning without getting “stuck”​. How practical this \"reset button\" in reality could be discussed. The evaluation criteria used in the paper align well with the methodology and objectives. The authors emphasize regret as the primary performance metric, which directly measures how well the algorithm is doing over time relative to an optimal policy. This is appropriate since the whole point is to guarantee low regret (i.e., near-optimal behavior even during learning)​.", "theoretical_claims": "The paper provides a series of theorems and lemmas to support its theoretical claims, and these appear to be both clear and plausible. The main theoretical result is that the proposed algorithm achieves sublinear regret. The authors give a proof sketch for this (Theorem 4.4) which outlines the key idea: classifying episodes as “fast” or “slow” and showing that slow (lengthy) episodes are rare, while fast episodes incur essentially no regret​. This reasoning is intuitive and aligns with known techniques in regret analysis for episodic MDPs – by ensuring that long exploratory episodes (which might cause more suboptimal steps) don’t happen too often, the total regret can be bounded. The proof sketch references standard concentration bounds and optimistic planning arguments, suggesting the authors are leveraging established frameworks like UCRL2 but adapted to the reach-avoid setting.\n\nThe reduction from general LTL to reach-avoid via automata is supported by known results in formal methods – the paper essentially assumes one can obtain a deterministic Rabin automaton for the LTL formula and then construct a product MDP. The graph learning algorithm (Alg. 5) is given to handle unknown transitions; its correctness is stated in terms of sample complexity (Theorem A.2 in the appendix) guaranteeing that with enough samples, the learned graph matches the true MDP’s graph with high probability​. This is a sensible approach: by knowing a lower bound $p_{\\min}$, one can detect missing transitions by repeated exploration. The theoretical claim that full LTL is not PAC-learnable without such an assumption has been shown in prior work, justifying its existence.", "experimental_designs_or_analyses": "The experimental evaluation, presented in the appendix (Appendix C)​, is sound and provides evidence that the algorithm works as intended. The authors test their approach on a gridworld environment with a reach-avoid LTL specification (reach a goal region G while avoiding a set of bad states B). The gridworld setup is appropriate – it’s a classic scenario to evaluate goal-reaching under uncertainty – and they introduce stochasticity by making movements succeed with 90% probability and fail (stay in place) with 10% probability​. This ensures the problem is non-trivial (the agent must deal with uncertainty). They also treat collisions with walls as entering an absorbing bad state B​, which effectively simulates an environment where hitting a wall ends the episode (a realistic “failure” condition). The experimental metrics are well-chosen to match the paper’s objectives.", "relation_to_broader_scientific_literature": "The paper’s contributions are novel in the context of prior work on RL for temporal logic objectives. No previous work has achieved a regret bound for general LTL specifications in unknown MDPs – this is explicitly noted by the authors and supported by the literature​. Earlier approaches to LTL control learning fell into two broad categories: (a) Model-free or heuristic RL methods that ensured eventual convergence (with high discount factors or reward shaping) but offered no finite-sample guarantees, and (b) PAC-learning approaches that provided probabilistic guarantees on the final policy but not on the online performance. This work constitutes a natural extension of the (b) approaches by including a regret analysis.", "essential_references_not_discussed": "The paper’s reference list and related work discussion appear to cover the important literature in this area.", "other_strengths_and_weaknesses": "Strengths: This work is original and significant. It tackles a known challenging gap – learning controllers for complex temporal logic goals with measurable performance during learning – and provides a novel solution with strong guarantees. Another strength is the clarity of presentation: the paper is well-structured (with a clear breakdown of the problem into subproblems), and important assumptions and definitions are stated upfront.\n\nWeaknesses: One weakness is the strong assumption of knowing a positive lower bound on transition probabilities ($p_{\\min}$). While the authors make it clear this is needed for full generality (since without it, one cannot even PAC-learn LTL​), it does raise the question of how one might obtain such a bound in practice. In very large or continuous systems, $p_{\\min}$ could be extremely small or unknown. Another weakness is related to experimental validation scope. The paper demonstrates the approach on a relatively simple task (gridworld with an “until” specification). It would have strengthened the paper to see an example of a more complex LTL formula (for instance, one with an eventuality that requires the system to visit a region repeatedly, or a combination of reach-avoid tasks) to ensure the method scales to those cases. The current experiment essentially tests the core reach-avoid algorithm (Alg.1) but does not stress-test the full general LTL pipeline (Alg.4 + Alg.5) in a complex scenario.", "other_comments_or_suggestions": "Appendix C, “our algorithcm”\n\n\"episode length vary” should be “episode lengths vary”\n\nAnother suggestion is to provide a bit more clarification on the use of the term “sharp bounds” in the abstract​ – perhaps in the introduction or conclusion, explicitly state that the regret bound is on the order of $\\sqrt{K}$ (with logarithmic factors) and that this is comparable to known lower bounds in simpler settings.", "questions_for_authors": "1. How does the proposed algorithm scale with respect to the size of the state space and the complexity of the LTL formula?\n\n2. The approach requires $p_{\\min}$ to be known. How realistic is this in typical applications, and what are the consequences if $p_{\\min}$ is unknown? Can the authors elaborate on how one might choose or estimate $p_{\\min}$ in practice?\n\n3. In the experimental evaluation, did the authors implement the graph-learning algorithm (Alg. 5), or did they assume the transition graph was known in advance for the gridworld?\n\n4. The experiments show a faster convergence compared to the ω-PAC method. Could the authors provide more detail on this comparison?\n\n5. The algorithm sets an initial episode deadline $H_1$ and then adjusts it. How is $H_1$ chosen, and how robust is the algorithm to this choice?", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "oGjkv2J4Bq", "reviewer": "Reviewer_uDpf", "summary": "The paper tackles reinforcement learning (RL) under linear temporal logic (LTL) specifications in unknown Markov decision processes (MDPs). The primary goal is to guarantee sublinear regret with respect to the (unknown) optimal probability of satisfying an LTL property. From classic reach-avoid setting, author also extend to a more general setting using LTL property to a deterministic Rabin automaton.", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank you for the detailed and useful feedback! We plan to improve our paper taking your comments into account. Our response to your specific questions are summarized as follows. \n\n**Discussion on the practicality of known lower bounds for transition probabilities:**\n\nWe agree with the reviewer that in a practice deriving $p_{min}$ might be challenging. However, all we need is to know a positive lower bound for the minimum transition probability, and not its exact value. Further, the assumption of knowing $p_{min}$ is strictly weaker than the other typical assumptions such as knowing the underlying connection graph of MDP, and there are already negative results in the literature regarding the consequences of not knowing $p_{min}$ for learning against infinite-horizon specifications. Consider a simple MDP with a state set $S = \\set{s_{\\text{init}}, G}$ and a singleton action set $A = \\set{a}$, where the only outgoing transition from the initial state $s_{\\text{init}}$ has transition probability $T(s_{\\text{init}}, a, G) = \\varepsilon$. It is easy to observe that, while the optimal value is one, selecting any $p_{min} > \\varepsilon$ results in learning an MDP where the optimal value becomes zero. Hence, knowledge of $p_{min}$ is crucial for effectively learning in infinite-horizon tasks. In practice, domain-specific knowledge of the target system can be helpful in order to choose a sensible value for $p_{min}$.\n\n\n**Writing of section 4.1:**\n\nSection 4.1 is specifically dedicated to explaining various components of the main algorithm (Algorithm 1). In particular, the following components of Algorithm 1 are discussed in detail: (1) the application of Equation (4) for computing confidence intervals, which are then used to construct interval MDPs from the observed data; (2) the operation of our proposed Extended Value Iteration method (Algorithm 2); and (3) the use of Equation (9) to compute episode-specific deadlines. These explanations are provided in the respective subsections of Section 4.1. We appreciate the reviewer’s comment and will revise the writing in Section 4.1 to clarify the connections between these subsections at the outset.\n\n**Further clarification for Equation (4):**\n \nEquation (4) is used for computing confidence intervals used for constructing interval MDPs, and it is derived at earlier work (see Lemma 4.1). It provides a confidence bound for transitions for every state-action pair $(s,a)$, and is used to construct the interval MDPs.\nIn the final version, we will include Equation (4) in the body of Lemma 4.1, and also give a brief explanation regarding the terms within Equation (4).\n \n\n**Experimental results:**\n \nAs explained in Section 5, model checking for general LTL specifications over finite MDPs reduces to a reach-avoid problem over the corresponding product MDP. Therefore, regardless of the specific LTL specification, the final step always involves solving a reach-avoid problem in the product space. In response to the reviewer’s concern, we conducted an additional experiment using the same gridworld example described in the Appendix, but with a new LTL specification: “visit $G$ infinitely often while avoiding the walls.” The performance of our method remained consistent with the results reported in Figures 3, 4, and 5. Accordingly, we plan to revise the manuscript to replace the current reach-avoid task with this LTL specification. We will also include the corresponding Deterministic Rabin Automaton (DRA) and the structure of the resulting product MDP in the appendix. Finally, we would like to emphasize that the primary contribution of this paper is the development of the first regret-free controller synthesis algorithm. The experiments are primarily intended to provide insight into various aspects of the approach, including empirical performance, the gap between practical and theoretical sample complexity, and the effect of different episode lengths.\n\nProposed changes based on comments of reviewer 3:\n- Improve writing of Section 4.1\n- Include a remark on challenges related to estimating $p_{min}$ in practice\n- Replace the current reach-avoid task with a more complex LTL specification and report the results, DRA and product MDP", "claims_and_evidence": "Claims are all supported by solid proof and toy example experiment backup.", "methods_and_evaluation_criteria": "Methods and evaluation criteria make sense. Since this approach is under tabular MDP setting, experiment seems fairly easy but the major contribution is on the theory side.", "theoretical_claims": "I have walked through proof of thm 4.4 which makes sense to me, but I'm curious of the definition of transition function in eq4.", "experimental_designs_or_analyses": "Yes, the experiment makes sense under the basic tabular setting. However, it would be great if author can conduct experiments on more complex setting, eg. more complicated map?", "relation_to_broader_scientific_literature": "This work borrows idea from classic controller synthesis to", "essential_references_not_discussed": "Most of the works review know has been properly cited in the paper.", "other_strengths_and_weaknesses": "1. For the reach-avoid case, the authors prove a regret bound on the order of $O(\\sqrt{K})$ for K episodes, with high probability.\n2. By extension, for the general LTL setting (using the product MDP trick), the same $O(\\sqrt{K})$ scaling holds again, under certain assumptions such as known pmin and the ability to treat non-accepting states or MECs as “resets.”\n3. They mention gridworld-type experiments showing that their approach converges faster than a purely PAC-based method from prior literature. While not a large-scale experiment, it demonstrates that the theoretical advantage—sublinear regret—can also manifest as faster finite-time progress in practice.\n4. The biggest step forward is a proven finite-time, sublinear regret guarantee for LTL tasks in unknown MDPs, extending ideas from optimistic exploration to logic-based specifications.\n5. Once they can identify the sets of accepting vs. rejecting MECs (via pmin and some exploration episodes), they unify a wide class of LTL formulas under the same approach.\n6. A key assumption is that pmin (a positive lower bound on all nonzero transition probabilities) is known in advance. This is not always realistic.", "other_comments_or_suggestions": "1. It would be better to improve the writing for section 4.1. Each sub-section in 4.1 seems quite detached from each other.", "questions_for_authors": "1. reviewer is curious in eq4 how the bound of plausible MDPs is chosen? And what is the intuition behind current MDPs' transition bound?", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Meta-review: This paper proposes a regret-free reinforcement learning algorithm for satisfying LTL specifications in unknown MDPs. The approach begins with a method for infinite-horizon reach-avoid tasks and extends to general LTL objectives via automata-based reductions. A core contribution is the theoretical guarantee of sublinear regret in the number of episodes, supported by formal proofs and empirical evaluation in a gridworld domain.

All reviewers agree that the paper makes a significant theoretical contribution by being the first to provide regret bounds for LTL-constrained RL. The proof of sublinear regret is well-grounded in standard RL techniques, under the assumption of a known lower bound on transition probabilities ($p_{min}$). While the experiments are limited to a basic tabular gridworld, they demonstrate the algorithm’s superior sample efficiency compared to a PAC-learning baseline. The assumption of $p_{min}$ is noted as a potential limitation in practical scenarios. Reviewers also expressed concerns about the clarity of Section 4.1 and Algorithm 1. The authors are encouraged to clarify how their analysis builds upon Tarbouriech et al. (2020), particularly in the key proofs, and to clearly explain how the assumption of SSP-communicating MDPs is relaxed in their work.

Overall, the paper makes a compelling and novel contribution to LTL-constrained RL by introducing a regret-based framework with rigorous theoretical support. Despite some concerns about presentation clarity, the work substantially advances the field. The meta-reviewer encourages the authors to revise the manuscript based on the reviewers' feedback.
Decision: Accept (poster)