Policy Optimization with Linear Temporal Logic Constraints
Authors: Cameron Voloshin
Hoang Minh Le
Swarat Chaudhuri
Yisong Yue
Venue: NeurIPS 2022 Accept (2022)
Keywords: Reinforcement Learning
RL
Linear Temporal Logic
LTL
Constrained
Policy
Optimization
Learning

Abstract: We study the problem of policy optimization (PO) with linear temporal logic (LTL) constraints. The language of LTL allows flexible description of tasks that may be unnatural to encode as a scalar cost function. We consider LTL-constrained PO as a systematic framework, decoupling task specification from policy selection, and an alternative to the standard of cost shaping. With access to a generative model, we develop a model-based approach that enjoys a sample complexity analysis for guaranteeing both task satisfaction and cost optimality (through a reduction to a reachability problem). Empirically, our algorithm can achieve strong  performance even in low sample regimes.

Policy Optimization with Linear Temporal Logic Constraints
Cameron Voloshin Caltech
Hoang M. Le Argo Al
Swarat Chaudhuri UT Austin
Yisong Yue Argo AI Caltech
Abstract
We study the problem of policy optimization (PO) with linear temporal logic (LTL) constraints. The language of LTL allows flexible description of tasks that may be unnatural to encode scalar cost function. We consider LTL-constraieed PO systematic framework, decoupling task specification from policy selection, and as an alternative the standard of cost shaping. With access a generative model, we develop a model-based approach that enjoys sample complexity analysis for guarantceing both task satisfaction and cost optimality (through a reduction to a reachability problem). Empirically, our algorithm achieve strong performance even in low-sample regimes.
Introduction
The standard reinforcement learning (RL) framework aims find policy that minimizes cost function. The premise is that this scalar cost function can completely capture the task specification (known the "reward hypothesis" [55] (3)). To date, almost all theoretical understanding of RL is focused on this cost minimization setting (c.g., 62 32 31
45
10 3
47 48)).
However, capturing real-world task specifications using scalar costs can be challenging. For one, real- world tasks often consist of objectives that are required, as well as those that are merely desirable. By combining these objectives into scalar costs, one erases the distinction between these two categories of tasks. Also, there is recent theoretical evidence that certain tasks are simply not reducible to scalar costs [1 (see Section 2. In practice, one circumvents these challenges using heuristics such as adding "breadcrumbs" " 54 However, such heuristics can lead catastrophic failures which the
learning agent ends up exploiting the cost function in an unanticipated way 44 61 28 68 44]
In response these limitations, recent work has studied alternative RL paradigms that use Linear Temporal Logic (LTL) to specify tasks (see Section 7 LTL is modeling language that can express desired characteristies of future paths of the system [1]. The notation is precise enough to allow the specification of both the required and desired behaviors; the cost minimization is left only to discriminate between which satsssatss policy is "best". This ensures that the main objective e.g., time, energy, effort - does not have any relation to the task and is easily interpretable.
Existing work on RL with LTL constraints tends make highly restrictive assumptions. Examples include (i) known mixing time of the optimal policy 233, (ii) the assumption that every policy satisfies the task eventually [64]. or (iii known optimal discount factor (26), all of which assist in task satisfaction verification. These assumptions have complex interactions with the environment, making them impractical if not impossible calculate. The situation is made more complex by recent theoretical results [66] 7 that show that there are LTT. tasks that are not PAC-MDP-learnahle.
In this paper, address these limitations through novel policy optimization framework for RL under LTL. constraints. Our approach relies on two assumptions that are significantly less restrictive than those in prior work and circumvent the negative results on RL-modulo-LTL: the availability
36th Conference on Neural Information Processing Systems (NcurIPS 2022).

---

of a generative model of the environment and lower bound on the transition probabilities in the underlying MDP. Under these assumptions, we derive a learning algorithm based on reduction to reachability problem. The reduction in our method can be instantiated with several planning procedures that handle unknown dynamies [22 46]. We show that our algorithm offers strong constraint satisfaction guarantees and give rigorous sample complexity analysis of the algorithm.
In summary, the contributions of this paper are:
1. We provide a novel approach to LTL-constrained RL that requires significantly fewer assumptions, and offers stronger guarantees, than previous work.
2. We develop several new theoretical tools for our analysis. These may be of independent interest.
3. We empirically validate using both infinite- and indefinite-horizon problems, and with composite specifications such collecting items while avoiding enemies. We find that our method enjoys strong performance, often requiring many fewer samples than our worst-case guarantees.
2 Motivating Examples
We examine two examples where standard cost engineering cannot capture the task (Figure D.. We consider the undiscounted setting here. See [4 for difficult examples for the discounted setting.
Example (Infinite Loop). A robot is given the task of perpetually walking between the coffee room and the office (Figure [ (Left)). To achieve this behavior, both the policy and cost-function must be distory-dependent. These can be made Markovian through proper state-space augmentation and has been studied in hierarchical reinforcement learning or learning with options [38] (66.. Options engineering is laborious and requires expertise. Nevertheless, without the appropriate augmentation, any cost-optimal policy Markovian cost function will fail at the task. We will see in Section that any LTL expression comes with automatic state-space augmentation, requiring no expert input.
Example 2 (Safe Delivery). The goal is to maximize the probability of safely sending packet from one computer to another (Figure [ (Right). Policy leads to a hacker sniffing packets but passing them through, and is unsafe. Policy 2 leads to hacker stealing packets with probability p 0, and is safe with probability 1 - p. and is the policy that satisfies the task. For cost engineering, let R and S be the recurring costs of the received and stolen states. For the two policies, the avg. costs are R and O2 PS + (1 R.. Strangely, we must set R > S in order for < 91. Fortunately, optimizing any cost function constrained satisfying the LTL specification does not suffer from this counter intuitive behavior as only policy 2 has any chance of satisfying the LTL expression.
Figure 1: (Left) Infinite Loop. The robot must perpetually walk between the coffee and office.
Without proper state-space augmentation, a markovian cost function cannot capture this task. (Right) Safe Delivery. The specification is to deliver a packet without being interfered. Policy 2 should be chosen. One would need to penalize receiving the packet significantly over having it stolen: R > S.
3 Background and Problem Formulation
We now formulate the problem. An atomic proposition is variable that takes truth value. An alphabet over a set of atomic propositions AP is given by Σ = 2AP For example, if AP = {a. 6} then Σ (U. (a), (b), b)). A(X) represents the of probability distributions over set X.
3.1 MDPs with Labelled State Spaces
We assume that the environment follows the finite Markov Decision Process (MDP) framework given by the tuple M (SM) M P.M C.M. d. M) consisting of finite state space S.M a finite

---

action space A an unknown transition function P.M. S.M x A. + A(SM). cost function C: C:SM; x AM [[[Cmin: Smax]) D) an initial state distribution dn E A(SM). and labelling function I,M; : S.M - E. We take (s) to be the set of available actions in state Unlike traditional MDPs, M has a labeling function I,M which returns the atomic propositions that are true in that
state. A run in M is sequence of states T = (8o. $1....) reached through successive transitions.
3.2 Linear Temporal Logic (LTL), Synchronization with MDPs, and Satisfaction
Now we give some basic background on LTL. For more comprehensive overview, see
Definition 3.1 (LTL Specification, Øp). An LTL specification +p is the entire description of the task, including both desired and required behaviors, and is constructed from a composition of atomic propositions, including logical connectives: not (-), and (&), and implies (->); and temporal operators: next (X), reppentedly/llwwyyy/lbblll (G), eventually (F), and until (U).
Examples. Consider again the examples in Section 2 For AP = fa, b), some basic task specifica- tions include safety (G-a), reachability (Fa), stability (FGa). response (a aa> Fb), and progress (a & Fb). For the Infinite Loop example (Figure (Lef)), AP = {o,c} indicating the label of the grid location of our agent (office, coffee, or neither). The specification is "GF(o & X Fe)" meaning "go between office and coffee forever", and is combination of safety, reachability, and progress. For the Safe Delivery example (Figure I (Right)), AP = {s} indicating the safety of a state. The specification is "Gs" meaning "always be safe".
Synchronizing MDP with LTL. By synchronizing an MDP with LTL formula, we can easily check if run in the MDP satisfies a specification In particular, it is possible to model the progression of satisfying y through specialized automaton, an LDBA B, [52], defined below. More details for constructing LDBAs are in [25] 11 35]. We drop from B, for brevity.
LTL Satisfaction:
Definition 3.2. (Limit Deterministic Büchi Automaton, LDBA (52)) An LDBA is a tuple
(88; Σ As, PB " , consisting of (i) a finite set of states S (ii) finite alphabet Σ = 2 As is set of indexed jump transitions (iii) a transition function pB S (E) - 25t (iv) accepting states SB+ S S and (v) initial state s6. There exists a mutually exclusive partitioning of 5 S U s such that Sh+ S St and for s E S a E then (s, S ST and only (possibly) non-empty for E S and allows B to transition without reading an AP. A path a = ($0.$1,... .1....) is sequence of states in B reached through successive transitions. accepts a path a if there exists some state SB+ in the path that is visited infinitely often.
[P a)l 1, deterministic. Ag(s)
We can now construct a synchronized product MDP from the interaction of M and B.
Definition 3.3. (Product MDP) The product MDP XM.55 = (S,A, do, L, L,) is MDP with S = S.M x 8 A = A u A C( b), a) = (M(.ma) if a E (M() otherwise 0. do = {m, bm E d b E (s I. I.M(m)); ], I((m, b)) (M = ((.b) S/b E SBr) accepting states, and P S x A + A(S) taking the form:
P. pmMmma. m')
a (M)), U' pb L(m'))
P((m, b), (ml,
1,
E A e p8(6, a), m m
0.
otherwise
A run T = (so, .1....) ((my. bu), (m1.br .......) in X' is accepting (accepted) if (bo, by....) ..). the projection onto B, accepted. Equivalently, some E S* in X' visited infinitely often. This leads us to the following definition of LTL satisfaction:
Definition 3.4 (Satisfaction, 7 += sp). A run 7 in X' satisfies sp denoted r == y, if accepted. Definition 3.5. (Satisfaction, }= sp) A policy E πI satisfies &o with probability P(x } yo] E [1 -p] Here, 1x is an indicator variable which is when is true, otherwise 0. T.P is the set of trajectories induced by in X' with transition function P.
3.3 Problem Formulation
Our goal is to find a policy that simultaneously satisfies given LTL. specification &o with highest probability (probabilit-ootiima) and is also optimal w.r.t. the cost function of the MDP, We consider
3

---

(stochastic) Markovian policies II, and define the set of all probability-optimee policies as Imax F pl]. We first define the gain g (average-cost) and transient cost J:
farg m P(
C(sn ((s))) (())) xl
gT EE
lim T T-+00
Σ C(s,, ((x)))
B
Clss,
(I)
where Ky is the first (hitting) time the trajectory leaves the transient states induced by m. When P clear from context, abbreviate of and J by In and Jn. respectively.
Gain optimality for infinite horizon problems has long history in RL [12] 46). Complementary to gain optimality, we consider hybrid objective including the transient cost. For any À 2 0, the optimal policy is the probability- opttimll policy with minimum combined cost:
arg
min max
Jx
Agn = arg min TEll
(Jx + Ag. )P + (= (=VV.)).
(OPT)
In other words, probability-optiine policies are those that satisfy the entirety of the task, both desired and required behaviors, whereas V.. (J, + P }= sp] is the normalized value function corresponding to notion of energy or effort required, with À representing the tradeoff between gain and transient cost. We will often omit the dependence of V on P and À for brevity.
Example. Consider the Safe Delivery example (Figure I (Right)). For policy 1, IP(1 = 4] 0 and so 1 & max. Let policy be cost 1 timestep before stolen receipt, then 92 R is the (conditional) gain, J2- = 1 is the (conditional) transient costs, IP[2 = p - 1 p, and V22 - (1 + ( - p).
Problem (Planning with Generative Model/Simulator). Suppose access to generative model of the true dynamics P from which we can sample transitions s' ~ P(s. a) for any state-action pair (s. a) x A With probability 1-6 8, for some errors c,., Ey >> 0, find a policy π E II that simultaneously
has the Tollowing properties: (i) |IP(T = xp] - P( - spl < exp
(ii) VV= V.- ev.
4 Approach
4.1 End Components & Accepting Maximal End Components
Our analysis relies on the idea of an end component: a recurrent, inescapable set of states when restricted to certain action set. It is a sub-MDP of a larger MDP that is probabilistically closed.
Definition 4.1. (End Component, EC/MEC/AMEC (IT) Consider MDP (S, P. C, do L*).). ). An end component AE)A) is a set of states E S S and acceptable actions AF(s) C A(s) (where E F)) such that v((s,) E F x AE then Post(s, a) = {s'|P(s, a, 8') > 0} C F. Furthermore, reachable from one another by means of actions in Ag. We say an end component (E, Ag) ] is maximal (MEC) if it is not contained within larger end component (E',A'' ie. 3(E", Agr) ) EC where E S E", Ag(s) S Ag (s) for each s E A. A MEC (E, Ag) is accepting MEC (AMEC) if it contains an accepting state, Es E E s.t. s S S*.
(F., AE) is strongly connected: any two states in
4.2 Heve-Level Intuition
The description of our approach, LTL Constrained Planning (LCP), in Section 4.4 is rather technical in order to yield thcoretical guarantees. We thus first summarize the high-level intuitions.
Solution Decomposition. Consider the accepting states st s in Figure (Left), which are the states we need to visit infinitely often to satisfy the specification. First, let us identify the accepting maximal end components (AMECs) of s and s²: the state sets A, and A₂ (resp.) and their corresponding action sets AA, and As, (the blue arrows in A₁ and A2). Note that these AMECs do not include the yellow action Figure 2 (Left), which has a chance of leaving A and getting stuck in Ag.
Our solution first runs a transient policy until reaching A1 or Ag, and then switches to (probability- optimal) recurrent policy that stays within A₁ or Ag (resp.) while visiting si or s (resp.) infinitely often. A probability-optmmal recurrent policy will select actions in AA. and AA, to visit si si
Normalized objectives are not unusual in RL, e.g. in discounted settings, multiplication by (1-7) 7) 2 'The use of a generative model is increasingly common in RL [24 40 3 58) and is applicable in many settings where such generative model is readily available simulator (e.g.. (11..

---

80
$0
A
A2
(b) Example, Infinite Loop
(c) Example, Safe Delivery
(a) Abstract Diagram
Figure 2: Product MDP diagrams. (Left) The goal of L.L. Constrained Policy Optimization can be reduced to a reachability problem. We want to reach A1 or A2 from and then follow the blue arrows with some distribution. A3 with the blue arrows is rejecting end component because it does not contain an accepting state s". For B < 1, the yellow action is not in the allowable action set of A because there is a risk entering Ag, strictly decreasing our probability of LTL satisfaction. (Center) Example for Infinite Loop, Figure Left. (Right) Example for Safe Delivery, Figure [ Right.
infinitely often (e.g,, the uniform policies with the AMECS (AI,AA,) and Aa,)) )) Finding a transient policy from to A2 can be viewed as a reachability problem. which we can solve via a Stochastic Shortest Path (SSP) problem and leverage recent literature [58] 34.
Cost Optimality. As stated in OPT the goal to find a cost-optimal policy within the set of roopaaa policies. For instance, the uniform policy over AA, and AA, (the blue arrows in Figure 2 (Left) is probability optimal, but may not be cost optimal. Similarly, the unconstrained cost-optimal policy may not be probability optimal. Consider just Ai for the moment. Suppose the cost of the arrows between the white nodes is 4 while the other costs are 7. Then the uniform 5. The gain-optimal policy that deterministically selects the actions between the white nodes # has cost (4#1) = but is not probability optimal. If we perturb से to make it even slightly stochastic (but still mostly deterministic, i.e 7-greddy with vi Rs 0), then it will be arbitrarily close to gain optimality and also recover probability optimality. This is preferable probability-optimal policy over the uniform policy,
(probability-optimal policy in A₁ over AA, has cost (444) + (T+I*4)
Overall Procedure. The high-level procedure is: (i) identify the AMECs (e.g. (A1, AA, ), (A2, A2))
by filtering out bad actions like the yellow arrow; (ii) find a cost-optimal (optimal gain cost) recurrent policy in each AMEC that visits some s* infinitely often; (iii) instantiate an SSP problem that finds a cost-optimal (optimal transient cost) transient policy from to A U A2 and avoids A3; (iv) return a policy that stitches together the policies from (ii) and (iie). See Section for the algorithmic details. We show in Section 5 that this solution gives the optimal solution to OPT
4.3 Additional Assumptions and Definitions
Perhaps surprisingly, when planning with simulator (i.e., generative model), even infinite data is insufficient to verify an I.TI. formula without having a known lower-bound on the lowest nonzero probability of the transition function P [I]. Without this assumption, LTL constrained policy learning is not learnable [66]. We thus begin by assuming a known lower bound on entries in P on the lowest Assumption 1 (Lower Bound). We assume we have access a lower bound non-zero probability of the transition function P (Sec. 3.7):
<< 3
min E
(P(s, a, a, s))ss,,)))) 0).
We assume that all the costs strictly positive, avoiding zero-cost (or negative-cost) cycles that trap a policy. Leveraging cost- cosst-erturbations and prior work [58) can remove the assumption.
Assumption 2 (Bounds cost function). The minimum cost Cmin > 0 (Sec. 3.7 is strictly positive.
Let D = {(s, a, 3')} be all the collected samples (s, a, while running the algorithm. At any (()e). is the empirical frequency of visiting s' from (s, a). We introduce point, a(s. [((.a)ED)]
"Our assumptions consistent with the minimal requirements studied by 41
5

---

an event & and error (n) to quantify uncertainty on a(s.a.s) based on current data: n(s.a) [(s,a) E D) & is based on empirical Bernstein bounds 142,, and holds w.p. 6 (Lemma B.1 Definition 4.2 (High Probability Event). A high probability event E:
= a s' E x A S, an(s, 1: ((((,,,,')) P(s, s')) S Vsns (n) S (b()))
where Year (n)) = V 81 ((),,,,)) + 55(m), v(n) = V + _5(n), and
{(n) log( In )
Remark 4.1. For some p > O, if we require P(ss, s') (ss. a, s')l S. then we need n a)
/ (p) samples for state-action pair (s, a). See Lemma B.2 for the quantity &o (p).
Definition 4.3 (Plausible Transition Function). The set of plausible transition functions is given by
P(s, a, s²) P(s, s'),,, (s) P(s,a,5)) weas' n [ 1181--8. otherwise
F(s,a,8') E {0. 13 (3)
P P= P= A(S)
Let P(s, =) (P(s, a. P) be the possible transition distributions for state-action pair (s, a). We denote 8= Bawn [Ps, s')] as the Markov chain given dynamics P with policy and
can be thought of as a |S| |S] matrix Pa {pt) {
4.4 Main Algorithm: LTL Constrained Planning (LCP)
Algorithm LTL Constrained Planning (LCP)
Param: Error ev 0, Error Co > O, Tolerance 8 Lower bound
0 (see Assumption |/ Empirical estimate of P
I: Globally, track Pss, 8') H[S
(EDD
2: ((A), AAy)......... (Am, AA,)) + (S,,
3: for 1,.... do
4: Set Ti f- (l )
Plan gain-optimal policy m, for A (annTraanien(((A1gg)))) (Ak, gk)), 20r) // Plan shortest paths policy mo Ui A;
5: Set
6: return Ui
Our approach, LTL Constrained Planning (LCP), has three components, shown in Algorithm 1 and described below. Recall from Problem I that the policy optimization problem OPT is instantiated over product MDP (Def. 3.3), and that are given generative model of the true dynamics P from which we can sample transitions s' ~ P(s, a) for any state/action pair.
Finding AMECs (FindAMEC). After sampling each state-action pair Oplnaamec = ( times (see
Prop. B.4). by Assumption T we can verify the support of P. We can compute all of the MECs using Algorithm 47 from [1]. Among these MECs, we keep the AMECCs, which amounts to checking
the MEC AA, contains an accepting state s" E S' from the given product MDP.
PlanRecurrent (PR).
plan in each AMEC (A,Aa) (i.e., find the optimal recurrent policy), we use Alg. 2 with (extended) relative value iteration (VI, Alg. 4 in appendix) using the optimistic Bellman operator L.g (see Table we discuss a in next paragraph). Let Tu denote the greedy policy w.r.t. the fixed point = Cp (u is the optimistic value estimate). Using the greredy policy, = (1 n) + (Unif(AA) (Alg. 2 Line 7), together with Px. makes A re- current: s* A is visited infinitely often and PP(m | s/ E A = 1. Since can be arbitrarily small (Lemma B.7 then In Jr, and n is both cost and probability optimal. As intuited in Sec-
Algorithm PlanRecurrent (PR)
Param: AMEC (A, As), error 6za >0
1: Set 27((FFiarrec 11 P P
2: repeat
Set p 2
4: Sample Φ (p) times V(s a) E Ax AA
5:
v',u, P VI dea. Eaa) 11 v' L
6: until p 3/
(=(1)
#1 ||p
Pll1 small
7: Set policy + g-gredy policy w.r.t. v'
Set gain 9- + (m v) min(o' - u))
9: return gs
tion 4.2 has full support over Aa but is nearly
deterministic
'Interestingly, typical RL settings admit a fully deterministic optimal policy, but for LTL constrained policy optimization the optimal policy may not be deterministic (although can be very nearly so).

---

Table 1: Subroutine Operators and Parameters for Value Iteration
Op/Param
Description
Chav(s)
min.eAA(1) (C(s, + minyee((..)) p) (1 a)v(s) Vs E A
dea(Va+1, un) cnn
max.ca (s)) - min.ca (Un=1(s) (s) - vn(ss) ) <
3
min (minGeAs(1) (C( a) mimpe p²v) v0),V/15 V/Ep):
8E8) - SE
Loru(s)
Age.
der(Un+1, un) <EP
110+11 valla Epnp
is an iterative procedure (Alg. 4 in appendix), and terminates via dra < PA VI in Line 5 of Alg.
(Table D. Convergence of extended VI is guaranteed [46] [29] [22], so long the dynamics. P arg min PePssaa p v, achieving the inner minimization of Zep are aperiodic - hence the aperiodicity transform E (0, 1) in CP 46]. Computing P can be done efficiently [29] (Alg. 5 appendix). For
stability, we shift each entry of Un. by the value of the first entry vn (0) 12
Alg. returns the average gain cost In of policy π when we have enough samples for each state-action pair in (A, to verify that n > - (<a((-A((P))) where A(P₂) = max;; Σx Pix
Pykl
Here, A(P=) is an easily computable measure on the ergodicity of the Markov chain P
18 We
track (n) (recall Def. 4.2 via variable p and sample (p) p² (see Lemma
B.2
samples
from each state-action pair in AA) (Alg. 2 Line 4). We halve / each iteration (Alg. Line 3)
and convergence is guaranteed because p will never fall below some unknown constant
A
6|.4] Giuoo
(see Lemma B.8 the halving trick is required because Å is unknown priori.
Proposition 4.2 (PR Convergence & Correctness, Informal). Let TA be the gain-optimal policy in G]A]cmas AMEC (A, Algorithm terminates after most log2 (=a(1-Aa)
repeats, and collects most
=0 |A 2
(e(1-A)))) samples for each (s, a) (A, The 7-greedy policy w.r.t. v' (Alg. 2 Line
5) is gain optimal and probability optimal: 1ga 9 < Eps. P|T + 0/50 E =.
Plan Transient (PT). This is the stochastic shortest path (SSP) reduction step that finds policy from the initial state so to the AMECs (Alg. 3). The main algorithmic tool used by PlanTransient is similar to that of Pl PlanRecurrent: it also uses extended value iter- ation (VI, Alg. 4 in appendix) but with different optimistic Bellman operator Lpt (Table [ and then returns a (fully deterministic) greedy policy w.r.t. the resulting optimistic value u (Alg. 3 Line 4). LPT is used to calculate the highest probability, lowest cost path to the AMECs (Alg. Line 3).
Algorithm PlanTransient (PT)
Param: States & gains: {(Ai, ((A,g)))== eTr. for > 0
I: Set Vr(s) = Àgı for E As /1 Terminal costs
2: Sample ovr times V(s,a) a) (S UA:)) A
3: v', v' P.P
VI(Cer, dor, cf, Vr) Il d' Larv
4: Set g-geedy policy w.
return π
Since rejecting end components might exist (see Ag from Figure 2 (Left)), a trajectory may end up stuck and accumulate cost indefinitely, and In Prop. 1.13 we show how to select V such that π will reach the target states (in this case, the AMECs), first with high prob and then with lowest cost. The existence of such a bound on ||u||oo was shown to exist, without construction, in 34 In practice, choosing large V is enough.
must bound | co < VEEEp to prevent blow up.
The terminal costs Vr (Alg. 3 Line 1) together with Bellman equation LpT has value function V Rs p(Jx + + - P:9r.) + //V/ Rs Va, relating to Vn (OPT). see Section A.
Here,
p: = P| reaches A,J = E E, [lawer [ stsea,] and p = Σ Pr. VI converges when der < EPT
(see Table D. Convergence of extended VI for SSP is guaranteed [58 34] The number of samples
required for each state-action pair (s,a) E (S \ UA;)) x is OPT
Cmin MI
Proposition 4.3 (PlanTransient Convergence & Correctness, Informal). Denote the cost- and 1
prob-optimal policy as x'. After collecting at most n 3( Ö(1 samples for each (s.a) (S U Ar) x A, the greedy policy N w.n.t (Alg. Line 3) is both cost and probability optimal: VV Var EpTy
[PP[T reaches _ A.J IP[ reaches U._ Aill S Exp.
7

---

End-To-End Guarantees
The number of samples necessary to guarantee an cq, E,, PP- approximation to the cost-optimal and probability-optimal policy relies factors: 8 (lower bound on the min. non-zero transition probability of P), {Cmin: Cmax] (bounds on the cost function C), AA; (worst-case coefficient of ergodicity for EC AA,)), V (upper bound on the value function), and À (tradeoff factor).
Theorem 5.1 (Sample Complexity). Under the event &, Assumption 7 Mand after
n n= 0= 1
(181214 minn
| "max
22
E/
(1-AA
sample fare collected from each state-action pair, the policy returned by Algorithm 6, simultaneously ey-cost optimal and egg pprobability optimal, satisfying:
7
is, with
probability
(i) [P + p] - P| + r|] S
(ti)
11V Vx- Iloe <v..
(4)
With a sufficiently large À (which may not be verifiable in practice), is also gain optimal. Corollary 5.2 (Gain (Average Cost) Optimality). There exists X > 0 s.t. s.t.for for X X", the policy a 9n arg min.s 9n', and is probability and gain optimal.
returned by Alg. 7 satisfies
The bigh-level structure of our analysis follows the algorithm structure in Section 4.4 via composing the constituent guarantees. To complete the analysis, we develop some technical tools which may be of independent interest, including a gain simulation Lemma B.8 and an r-greedy optimality Lemma B.7 For ease of exposition, we also ignore paths between AMECs (see Appendix (.2).
6 Empirical Analysis
We perform experiments in two domains: (1) Pacman domain where agent find food and indefinitely avoids a ghost; (2) discretized version of mountain car (MC) [44 where the agent must reach the flag. Our goal is to understand whether: (i) our ICP approach [Alg[) produces competitive polices; (ii) LCP can work in continuous state spaces through discretization; (iii) LCP can enjoy efficient sample complexity in practice. For baseline, we use Logically Constrained RL (LCRL, (26)), which is
Q-learning approach to LTL-constrained PO in unknown MDPs. We also do heavy cost shaping to LCRL as another baseline. See App for more details, experiments, and figures.
6.1 Results
Competitiveness of the policy in full LTL specs? The probability of LCP satisfying the LTL
spec in Figure 3 (Left) approaches 1 much faster than the two baselines. The returned policy collects the food quickly and then stays close, but avoids, the ghost. Any pol- icy that avoids the ghost is equally good, as we have not incentivized to stay far away. LCRL redefines cost as 1 if the LTL solved and otherwise, which is too sparse and learning suffers. Indeed, shaped LCRL performs better than straight LCRL.
Pacman
Mountain Car
1.0
08
0.8
Better
0.6
08
LCP (Gurs)
Better
(shaped)
0.2
0.2
LCRL
Max
0.0
0.0
1.00
190
Better
Timesteps
Better
60
170
100
20
Performance in continuous state space? Similarly, the probability of satisfying the LTL spec in Figure 3 (Right) goes up to However, here the LCRL (shaped) base- line performs relatively well as it is being given "breadcrumbs" for how to solve the task. Our algorithm performs well without needing any cost shaping. Standard LCRIL fails to learn. This experiment demonstrates that our method can be used even in discretized continuous settings.
Total Number Samples (x10P)
23
30
411
50
60)
Total Number of Samples (x10P)
100
160
200
Figure 3: Results. (Left Column) Pacman. ip to eventually collect food and always avoid the ghost. We let the system run for a maximum of 100 timesteps. (Right Column) Discretized Mountain Car (MC). up is to eventually reach the flag.
samples required. See Appendix Section [og(1-8) whereas ours is Ō We conjecture that (()
*The lower bound relating 8 from 41 is Q log(28)
8

---

Sample Complexity? Our theory is quite conservative w.r.t. empirical performance. In Pacman (Figure B Left), Thm. 5.1 suggests = 350 samples per (s, a) pair just to calculate the AMECs. Empirically, LCP finds good policy after 11 samples per (s, a) pair (~ 66k/6k samples/pair).
Other Considerations. One of the strengths and potential drawbacks of L.TL is its specificity. If a s, for a truly infinite horizon problem, is to "eventually" do something, then accomplishing the task quickly is not required. As finite horizon problem, in MC (Fig. 3 Right) SSP finds the fastest path to the goal. In contrast, since any stochastic policy with full support will "eventually" work, the policy returned by LCP for Fig (Left) (Fig. Center, & App Fig. | may take exponential time to complete a single loop. Two straightforward ways to address this issue are: (a) including explicit time constraints yo: and (b) cost shaping to prefer policies reaching some s" quickly and repeatedly,
Unlike standard cost-shaping, 4 satisfaction is still guaranteed since the cost is decoupled from yp
7 Related Work
Constrained Policy Optimization. One attempt at simplifying cost functions is to split the desired behaviors from the required behaviors. The desired behaviors remain as part of the cost function while the required behaviors are treated as constraints. Recent interest in constrained policy optimization within the RL community has been related to the constrained Markov Decision Process (CMDP) framework 6 33 43). This framework enables clean methods and guarantees, but enforces expected constraint violations rather than absolute constraint violations. Setting and interpreting constraint thresholds can be very challenging, and inappropriate in safety-critical problems (38].
LTL + RL. Recently, LTL-constrained policy optimization has been developed as an alternative to CMDPs 4T. Unlike CMPDs, the entire task is encoded into an LTL expression and is treated the constraint. Q-learning variants when dynamics are unknown and Linear Programming methods when dynamics are known are common solution concepts (50) 26 13 16 (0). The Q-learning approaches rely on proper, unknowable tuning of discount factor for their guarantees. Theoretically oriented works include 23 While providing PAC-style guarantees, the assumptions made in these works rely on unknowable policy-environmen interaction properties. We make no such assumptions here.
high-level specifications that can be translated into reward machines (30). These works are generally empirical and handle finite repeated finite problems (episodic problems at test time); they can only handle smaller set of LTL expressions. specifically regular expressions. Our work handles w-regular expressions, subsuming regular expressions and requires nontrivial leap, algorithmically and theoretically, to access the broader set of allowable expressions. Many problems are w-regular problems, but not regular, such as liveness (something good will happen eventually) and safety (nothing bad will happen forever). The works that attempt to handle full LTL expressibility redefine reward as 1 if the LTL. is solved and 0 otherwise; the cost function of the MDP is entirely ignored.
Another solution technique is employing reward machines [60] 17 633
Verification and Planning. As an alternative to our approach, one might consider LTL satisfaction verification and extend an optimization technique by checking every policy (which will naively take an exponential amount of samples to verify a single policy [5 8). Many verification approaches exist (36
27 and among the ones that do not assume known dynamics, the verification guarantees rely on quantities as difficult to calculate as the original verification problem itself (8).
8 Discussion
We have presented novel algorithm, LCP, for policy optimization under LTL constraints in an unknown environment. We formally guarantee that the policy returned by LCP simultancously has minimal cost with respect to the MDP cost function and maximal probability of LTL satisfaction. Our experiments verify that our policies are competitive and our sample estimates conservative.
The assumptions we make are strong, but to the best of our knowledge, are the most relaxed amongst tractable model-based algorithms proposed for this space. Model-free algorithms (Q-learning) have less stringent assumptions but do not come with the kind of guarantees that our work has and largely ignore the cost function, solving only part of the problem. An interesting future direction would be to extend our work to continuous state and action spaces and settings with function approximations.

---

Acknowiedgements. Cameron Voloshin is funded partly by an NSF Graduate Fellowship and a Kortschak Fellowship. This work also supported in part by NSF #1918865, ONR #N00014-20-1-2115, and NSF #2033851.
References
[1] David Abel, Will Dabney, Anma Harutyunyan, Mark K Ho, Michael Littman, Doina Precup, and Satinder Singh. On the expressivity of markov reward. In Advances in Neural Information Processing Systems, 2021.
[2] Joshua Achiam, David Held, Aviv Tamar, and Pieter Abbeel. Constrained Policy Optimization. In Proceedings of the 34th International Conference Machine Learning, 2017.
[3] Alekh Agarwal, Sham Kakade. and Lin F Yang. Model-based reinforcement learning with generative model is minimax optimal. In Conference Learning Theory, 2020.
[4] Alekh Agarwal, Sham M Kakade, Jason D Lee, and Gaurav Mahajan. Optimality and approximation with policy gradient methods in markov decision processes. In Conference on Learning Theory, 2020.
[5] Gul Agha and Karl Palmskog. A survey of statistical model checking. ACM Trans. Model. Comput. Simud., 28(1), jan 2018.
[6] Eitan Altman. Construined Markov Decision Processes: Stochastic Modeling. Routledge, Boca Raton, edition, December 2021.
Rajecv Alur, Suguman Bansal, Oshert Bastani, and Kishor Jothimurugan. A framework for transforming specifications reinforcement learning. arXiv preprint arXiv:2 1..00222, 2021.
[8] Pranav Ashok, Jan Křetínský, and Maximilian Weininger. Pac statistical model checking for markov decision processes and stochastic games. Isil Dillig Serdar Tasiran, editors, Computer Aided Verification, page 497-519. Cham, 2019. Springer International Publishing.
Alex Ayoub, Zeyu Jia, Csaba Szepesvari, Mengdi Wang, and Lin Yang. Model-based reinforcement learning with value-targeted regression. In International Conference on Machine Learning, 2020.
[10] Kamyar Arizzadenesheli, Alessandro Lazaric, and Animashree Anandkumar. Reinforcement learning of pomdps using spectral methods. In Conference Learning Theory, 2016.
[11] Christel Baier and Joost-Piete Katoen. Principles of model checking. The MIT Press, Cambridge, Mass, 2008.
[12] Dimitri P Bertsekas et al. Dynamic programming and optimal control 3rd edition, volume ii Belmont, MA: Athena Scientific, 2011.
[13] Alper Kamil Bozkurt, Yu Wang. Michael M. Zavlanos, and Miroslav Pajic. Control synthesis from linear temporal logic specifications using model-free reinforeement lcarnigg In 2020 IEEE International Conference on Robotics and Automation (ICRA), pages 19349-10355, 2020.
[14] Greg Brockman, Vicki Cheung, Ludwig Pettersson, Jonas Schneider, John Schulman, Jie Tang, and Wojciech Zaremba. Openai gym, 2016.
[15] Tomáš Brázdil, Krishnendu Chatterjee, Martin Chmelik, Vojtech Forejt, Jan Křetínský, Marta Kwiatkowska, David Parker, and Mateusz Ujma. Verification of markov decision processes using learning algorithms. In Franck Cassez and Françços Raskin, editors, Automated Technology for Verification and Analysis, page 98-1 14, Cham, 2014 4. Springer International Publishing.
[16] Mingyu Cai, Shaoping Xiao, Zhijun Li, and Zhen Kan. Optimal probabilistic motion planning with potential infeasible Itl constraints. IEEE Transactions Automatic Control, pages 1-1, 2021.
[17] Alberto Camacho, Rodrigo Toro Iearte, Toryn Q. Klassen, Richard Valenzano, and Sheila A. Mcllraith. Lil and beyond: Formal languages for reward function specification in reinforcement learning. In Proceedings of the Twenty-Eight International Joint Conference Artificial Intelligence, IJCAI-19, pages 6065-6073. International Joint Conferences on Artificial Intelligence Organization, 2019.
[18] Grace E. Cho and Carl D. Meyer. Comparison of perturbation bounds for the stationary distribution of markov chain. Linear Algebra and its Applications, 137- 2001.
[19] Christoph Dann and Emma Brunskill, Sample complexity of episodic fixed- horizon reinforcement learning. Advances in Neural Information Processing Systems, 28, 2015.
10

---

[20] Xuchu Ding, Stephen L. Smith, Calin Belta, and Daniela Rus. Optimal control of markov decision processes with linear temporal logic constraints, IEEE Trunsactions Automatic Control, 595))1224--2277, May 2014.
[21] Alexey Dosovitskiy, German Ros, Felipe Codevilla, Antonio Lopez, and Vladlen Koltun. Carla: An open urban driving simulator. In Conference on robot learning, 2017.
[22] Ronan Fruit, Matteo Pirotta, and Alessandro Lazaric. Improved analysis of ucr12 with empirical bernstein inequality, arXiv preprint arXiv:2007.05456, 2020.
[23] Jie Fu and Ufuk Topeu, Probably approximately correct MDP learning and control with temporal logic constraints, Dieter Fox, Lydia E. Kavraki, and Hanna Kurniawati, editors, Robotics: Science and Systems X, University of California, Berkeley, USA, July 12-16, 2014, 2014.
[24] Mohammad Gheshlaghi Azar, Rémi Munos, and Hilbert J Kappen. Minimax pac bounds on the sample complexity of reinforcement learning with generative model. Machine learning, 91(3):325-34) -495,,4444000 2013.
[25] Ersst Moritz Hahn, Guangyuan Li, Sven Schewe, Andrea Turrini, and Lijun Zhang. Lazy probabilistic model checking without determinisation. arXiv preprint arXiv:1311.2928 2013.
[26] Mohammadhosein Hasanbeig, Alessandro Abate, and Daniel Kroening. Logically-constraing reinforce- ment learning, 2018.
[27] Thomas Hérault, Richard Lassaigne, Frédéric Magniette, and Sylvain Peyronnet. Approximate probabilistic model checking. In Bernhard Steffen and Giorgio Levi, editors, Verification, Model Checking, and Abstract Interpretation, page 73 84, Berlin, Heidelberg, 2004, Springer Berlin Heidelberg.
[28] Borja Ibarz, Jan Leike, Tobias Pohlen, Geoffrey Irving, Shane Legg, and Dario Amodei. Reward learning from human preferences and demonstrations in atari. Advances in neural information processing systems, 31, 2018.
[29] Thomas Jaksch, Ronald Ortner, and Peter Auer. Near-optimal regret bounds for reinforcement learning. Journal of Machine Learning Research, 1660))1563-1600 2010.
[30] Kishor Jothimurugan, Rajeev Alur, and Osbert Bastani. A composable specification language for reinforce- ment learning tasks. Advances in Neural Information Processing Systems, 32, 2019.
[31] Sham Kakade. On the sample complexity reinforcement learning. PhD thesis, Gatsby Computational Neuroscience Unit, University College London, 2003.
[32] Sham Kakade and John Langford. Approximately optimal approximate reinforcement learning. In In Proc. 19th International Conference on Machine Learning. Citeseer, 2002.
[33] Abbas Kazerouni, Mohammad Ghavamzzdeh, Yasin Abbasi Yadkori, and Benjamin Van Roy. Conservative contextual linear bandits. In I. Guyon, U. Von Luxburg, Bengio, H. Wallach, R. Fergus, S. Vishwanathan, and R. Garnett, editors, Advances in Neural Information Prucessing Systems, volume 30. 2017.
[34] Andrey Kolobov, Mausam, and Daniel S. Weld. A theory of goal-oridnted mdps with dead ends. In Proceedings of the Twenty-Eight Conference on Uncertainty in Artificial Intelligence, 12,'12, page 438-447, Arlington, Virginia, USA, 2012. AUAI Press.
[35] Jan Kietinský. Tobias Meggendorfer. and Salomon Sickert. Owl: library for w-words, automata, and Itl. In International Symposium on Automated Technology for Verification and Analysis, pages 543-550. Springer, 2018
[36] M. Kwiatkowska, G. Norman, and D. Parker. Prism 4.0: Verification of probabilistic real-time systems. In G. Gopalakrishnan and S. Qadeer, editors, Proc. 23rd International Conference on Computer Aided Verification (CAV'II), volume 6806 of LNCS, page 385-591. Springer, 2011.
[37] Richard Lassaigne and Sylvain Peyronnet. Probabilistic verification and approximation. Electron. Notes Theor. Comput. Sci., 143:101-114, jan 2006.
[38] Hoang M Le, Nan Jiang, Alckh Agarwal, Miro Dudík, Yisong Yue, and Hal Daumé III. Hicrarchical imitation and reinforcement leamnin. In International Conference on Machine Learning (ICML), Jul 2018.
[39] Hoang M Le, Cameron Voloshin, and Yisong Yue. Batch policy learning under constraints, In International Conference on Machine Learning (ICML),013)

---

[40] Gen Li, Yutng Wei, Yuejie Chi. Yuantao Gu, and Yuxin Chen. Breaking the sample size barrier in model-based reinforcement learning with generative model. Advances in neural information processing systems, 13:12861-12872. 2020.
[41] Michael L. Littman, Ufuk Topcu, Jie Fu, Charles Isbell, Min Wen, and James MacGlashan. Environment- independent task specifications via gitl, 2017.
[42] Andreas Maurer and Massimiliano Pontil. Empirical bernstein bounds and sample variance penalization, 2009.
[43] Sobhan Miryoosefi, Kianté Brantley, Hal Daume III, Miro Dudik, and Robert E Schapire. Reinforcement learning with convex constraints. Neural Information Prucessing Systems (NeurIPS), 2019.
[44] Andrew Y Ng. Daishi Harada, and Staart Russell. Policy invariance under reward transformations: Theory and application to reward shaping. In loml, volume 99, pages 278-287, 1999.
[45] lan Osband, Daniel Russo, and Benjamin Van Roy. (more) efficient reinforcement learning via posterior sampling. Advances in Neural Information Processing Systems, 26, 2013.
[46] Martin I. Puterman, Markov decision processes: discrete stochastic dynamic programming. John Wiley Sons, 2014.
[47] Guannan Qu and Adam Wierman. Finite-time analysis of asynchronous stochastic approximation and g-learning. In Conference on Learning Theary, 2020.
[48] Guannan Qu, Chenkai Yu, Steven Low, and Adam Wierman. Exploiting linear models for modcl-free nonlincar control: A provably convergent policy gradient approach. In 2021 60th IEEE Conference on Decision and Control (CDC), pages 6539-6546. IEEE, 2021.
[49] Jette Randløv and Prehen Alstrom. Learning to drive a bicycle using reinforcement learning and shaping.
In ICMI,, 1998.
[50] Dorsa Sadigh, Eric S. Kim, Samuel Coogan, S. Shankar Sastry, and Sanjit A. Seshia. A learning based approach to control synthesis of markov decision processes for linear temporal logic specifications. In 53rd IEEE Conference Decision and Control, pages 1091-1096, 2014.
[51] E. Seneta. Perturbation of the stationary distribution measured by ergodicity coefficients. Advances in Applied Probability, 20( 11:22822300, 1988.
[52] Salomon Sickert, Javier Esparza, Stefan Jaax, and Jan Křetúnský. Limit determisttiiiiit büchi automata for linear temporal logic. In Swarat Chaudhuri and Azadeh Farzan, editors, Computer Aided Verification, page 312-332, Cham, 2016. Springer International Publishing.
[53] David Silver, Satinder Singh, Doina Procup, and Richard S Sutton. Reward is enough. Artificial Intelligence, 199:10 2021.
[54] Jonathan Sorg. The Optimal Reward Problem: Designing Effectivv Reward for Bounded Agents. PhD thesis, University of Michigan, USA, 2011.
[55] Richard S. Sutton and Andrew G. Barto. Reinforcement Learning: An Introduction. The MIT Press, second edition, 2018
[56] R.S. Sutton, D. Precup. and S. Singh. Between MDPs and semi-MDPs: framework for temporal abstraction reinforcement learning. Artificial Intelligence, 112:181-211, 1999.
[57] Csaba Szepesvári. Algorithms for reinforcement learning. Synthesis lectures on artificial intelligence and machine learning, 4(1):11033, 2010.
[58] Jean Tarbouriech, Mattoo Pirotta, Michal Valko, and Alessandro Lazaric. Sample complexity bounds for stochastic shortest path with a generative model. In Proceedings of the 32nd International Conference on Algorithmic Learning Theory, Mar 2021.
[59] Jean Tarbouriech, Runlong Zhou, Simon Shaolei Du, Matteo Pirotta. Michal Valko, and Alessandro Lazaric. Stochastic shortest path: Minimax, parameter-free freee and towards horizon-free regret. In A. Beygelzimer, Y. Dauphin, P. Liang, and J. Wortman Vaughan, editors, Advances in Neural Information Processing Systems, 2021.
[60] Rodrigo Toro Iearte, Toryn Q Klassen, Richard Valenzano, and Sheila A. Mcllraith. Reward machines: Exploiting reward function structure in reinforcement learning. J. Artif. Int. Res., 73, may 2022.
12

---

[61] Marin Toromanoff, Emilie Wirbel, and Fabien Moutarde. Is deep reinforcement learning really superhuman atari? leveling the playing field. arXiv preprint wrXiv:198.004633 2019.
[62] John Tsitsiklis and Benjamin Van Roy. Analysis of temporal-diffferene learning with function approxima- tion. Advances in neural information processing systems, 9, 1996.
[63] Pashootan Vaezipoor, Andrew C. Li, Rodrigo Toro Icarte, and Sheila A. Mcllraith. Lulaactio: Generalizing LTL instructions for multi-task RL. In Proceedings of the 38th International Conference Machine Learning, ICML, volume 139 of Proceedings of Machine Learning Research, pages 19497-10500 2021.
[64] Eric M. Wolff, Ufuk Topeu, and Richard M. Murray, Robust control of uncertain markov decision processes temporal logic specifications. In 2012 IEEE 51st IEEE Conference on Decision and Control (CDC), pages 3372-3379. 2012.
[65] Yihong Wu and Pengkun Yang. Chebyshev polynomials, moment matching, and optimal estimation of the unseen. The Annals of Statistics, 47(2):857 883, 2019.
[66] Cambridge Yang, Michael Littman, and Michael Carbin. Reinforcement learning for general LTL objectives is intractable. CoRR, abs/2 12111.12679, 2021.
[67] Hákan L. Younes, Edmund M. Clarke, Paolo Zuliani. Statistical verification probabilistic properties with unbounded until. In Jim Davies, Leila Silva, and Adenilso Simao, editors, Formal Methods: Foundations and Applications, page 144-160, Berlin, Heidelberg. 2011. Springer Berlin Heidelberg.
[68] Baohe Zhang, Raghu Rajan, Luis Pineda, Nathan Lambert, André Biedenkapp. Kurtland Chua, Frank Hutter, and Roberto Calandra. On the importance of hyperparameter optimization for model-bases reinforcement learning. In International Conference Artificial Intelligence and Statistics, 2021.
13


Reviews:
[{"review_id": "pjpyfLBPhyF", "reviewer": "Reviewer_efrT", "summary": "Policy optimization in RL often involves complex reward engineering that can lead to unexpected results. Linear temporal logic (LTL), however, provides a robust language to encode a cost function where a scalar cost function may be unnatural. This paper provides a novel approach to LTL-constrained reinforcement learning, LTL constrained planning or LCP, under fewer assumptions and providing stronger guarantees than in the existing literature. The authors propose LCP based on a reduction to a reachability problem, and they show that the algorithm \"offers strong constraint satisfaction guarantees\", as well as prove its sample complexity. The algorithm itself consists of 3 parts: (1) finding an AMEC given the product MDP; (2) finding a cost-optimal recurrent policy within the AMECs; (3) finding a cost-optimal transient policy to reach this AMEC. Finally, the authors provide an empirical evaluation of their method on various environments, showing that their method achieves higher performance with lower sample complexity compared to baselines.", "questions": "I believe the paper, which is quite theoretical, could be improved with some discussion for practitioners, i.e. when to use LCP and when LCP would not offer extra benefit (apart from in truly infinite-horizon problems). In particular, the authors only present empirical evaluations in which LCP outperforms existing methods. Were there environments tested where LCP did not outperform existing baselines? LCP tends to give a larger advantage over baselines under which conditions (e.g. when the task is more complex)?", "limitations": "Limitation are discussed in Section 6, where authors describe how LCP may fall short when used alone in infinite-horizon problems.", "rating": 7, "confidence": 2, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Originality & Quality: To the best of my knowledge, the method LCP appears to be new, and well-situated in / compared to the existing literature. This work is complete, proposing a method and evaluating it against existing baselines. \n\nClarity: The submission is clearly written and well-organized. In particular, the inclusion of a section detailing the high-level intuition is very useful to orient the reader, as the work introduces a lot of terminology and is easy to get bogged down in e.g. the proofs in the appendices.  Ideally, I would have liked to see a conclusion that recaps the takeaways from this work and that lays down an avenue for future work, but perhaps this is just a matter of style.\n\nSignificance: This work provides a unique theoretical and experimental approach to policy optimization by reframing LTL constrained policy optimization as a reachability problem to recurrent states. ", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "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": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}, {"review_id": "nJXxHLlAz3n", "reviewer": "Reviewer_pGRX", "summary": "This paper presents a novel framework for reinforcement learning under hard LTL constraints. The proposed method, LCP, finds policies that primarily aim to satisfy the constraints over infinite horizons while secondarily minimizing a cost function (representing soft preferences). The method also relaxes many restrictive assumptions from prior works and is rigorously justified through theoretical analysis. Experiments on two RL domains help verify these claims and show the competitive performance of LCP compared to a prior method, LCRL. ", "questions": "- Often in Markov reward processes, only the recurrent cost rate is considered since the transient costs do not affect the long-term average cost. What's the motivation for including transient costs in the optimization objective? \n\n- (Minor issue with the framework): It's unclear to me that (OPT) is a well-defined optimization problem (with a solution $\\pi^*$ that is at least as good as any other solution). This is touched on by the in-text discussion of $\\eta$-greedy policies. If this is the case, then Corollary 5.2 is problematic since the result of the argmin wouldn't be defined.\n\n- In the PacMan domain, how would incorporating the food reward into the cost, rather than the LTL constraint, affect the performance of LCP? To my understanding, either objective could specify the same desired behaviour. ", "limitations": "The limitations were adequately addressed. ", "rating": 7, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 4, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "**Originality**: To my understanding, this work borrows ideas from the literature (e.g. the concept of MECs in model checking is widely known) but proposes an elegant and original approach derived from these concepts. This allows the authors to derive strong theoretical guarantees, and some of the key differences with respect to prior work are explained in the text. However, I admit there may be related work that I'm unaware of. \n\n**Quality**: \nThe authors propose a strong model-based approach, LCP, to the LTL-constrained policy optimization problem. This method is backed by rigorous theoretical analysis, though I was unable to verify all of the proofs (which are numerous, and quite dense). However, LCP is conceptually easy to understand and the claims appear reasonable. I have one minor issue with the framework, which I hope the authors can clarify in a question below. \n\nThe superior performance of LCP over a prior work, LCRL, are demonstrated on two domains, though I think the reasons for this need better explanation. The current claim that vanilla LCRL performs worse due to the \"extremely sparse\" cost function is dubious, as the cost function is uniform everywhere and virtually irrelevant in both domains. Overall, the experiments have a few other weaknesses:\n\n- The performance of LCP appears quite sensitive to specific LTL constraints, and should be evaluated on more than only two.\n- The cost function seems to play no role for LCP and vanilla LCRL in the current environments, reducing the problem to \"maximize the probability of satisfying the constraint.\" \n\n**Clarity**: Overall, the paper is very well-written except for the short experiments section, which delegates many important details to the Appendix. I would also appreciate if the authors could report the LBDAs and the MECs (or a brief description) for these domains so that reviewers can better understand how LCP handles these problems.\n\n**Significance**: This paper tackles the important problem of learning constraint-satisfying policies with guarantees. The authors frame this problem in a novel setting and provide an in-depth theoretical analysis which I believe will be useful to others in the field. The claims are backed by experiments, but as of now, their significance is unclear, in part due to missing details. \n\n\n\n", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "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": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}, {"review_id": "U4F36hEg-Tx", "reviewer": "Reviewer_Kr29", "summary": "The authors introduce a formal method for incorporating a probabilistic notion of LTL satisfaction for RL settings. They take the common approach to cross-product the statespace of the LTL's buchi automata for a combined reachable search space, and with the assumption of being able to sample any (s,a) pair on demand, propose a series of algorithms that separately treat the strongly connected components of the reachable states that infinitely achieve the goal condition (a requirement for infinite-trace LTL).\n\n## Revised Score\nRaised my evaluation after the authors teased apart the distinction to related work in the rebuttal.", "questions": "1. How might this work be modified to handle sample traces rather than arbitrary sampling of state-action pairs?\n2. How might any of this work be used in settings where the reachable state-space is unrealistic to enumerate? E.g., if $|AP|>100$", "limitations": "The limitation of being able to arbitrarily sample from the statespace seems kind of strong. Being able to reset is a fairly strong assumption, but being able to arbitrarily sample any $(s,a)$ pair is a very strong one. I feel similarly about the number of samples required (both theoretically and empirically) across the entire state space.\n\nThere is no immediate societal impact from this work, and the authors highlight this adequately.", "rating": 6, "confidence": 3, "soundness": 4, "presentation": 2, "contribution": 3, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "### Originality\nAs far as I'm aware, the approach to uniquely treat the SCCs of the merged state space (and the strategy to move between them) is unique. The only major issue I found with the originality is the absence comparison to much of the recent work on reward machines, LTL, etc, and how they can be used to control RL. It's unclear to me if these works come with the same assumptions highlighted in the other RL+LTL works cited in the paper. Some examples include:\n\n- Reward Machines: Exploiting Reward Function Structure in Reinforcement Learning\n- LTL2Action: Generalizing LTL Instructions for Multi-Task RL\n- LTL and Beyond: Formal Languages for Reward Function Specification in Reinforcement Learning\n- Using Reward Machines for High-Level Task Specification and Decomposition in Reinforcement Learning\n\n\n### Quality\nThe quality of the work appears to be of high caliber, but assessing it was difficult (more below).\n\n### Clarity\nThe paper is very dense -- it felt more like an extended abstract to a JMLR paper than a well rounded and self-contained conference submission. At times, entire paragraphs are just paraphrased sentences to results described and elaborated upon in the extensive supplementary work (e.g., paragraph just before section 6). The most difficult sections include:\n\n- Definitions 3.2 and 3.3\n- Definition 4.2\n- Lines 217 to 234\n\nThe general writing is extremely well done and free of grammatical / spelling issues. The only place caught my eye as a potential error is line 145 -- I think it should be $(E, A_E)$ and not $(E, A_{E'})$, and the $E \\subseteq E'$ should probably be $E \\subset E'$.\n\n### Significance\nWhile the results are strong, the significance is largely impacted by the small size of empirical domains and (ultimately) the sampling requirements for the approach to have any guarantees. It's unclear to me if these techniques can be applied in any reasonably sized RL setting (dozens to hundreds of atoms in a state).", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "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": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}]

Author rebuttal:

Decision: Accept