HypRL: Reinforcement Learning of Control Policies for Hyperproperties
Authors: Tzu-Han Hsu
Arshia Rafieioskouei
Borzoo Bonakdarpour
Venue: NeurIPS 2025 poster ()
Keywords: Reinforcement learning
formal methods
hyperproperties
temporal logics
specification-based RL
multi-agent RL
reward shaping
HyperLTL
MDP
Primary area: reinforcement_learning
TL;DR: A framework that synthesizes a tuple of optimal control policies for multi-agent systems that maximizes the probability of satisfying a desired hyperproperty.

Abstract: Reward shaping in multi-agent reinforcement learning (MARL) for complex tasks remains a significant challenge. Existing approaches often fail to find optimal solutions or cannot efficiently handle such tasks. We propose HypRL, a specification-guided reinforcement learning framework that learns control policies w.r.t. hyperproperties expressed in HyperLTL. Hyperproperties constitute a powerful formalism for specifying objectives and constraints over sets of execution traces across agents. To learn policies that maximize the satisfaction of a HyperLTL formula $\varphi$, we apply Skolemization to manage quantifier alternations and define quantitative robustness functions to shape rewards over execution traces of a Markov decision process with unknown transitions. A suitable RL algorithm is then used to learn policies that collectively maximize the expected reward and, consequently, increase the probability of satisfying $\varphi$. We evaluate HypRL on a diverse set of benchmarks, including safety-aware planning, Deep Sea Treasure, and the Post Correspondence Problem. We also compare with specification-driven baselines to demonstrate the effectiveness and efficiency of HypRL.

HypRL: Reinforcement Learning of Control Policies for Hyperproperties
Tzu-Han Hsu* Arshia Rafieioskouei"
Borzoo Bonakdarpour
Michigan State University
(tzuhan, rafieios, borzoo] Cmsu.edu
Abstract
Reward shaping multi-agent reinforcement learning (MARL) for complex tasks remains significant challenge. Existing approaches often fail to find optimal solu- tions or cannot efficiently handle such tasks. We propose HyPRL, a specification- guided reinforcement learning framework that learns control policies w.r.t. hyper- properties expressed in HyperLTL. Hyperproperties constitute a powerful formal- ism for specifying objectives and constraints over sets of execution traces across agents. To learn policies that maximize the satisfaction of HyperL.TL formula yo, we apply Skolemization manage quantifier alternations and define quantitative robustness functions to shape rewards over execution traces of a Markov decision process with unknown transitions. A suitable RL algorithm is then used to learn policies that collectively maximize the expected reward and, consequently, increase the probability of satisfying yp. We evaluate HYPRL diverse of benchmarks, including swaee planning, Deep Sea Treasure, and the Post Correspondence Problem. We also compare with specification-drivee baselines demonstrate the effectiveness and efficiency of HyPRL.
Introduction
Designing reward functions that accurately capture desirable behaviors in multi-agent reinforcement learning (MARL) remains notorious stumbling block. Consider wildfire scenario in x 3 grid- world with cells labeled (a, b....,i) i} (see Figure/ 1). Locations fi,f, c} are on fire, and two victims located {/ 9.. Now, two autonomous agents are deployed from {a} with two objectives; O the firefighter agent (FF) must extinguish all fire zones, and O2: the medical agent (Med) aims to rescue all victims. The agents also have satisfy within a 2-cell communication range, and C2: Med cannot pass any fire zone before FF extinguished the fire in that zone. The goal is to learn optimal policies for FF and Med that maximize the probability of satisfying all above requirements, as shown by the agent paths in Figure la.
constraints; C1: they must always remain
Now, suppose +50, rescue a victim: +10, agent out of range: - 100, and Med in fire zone: -100. These approaches
existing RL approach by assigning the following rewards; extinguish fire:
would guide FF to complete O optimally by path & _ 4 1h i, but due to C1 it forces Med to delay the rescue of the victim in {g} with redundant moves: S d 2 " d - g... (see Figure lb). Furthermore, the victim in { is trapped in fire, so satisfying O₂ depends on the progress of O₁, while respecting C₁ (safcty) and C22 (dependency). Such complex requirements make reward design in MARL particularly challenging. policies must account for both individual objectives and relational constraints between agents with dependencies. In fact, existing RL approaches often fail to find optimal policies because agent paths are implicitly universally quantified, which is overly restrictive and limits the ability of RL to explore more optimal solutions. That is, the set of requirements is of the form VT.VT'. tb where and T' are agents' paths and v specifies constrains and objectives.
Equaal contribution.
39th Conference on Neural Information Processing Systems (NcurIPS 2025).

---

1): FF extinguishes all fires.
(O2): Med rescues all victims.
)C FF and Med always stay
within 2-cells of each other.
(C2): Med must not passing any fire zone all time.
(a) Optimal policies. (b) Med paces in a d. (c) Med pauses in
Figure 1: A wildfire scenario with two objectives (O1, O2) and two relational constraints (C1, C2).
Temporal logics [37] have shown to be both expressive and effective to address objectives and constraints in single-agen settings [32, 24, 2, 10, 14, 21, 22, 28, 45,471, 47]. However, these methods cannot handle motivating example as it involves multiple agents. Recent works have been extended to MARL [33, 31, 20, 16]. but these approaches either fail to capture relational dependencies between agents can handle only subset of temporal properties, such as co-safty [29, 41]. Moreover, specifications in temporal logics that formalize the behavior of individual traces (e.g., LTL. are again inherently universally quantified and, hence, too restrictive.
In this paper, we propose a specification-guiéee RL framework that leverages the powerful framework of hyperproperties [12] and, in particular, the temporal logic HyperLTL [13], its formal foundation. Hyperproperties characterize requirements over sets execution traces, allowing the specification of relational and dependent behaviors that involve multiple agents or joint system executions, rather than individual behaviors of agents. This expressiveness is particularly well-suited for capturing relational, quantified, and multi-agent objectives. Building on this foundation, we propose Hyperproperties for Reinforcement Learning (HyPRL), a framework that learns a collection of control policies which maximizes the probability of satisfying hyperproperty expressed a HyperI.TI. formula. In motivating example, HyperL.TL allows a specification of the form Vr. _bb, which enables HyPRL to search for more optimal policies and identify the one in Figure 1a. The main challenge here is to deal with HyperLTL formulas with quantifier alternation, which has not been studied prior to HYPRL. Our work represents novel step towards the automated synthesis of reward mechanisms that capture complex objectives and constraints in multi-agent setting.
Contributions:
1. We formulate the control policies synthesis problem for a multi-agent system as a learning problem, where the goal is to maximize the probability of satisfying a HyperLTL formula that expresses a set of objectives and constraints (Section 4).
2. We address the challenge of reasoning about quantifier alternation in a HyperLTL formula due expressing dependencies among agents by Skolemization (Section 5.1).
3. We introduce quantitative semantics for HyperLTL that compute robustness values rewards, providing a solution of reward shaping for optimizing hyperproperty satisfaction (Section 5.2). Finally, use fff-the-shelf RL algorithms to learn optimal collection of policies (Section 5.3).
We evaluate HYPRL on diverse set of learning tasks, including safety-aware multi- objective planning, the Post Correspondence Problem, the famous Deep Sea Treasure benchmark, and the wildfire scenario. Our results show that HYPRL is more efficient and effective in handling complex requirements compared to selected baselines (Section 6).
2 Related Work
Logic-based Single-agent RL. DIRL [24] is framework that synthesizes an optimal policy which the specification is expressed in the language SPECTRL [23]. However, SPECTRL does not capture the full expressiveness of temporal logics as it only supports a fragment of LTL. In [32], the authors introduce truncated LTL for quantitative reasoning over LTL formulas, but is limited to single-agent task specifications (similar reasonings are also presented in [44, 2, 10]). In [28], LTL formulas are encoded by replacing operators and predicates with recurrent neural networks connected according to the parse tree, forming structure that captures the formula's semantics. In [14, 21, 45, 47, 30), the authors compose an MDP with a Limit Deterministic Büchi Automaton (LDBA),, which represents the LTL specification, and solve the compositional model control problem.

---

Logic-based Multi-Agent Reinforcement Learning. In [25], the authors extend the SPECTRL language [23] to con-cooperative multi-agent systems and train joint policies that form a Nash Equilibrium, which requires relational reasoning. However, their algorithm follows an "enumerate- approvch by exhaustively searching RL. policies to identify one that has higher probability to form such equilibrium, which leads to substantial learning overhead as the number of agents increases. Moreover, the extended language in [25] cannot handle arbitrary HyperLTL formulas. In [16], the authors propose reward shaping method by composing an MDP with a single centralized LDBA derived from a global LTL specification. However, this approach cannot capture inter-agent dependencies, and the product construction of LDBA may suffer from state- space explosion. More recent efforts in [33, 31, 20] extend quantitative reasoning to formulas with LTL operators in a multi-agent setting. However, in contrast to HYPRL, they only cover co-safety specifications and do not support the full logic.
Shield Synthesis. Shield synthesis for RL a technique that asks an agent to propose an action in each learning step, and a shield (i.c., safety guard) evaluates whether such action is safe [3. 26, 27]. In [34], the authors apply shield synthesis in a decentralized multi-agent setting, where the learning targets are specified by deterministic finite automata. However, the specifications are limited to universal (i.e., a 4" abb formula) and cannot handle properties such as planning tasks that involve dependencies (which is a A3 hyperproperty). Furthermore, the authors in [17] proposed factored shielding, which can learn multiple policies by a factorization of joint state space (i.e., decomposing one shield into multiple sub-shields). However, the main contribution is the improvement on RL scalability, but the limitation on universal-only properties remains.
3 Preliminaries
Markov Decision Processes (MDP). We model our RL problem for hyperproperties using MDP = (S, A, P. AP, L), where S is a finite set of states, 5 E S is the initial state, and A is a finite set of actions. The transition probability function P S x A x S [0, 1] assigns a probability to each transition, ensuring that for any state and action a, the sum of outgoing probabilities satisfies Eves P(s, 8') = 1. Additionally, AP denotes a finite set of atomic propositions, and I, S - 2AP is the labeling function. For example, Figure represents the MDP of Figure 1, where each state can be represented by (r,5) with x, y E (,, 1, labeled by {a, b,.,,;,, i}. and actions = {U, D, RR (i.e., four moving directions). A path in M is sequence Ç = _ $1 21 $2 "2, where s, S and a E A for all i 2 0. A sub-path (TEA) is
12.00
0.5
1:
11.00
0.5
10. 02
10.21
Figure 2: The MDP of The gorl-world in Figure 1.
segment se - ... au-1, 8k, for 0 < é < k < [c]. We write 2 and 2dd to denote the sets of all finite and infinite paths, respectively. A (deterministic) policy (fixed) action a E A. The trace & of path Ç is the sequence :: - + A maps each finite path where t(i)= = L(s)) for all i 2 O. Slightly abusing notation, we of labels Tr(() = ((0))())&())---
use Traces(2*) and Traces( (²4) to denote the sets of all finite and infinite traces, respectively.
Finite Semantics for HyperLTL. The syntax of HyperLTL [13] is given by the following grammar:
9 : Jr.p Vr.pp
$ : Pr I - sb V + O
t6b U vb,
where p E AP is an atomic proposition, a trace variable, and the second rule (for unquantified formulas) produces LTL formulas. The Boolean connectives and V have their standard mcanings, while O and l/ denote the "next" and "until" temporal operators, respectively. Other Boolean and temporal operators are derived as syntactic sugar: true - pr V -Pr, false - -true, 1b + e/s A -w/1 V 2/2 O 2/ e true t and v a - -vi, where 'O" and 'Lí are the eventually and always temporal operators. In a quantified formula, 3r means "along some trace 7", and V means "along all traces 7" We write Vars(pp) for the set of trace variables in formula y. A formula is closed if all E Vars(p) are quantified, with no variable quantified twice. Since RL algorithms operate finite samples, we adopt the finite semantics of HyperLTL [1]] over finite trace assignments, where a partial mapping II: : Vars(p) - -(2A)) assigns each E Vars(p) to a finite trace. Given II, trace variable T, and a finite trace E (2 we write [[[r + 1] for the assignment identical to II, except that is mapped to 1. We denote by Ho the empty trace assignment. For & E II, we refer to traces in the image of I1. Throughout this paper, we abbreviate tuples (II..... In) as (zi) An interpretation of
3

---

a HyperLTL formula yp = Q1...... Tn v. denoted by T= (E Varx(p))); is tuple of sets of traces, where we have one set T, per trace variable Tı, denoting the set of traces that can be assigned to Let Pr, be the distribution over set of paths induced by policy n, and we write Zr, D,, to denote a set of paths 2,, sampled from Drp such that n, the policy associated with the trace variable T4, for each i E (1..... ((r)((p)) (each trace variable ranges over the possible behaviors of an agent). We also define a family of sampled sets S = (Zr, ~ Da.)ief1,.... Vars(()) } >D,)) is the set of traces that T; can range over,
That is, for each 7, Vars(p), T. Traces which comes from the sampled paths from the associated policy π.. Abusing notation, we write Traces(S)) (S) as the tuple of sets of sampled traces. The satisfaction relation }= maps a formula y to model (T. IT, i), where i E Zz0 indicates the current evaluation position. Formally:
(T. II.0) = 3r. tb
there is t E Tr, such that (T, [[ - tl. () iff
(T. VT. V
iff
for all E Tr, such that [I[r t), 0) T
e
(T.
= Pr
iff
p E (T)
(T. = m
iff
(T, II. + 1b
(T, = $1 V 1
iff
(I, F 1 or (T, II. }= 2/2
(T. (1.) OΦ
iff
(T,11, - & and for all & 2
(T,
11 U 1/2
iff
there exists i with j < min such that (7, [1, T 122 and for all k E [(.J), (T, 1i
We say that an interpretation T satisfies HyperLTL formula yo, written T + if (T, Il. 0) - s. Likewise, a family of samples S (induced by each nG associated with each T; E Vars(p)). satisfies a sentence yo if (Traces(Z,, ~ (1.,,)e)) Example. The following HyperLTL formula captures the objectives and constraints of our mo- tivating example described in Figure 1, where 71 is the path for FF and T2 is the path for Med:
F yp.
Specification: iPeescue VTL. VTI.ar2-(VMm A M/aave A Visat A s/sate
O : Vitre A ((-))
C thatt A [(Locatioon, Location < <3)
O2: : V'ave e ((0r))
C2 sate - (-ing 4 in, (2 (f)) (-cr, cry)
For instance, the dependency constraint C2 for "Med cannot enter any fire zone until FF extinguished the fire in that zone" is expressed using the conjunction of temporal until operators. Notice that PReecue features V3 quantifier alternation, which increases the complexity of reasoning about hy- perproperties [8]. We emphasize that most RL approaches assume purely universal forms (i.e., V"), which cannot capture agent dependencies and often yield sub-optimal solutions. For instance, if FF ignores that Med must wait until the fire is extinguished to rescue victim, FF may follow its own optimal path that causes unnecessary delay for Med (see Figure Ic).
4 Problem Statement
Let us to denote optimality (e.g., x² denotes an optimal policy). The following optimization problem formulates policy synthesis as a learning problem.
Given an MDP M with unknown transitions and a HyperLTL formula of the form QITI.... Qu vh, our goal is to identify tuple of n policies (mi...., m;), such that:
(mi)ee E arg max P (Traces(Zr; ~ Dz,)) } x) (n.)
iEfl.....)
where Dry...., Dr., are the distributions over set of paths generated by policy spaces Ti...., Tn. That is, (Ti..... m maximizes the probability IP such that the generated tuple of sets of traces (Traces (Z,, ~ Dr,)..... Traces( ~ Dn,,)) from M satisfies s.
Example. Consider the MDP in Figure 2 and the following HyperI.TI. formula:
Pexp & Vr.Ery O ir A D dist(( v) (2. v)) <3)
Suppose agent FF with ni draws samples 2, IGF (EF) from the MDP:
CFF: (2. 8 (2
(2,2) (1.2) 4.2 (0.2)
FF 22 R
22 R (1.
(0.
4 (0.2)

---

Agent Med with policy draws 2rz
Meed Med):
Med (2 4 (1
(0.0)
(1,0) (1.0)
Med (2,0) 4 (2,1) 4 ببيا (1,2) + (م:2)
Notice that, the number of samples can be more than two. We now calculate the probability of satisfying yp using Zr, and 1rz (obtained by mi and πT2 follows:
Traces( (1GFF): 2x2)) F Seep
Traces 2-2)) F
Pexps
where "eed is the witness to T2 (existentially quantified) for both satisfaction relations. Hence, given 2 and 22, the probability of satisfying Sexp is evaluated as:
P mp) Traces((2r,) Zra)) F (Pep =
Now, if feep had the form AA, the evaluation has to over all combinations between 2n, and Z
Traces (races(((CFF)) (MMd))) of Sexx
Traces Traces(((GFF), (SMed))) (iled))))))) } Peepp
Traces Traces( ((C(p), ( (GM)d)) / 'Fexp
Traces((1<@F)) (MMdd))) } Pexp
Thus, the satisfaction probability of vv'v would be 0.5. This example demonstrates that the probability of satisfying a HyperLTL formula crucially depends on its quantifier structure.
5 Algorithmic Details of HYPRL
To solve the problem formally stated Section 3, our algorithm proceeds in the following three steps. We first Skolemize [40] to eliminate quantifier alternations and simplify the learning task. We then define quantitative semantics for HyperI.TL., converting satisfaction checking into robustness value optimization. Finally, we train a neural network using these robustness signals learn optimal policies that solve the original learning problem.
5.1 Step 1: HyperLTLL Skolemization
T2...., Let HyperLTL formula be of the form y Q.r... (T... Tn), where for 1 < I n, each Qr E (V. 3} quantifies a trace variable Te, and db is a quantifier-free LTL formula. We first Skolemize ş., producing Skolem(p)) to eliminate quantifier alternations. We define Qa {i Q 3} and Q = [j Qj V} the sets of existential and universal quantifier indices, respectively. For each i E Q² we denote Q7 (j <
i Qj V) the index set of all
universal quantifiers preceding Q;. A Skolem function for each E Q is defined as 7 + T, trace assignment II is consistent with f,,
and reduces constant function when Q ITT.,) T for all Q, and [(;;)) (I(,,,,)[(((T,, ... (T)o)))) for all Q², where Q = {ir < is ... < }. (1, = y for every trace assignment II consistent with all f,, then each f; is said to witness the satisfaction of [43]. For the inner LTL formula & (i.e., obtaining Skolem(") (v)). we replace each proposition Pr, with Pr. for all p E AP and i Q², thereby instantiating variables of the existentially quantified paths via their Skolem witnesses. In general, Skolemized of the following form:
Skolem(p)) 36 (T
Skolem(v)
each iEQU
for each jeQy
Based this transformation, we re-write the problem statement from Section 3 as follows. We first define the image of f,:
(f. ) (f. 1agg) ( ti, Traces(Zn,, ~ ~Dry): Q
That is. Ifg(f,) ( is the set of mapped traces (which r; for each E Q3 ranges over) from all possible preceding V-quantified Ti,, where each hyy is from its own sampled trace set Z Now, let us use
pa notation to ensure the collection of trace sets are ordered w.r.t. their path indices. Given two tuples of sets of traces T and Tz, define T DAI To (Traces( Z,, )uE(t..))) where each
5

---

p
Tr(Gea 1)
Pmin if Tr(See..)) and ((Tr(S(e:))); v) otherwise.
Tr(Gen) true)
Pmaz.
P
Tr(G
cc)
f(((se))
p
(r(GGe)) 76)
-p (T(((((e))))
(T(91a))
( ), if (k > f).
(T((91A))))
min (T((G()))))))
:E(e,A)
(Tr(S11)))) 040)
max pl (T((((i)))4)))
aEle.))
Tr(Gge:)) 4/1 v52)
min pf (Tr(C(e))) 111) (Tr)((((())))) 1/2))
Tr(Greu))) 1/1 122)
max (Tr(C(an)) 1/1 ( 2/22
(T((G()))) 1/2 11240 112)
max min (Tr((((u))) 1/2)) min p ((Tr(((aa))) jE(e,()
kE(t,k)
Figure 3: Quantitative semantics for LTL.
Traces either in Ti or Ta (and not both). Given MDP M and HyperLTL specification yp of the form and (2) a tuple of policies jTT), such that:
Tx-
Tu v. our goal is to compute (1) a tuple of Skolem witnesses (f))equ
(TT))EQ
arg max P/ (Img(f.)) xe (Traces(Zr, Day)) Skolem(p)) (xg))
iEQUajjEYy
That is, the tuple of policies (xz) maximizes the probability that the ordered collection (1) the generated traces of all universal quantifiers (Traces(Z,, ~ 2) and (2) the sets of mapped traces (i.c., the image) of each Skolem witness for all existential quantifiers (Img(f.))eeq= together satisfies Skolem(p)) Notice that in the updated problem statement, we compute policies only for universally quantified traces, while Skolem functions learned for existentially quantified traces to witness the optimality.
5.2 Step 2: Policy Learning with Quantitative Semantics
To transform the satisfaction checking problem (i.e., determining }-) into an optimization task, define quantitative semantics for HyperLTL, extended from [32]. In particular, we evaluate the Skolemized HyperLTT formula Skolem(pp) over tuples of sampled paths (Ci, . ... from M.
Robustness for a Single Trace. Let R. be the set of real numbers and V/ the set of all LTL formulas. We define a valuation function f: 2AP -> R that assigns real value to a set atomic propositions, provided as part of the input. Given a state
5 of an MDP M, the quantitative semantics are defined over predicates in the form of f (L(s)) < c, where is a user-specified threshold. Next, we define robusiness function p:: Traces (*) V IR that assigns robustness value finite trace for an LTL formula. Intuitively, the robustness value evaluates "how far" the given finite trace is from satisfying db The complete quantitative semantics shown Figure 3. We use constants Pmez and Priin for the maximum and minimum robustness values, respectively. Given a trace, higher p value implies the trace has higher robustness to satisfy v/. and lower p value means the trace is less likely to satisfy & (e.g.. a potential violation).
Formally, given LTL formula & and an MDP M,, path with higher robustness value indicates that it has higher probability to satisfy tb. The optimization task of seeking a single policy x² is:
[p (((Tr(Goo)) v) A Pmar C~D,
E arg max
Here, for simplicity, we use the notation to represent convergence. That is, at" maximizes the probability of satisfying y over the distribution of paths generated by policy
Robustness for Tuple of Traces. To evaluate the robustness value over multiple traces, we first define zip function that pointwise bundles tuple of traces. Given a tuple of finite traces (f.....,4, (,).
we derive a zipped trace zip((h, .h.....,, (.)) and for 2 0, zip( (i) & (4), ...,,,,40 (i)). Given LTL formula, tuple of paths (G1, C2.... ..., Sn) has higher probability of satisfying & if the

---

robustness value of zip( ((r (o:kk) ), Tr(Gejossa))..... (r((n(o: converges to Pmoz w.I.t. & for some .i,.... kin, where 0 S k
S Gel for each 1 I l S n. Thus, the optimization task of computing a tuple of policies { m2. n that maximizes the robustness becomes:
(mE)eE(L....))) E arg max P ( ((T(((((T)))) ~ Da,))), 16) A Pmaz
(m))
(E(I.....))
This formulation reflects that LTL formulas are implicitly universally quantified as we emphasized in Section 1. For instance, model checking v"' .a reduces checking V.O via self-composition [5, 8].
Robustness for Skolemized HyperLTL. Optimizing an alternating HyperLTL formula requires that policies for universally quantified paths simultaneously optimize the existentially quantified paths. In order to preserve ordering, we use Ug to make sure the union of trace tuples are in order w.r.t. their path indices. That is, given two tuple of traces (-)1 and (-)2, we define (+)1U=(-) & (Zr(G=))=eEL1-. (1.m)) where each Tr((.) is either from (-) or (-)2. Given a Skolemized HyperLTL formula, the inner LTL formula is denoted as Skolem (b), as defined in (1). For each i Q" and j e Q", we say a tuple of paths (S1, C2. Gn) satisfies up if and only if:
[o( (zzip(( ((i(((T((G)): Ug (Tr (Tr(S) Skolemm(()))) LEQa JEEY
4 Pmar
Essentially, the set ( (T((G)0::=)))))00 captures the tuple of traces produced by each Skolem function for each existential quantifiers (i.e., trace from (mg(f.) for each i E Q²). while (o: corresponds to the tuple of traces for j E QV. That is, we can formalize the optimization task for Skolemized HyperLTL as follows:
(xt) (xf) e arg max P ( ~ DT.)) (T((S)jo)) ~ P>,)))), (m)))g(m)))
Skolem( + Pmazz
(2)
jEQa
Notice that, for each E Q² (i.e., a Skolem function), the evaluation of dependes on whether the sampled trace Si ~ Dr, serves as a witness for its preceding (Gi)), That is, p(f,, v)) & (T((()),, Tr(S.. uz )), )) e)) Hence, the optimization of (τī) depends on (mz), which is nec- essary to capture the semantics of a HyperL.TL formula with quantifier alternation (we provide a comprehensive example in Appendix C). Finally, we show that the set of optimal policies obtained by (2) also solves the original optimization problem in Section (detailed proof in Appendix A).
Theorem 1 Given an MDP M and a HyperLTL formula ip an optimal tuple of policies (xt) keqaUs (mj)) for Skolem(pp) is also optimal tuple of policies for ip, that optimizes the probability of satisfying sp in M (the problem statement in Section 3).
5.3 Step 3: Reinforcement Learning for HyperLTL
Now, we solve the optimization task in (2) using RL, where the reward signal is defined by the robustness values from Section 5.2. As our MDP model lacks a built-in reward function, we use robustness values to guide learning. To avoid confusion with standard RL terminology, we refer to expected robustness value when mentioning expected rewards. For simplicity, we assume all sampled paths have equal length.
Optimizing Expected Reward. The goal of this step is to learn an optimal neural network ^ a parameterized compositional function that synthesizes the policies solving (2). The construction of learning constraints is inspired by the well-known Bellmun Equation [4], which characterizes the optimal expected reward of decision process as a recursive function of immediate reward and the value of future states. Let us use S to denoted the state of zipped path at position & (i.e.,
Sk zip(( (k)). We define the immediate reward for state-action pair (sk, az) based on the robustness value the zipped trace from (2):
R(s,. ax) A [0(iig (rip((Tr(GGoox))) (Tr( (o0s)) ))), Skolsm (1)) JEQ"
7

---

Agents
Envirunment
Table 1: HyperLTL specifications of case studies,
{S ... Sn)
Samples
MDP M
(SRL) 3r.. : M..) (cr Vyy) (1t,,, (Koi-pai) (ites Mra) (Paz, Me21)
Rebustmess values
Robustness function
(DST) Vra. OTTI, A OiT2, A ((3,)...11 .1AA (mp,, 8) (pper, por. <1)
Next episode
p .. (p)
3ry.arg Vioraaaccy (slexond. A A (Punn paee,
palr
Skolem (
[ (prpp, prsess) (Hern, #mt..)
PCCP)
HyperLTL
Skolemization
A (ppop, to piss (Penrr to paser D]] u ((thwrr, V thee A bothhure A (-threenn)) D)
Formula instramennaaton
Figure 4: Overview of HYPRL.
The expected reward E(sk. (g follows the classic Bellman formulation, combining immediate reward and future reward based on some discount factor (see Appendix B for details). Intuitively, IE( ds) quantifies the long-term utility of taking action dg at state 8д- Finally, for any arbitrary state 8 and action a, the Bellman Equation then defines the Q-value recursively for each (s, a) E S x A, denoted as QNN (s, a):
(3, A EP(s,,, a(s,a)) +7 Σ NN [P(ssaao(((sss
s'ES
a'EA
where (N((a | s') indicates that NN takes action a' on state s'. Consequently, the optimal action-value function for each (s, a) is:
QNN (s, A max QuNiss, a)
NN
Intuitively, Q-NN' (s, a) captures the maximum expected reward achievable from a state & by taking action a. We remark that, framework samples all paths for each quantifier simultaneously. That is, the learned neural network N\* induces a set of n functions (NNT. ... .NN n.. where (ors(()) and for all 1 l S n, N maps state to an optimal actions for path Çe.
Constructing Policies. Based on the learned N we now construct the tuple of policies (m NEE and (xg) that solves (2) for each k-step ranging over the sample size as follows. For each j Q7, we inductively construct the policies:
ス (Si & (sN
For each E Q3, construct Skolem witness follows:
x (Sssjuss) A NN: (f, (Tr(Si, jo.g)..... Tr(S (o.i))))
That is, the optimal policy for finite prefix Ç with E Q² depends on the optimal actions taken along the preceding universal paths .i..... 10 illustrating how our framework captures the dependency of an existential path on the universally quantified ones. To this end, from the learned neural network NN* succesfully derive two tuples (T])ieq) and (nt) for Equation (2).
Theorem 2 Given an MDP M and a HyperL.L formula s. the optimal neural network function NN* derives tuple of Skolem function witnesses (fe) and tuple of optimal policies (xz JEoy that optimize the satisfaction of (kolemmpp).
Theorem 2 gives the premise of Theorem 1, which, in turn, solves the original problem stated in Section 3 (detailed proof in Appendix A).
Implementation and Experiments
HYPRL fully implemented (see Figure 4). Given a Hyperl.TI. formula yo with n quantifiers, HYPRI. first constructs its Skolemized form Skolem(pp), prescribed in Section 5. Next, at cach step
8

---

Table 2: Descriptions of the case studies.
Safe RL in Grid Worlds (SRI.)
Two agents collaboratively learn policies. (st m2) to reach their respective goals while avoiding collisions in a grid world.
Two agents (a driver and a treasure collector) navigate among treasures.
Deep Sea Treasure (DST)
Learn policies (ai mz) such that, for all ways the collector maximizes treasures, safe route exists for the driver to exit within the time limit
Pust Correspondence Problem (PCP)
Learn policies (#i, #2) for PCP: for any semi-matching sequence of dominos, there exists an extension into full matches.
for each E (1,..., n), a policy m, observes finite path Gijo.e) and selects an action nT (G((o()))) yielding updated path (i The environment computes feedback using robustness function p to guide learning (Section 5.2). The optimal tuple of policies (* f-.,...; m are learned iteratively using a selected RI. algorithm such as DQN [36], PPO [39], or CQ-Learning [15] (Section 5.3). We summarize all our case studies and their corresponding HyperLTL specifications in Table and Table 1, respectively. We also investigate the wildfire scenario introduced in Section I with larger
grid-worlds, All experiments are ran on an Apple MI Max (10-core CPU, 24-core GPU), Additional details of experimental setups are provided in Appendix D.
Baseline. We experiment all cases using the setup from [32] by comparing against manually designed reward functions, To ensure fair comparison, for DST, we use the reward function from [42]; for the rest of the cases, we construct several reward functions and report the best- performing one (details are provided in Appendix
D). For SRL, we also compare with the method called "shield synthesis" [17], where a pre-synthesized shield enforces a safety property during learning and, in this specific case, can reason about inter-agent dependencies.
Results and Analysis. First, for SRL, we use the maps from [35] and compare CQ- lyaR against shield synthesis [17] (detailed map descriptions are inAppendix D). It is worth noting that for [17], shield has to be explicitly designed to avoid unsafe states, whereas HYPRL achieves better safe and goal-directed behavior purely through the robustness values derived from HyperLTL formula. Our analysis for SRL is presented in Table 3. In two-agent setting, the result shows that the policies learned by HyPRL outperform the shielded agent in all of the environments by requiring fewer steps to reach the goal, except in SUNY, where their performance is quite similar. Furthermore, in both SUNY and MIT maps, HYPRI. successfully avoids collisions as what we replicated from [17]. In three-agent setting (where the HTp formula is expanded to VEA), the shielding method successfully avoids all collisions; however, it failed to reach the goals within the bound of 100 steps in ISR, Pentagon, and MIT. In contrast, HYPRL was able to guide the agents to reach their goals significantly faster than both baselines and achieved fewer collisions compared to CQ-learning. We emphasize that although shield synthesis can avoid collision in all cases, it comes with the cost of spending a significant number of steps to reach the goal. In contrast, HyPRL maintains low collision rates in ISR and Pentagon, and learns policies that reach the goal with substantially fewer steps in ISR, Pentagon, and MIT maps.
Second, for SRL,, we compare DQN+HYPRL with DQN and present the results in Figure 6. The top four figures demonstrate that HYPRL always achieves higher number of successful goal completions under the same number of learning episodes. The bottom four figures show that HyPRL requires fewer episodes to learn collision avoidance.
For DST, we compare PPO+HYPRL with PPO, and DQN+HYPRL with DQN, using the reward functions from [42] in both cases. We evaluate using two metries: (1) the total amount of collected treasures E and (2) the average amount of collected treasures per step (Σ: /ssteps. As shown
Table 3: SRL, avg. and std. error of 10 evaluations after Ik training episodes, 10 runs, where S/B stands for step-bound which is 100 steps for all cases.
CQ
CQ + Shield [17]
CQ + HyPRL
Maps
No. Agents
Steps
Collisions
Steps
Collisions
Steps
Collisions
ISR
27.95
0.19=0.1
17.40=2.2
0.00=0.0
7.58=20.3
0.25
Pentagon
36.46+77.7
0.28=0011
15.20+
0.00=0.0
11.90++4.6
0.53++0.5
SUNY
2
01.99+0.55
0.01+000
11.50+0.3
0.00-0.0
12.48+0.6
0.00+0.00
MIT
48.28
0.20:10.1
33.46:13.4
0.00
23.20.10.5
0.00.10.0
ISR
98.79=0.8
12.68+338
S/B
0.00=0.0
74.18+-5.1
7.78+
Pentagon
97.15 2.4
16.46+7.2
S/B
0.00=000
7.7
10.92+1 1.4
SUNY
3
84.8917.9
0.63.10.2
82.35.14.1
0.00
44.95.18.3
0.71
MIT
96.9611..
2.83.11.3
S/B
0.00=0..0
71.5317.7
1.5820.7

---

Tolal Koooh
150
150
160
1000
100
153
50
100
100
200
100
200
100
200
150
300
ligioodes (ISR)
Epplodes (PENTAGON)
Eppoodes (SUNT)
Igloxdes (MFT)
10
10
5
100
200
100
200
100
200
0
150
300
Egtindes
Episndes PPENTAGON)
(SUNY)
Egisodas
Figure SRL results, avg. and std. error of total number of goal completions by 2 agents (top) and collisions (bottom). DQN+HYPRL (line -) and DQN (line
) over 10 runs.
Table 5: Wildfire results, avg. and std.
Table 4: DST results, avg. and std. error over 10 evalua- error of 10 trials after 5k episodes, 10 runs.
tions across, 10 runs, and Epi. stands for "Episodes".
Sow Method
Dret
Steps O.
Stepe
3² PRO
2.5
S14S66.1 1899021.1
76708851
Mohval
Epi.
E
Mathed
Ep-.
3 ag Atops
PPO HLRRL
2.90-4..03
143590:1.
PRO
4.11:12
01120004
DON
100402
PIO
422000
S/8
P HYOKL
500
2293622
0902000
DON HURL
4124144
03420000
HYRRI.
59.50=11.5
8057.8-111.1
PPO
1000
3:33008
011240000
DON
L45802
000200000
PIO
11.2-005
10001 N4:264
S08
PPO HVPRI.
1000
2.3
112
DON HYPRI.
1050
4.43-088
0.21-0003
PPO HYVRRI
6.94-007
41498811448 FAN
3962-8005
10P
PPO HYRRI
109:0001
5.3:0.10
312928:5599.0
520335222
in Table 4, policies learned by HYPRL outperform those learned by the baseline, regardless of the number of training episodes the choice of the RL algorithm.
Finding policies to solve the PCP problem is inherently chal-
DIGN+RVVRRLL 12- 66) DON
Rof match
lenging due to its undecidability. HYPRL is able to learn op- timal policies that solve PCP more efficient, compare to the
200
baseline. Figure 5 presents the performance comparison of DQN+HyPRL with DQN, showing that HyPRL achieves more successful matches in both 5- and 6-domino settings.
200
Lastly, we evaluate HYPRL on the wildfire scenario and com- pare PPO+HYPRL with PPO. As shown in Table 5, even when scaling up the grid-world environment from 32 to 52, 82, and
Eploades
PCP results, avg. and std. error of total matches, 10 runs. 10a, HYPRL consistently outperforms the baseline by requiring fewer steps to rescue victims, extin- guish all fires, and maintain a safe distance between the two agents. The step-bounds are set to 10k steps for the 32 and 52 environments. 20k steps for 82, and 30k steps for 102. In fact, PPO fails to learn policies capable of rescuing victims (02) within the step-bounds for 52 and 8?, and is unable to extinguish all fires (O₂) within the step-bound in the 10 setting.
Figure 5:
7 Conclusion
We introduced HYPRL, reinforcement learning framework that synthesizes control policies for tasks specified as HyperL.TI formulas over MDPs with unknown transitions. By leveraging the expressiveness of hyperproperties, HYPRI. can handle complex multi-agent objectives and relational constraints, including safe planning and undecidable problems like PCP. Our quantitative semantics automatically derives robustness values from the specification and learns control policies that maxi- mize the probability of satisfying the given HyperLTL property. Implemented with off-the-shelf RL comparable baselines across set of
algorithms, HyPRL demonstrates superior performance diverse case studies, especially in scenarios where reward shaping is non-trivial.
L Limitations. HyPRL currently does support fully decentralized control policies, where each agent lears its local policy without access to global observations and rewards. Second, it is possible that environment states are not fully observable. That is, instead of an MDP. the environment is a partially observable MDP (POMDP). We believe these limitations open up exciting future work and can be addressed by extending HYPRL.
Societal impacts. This work marks significant step towards extending MARL to complex tasks with relational requirements. By enabling the learning of policies under interdependent objectives, our approach broadens the applicability of MARL to critical domains such as disaster response, swarm drones, smart home automation, and industrial resource management, where coordination among agents is essential for success.
10

---

References
[1] Alekh Agarwal, Nan Jiang, Sham Kakade, and Wen Sun. Reinforcement learning: Theory and algorithms. CS Dept., UW Seattle, Seattle, WA, USA, Tech. Rep, 32:96, 2019.
[2] Derya Aksaray, Austin Jones, Zhaodan Kong, Mac Schwager, and Calin Belta. Q-learning for robust satisfaction of signal temporal logic specifications. In 2016 IEEE 55th Conference on Decision and Control (CDC), pages 6565-6570. IEFF, 2016.
[3] Mohammed Alshiekh, Roderick Bloem, Rüdiger Ehlers, Bettina Könighofer, Scott Niekum, and Ufuk Topcu. Safe reinforcement learning via shielding. In Proceedings of the AAAI conference on artificial intelligence, volume 32, 2018.
[4] EN Barron and H Ishii. The bellman equation for minimizing the maximum cost. NONLINEAR ANAL THEORY METHODS APPLIC., 13(9):1067-1090 1989.
[5] Gilles Barthe, Pedro R D' argenio, and Tamara Rezk. Secure information flow by self- composition. Mathematical Structures in Computer Science, 21(6):107--122,, 2011.
[6] Richard Bellman. On the theory of dynamic programming. Proceedings of the national Academy of Sciences, 38(8)7716-71,, 1952.
[7] Raven Beutner and Bernd Finkbeiner. Hyperad logic for hyperproperties in multi-agent systems. Logical Methods in Computer Science, Volume 19, Issue 2:13, May 2023, ISSN 1860-5974.
[8] B. Bonakdarpour and B. Finkbeiner. The complexity of monitoring hyperproperties. In Proceedings of the 31st IEEE Computer Security Foundations Symposium CSF, pages 162-174, 2018.
[9] B. Bonakdarpour and S. Sheinvald. Finite-word hyperlanguages. Information and Computation, 295: 104944, 2023.
[10] Ronen Brafman, Giuseppe De Giacomo, and Fabio Patrizi. Ltff/ldf non-markovian rewards. In Proceedings of the AAAI conference artificial intelligence, volume 32, 2018.
[11] N. Brett, U. Siddique, and B. Bonakdarpour. Rewriting dewriting-based based runtime verification for alternation- free HyperLTL. In Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 77-93, 2017.
[12] M. R. Clarkson and F. B. Schneider. Hyperproperties. Journal of Computer Security, 18(6): 1157-1210, 2010.
[13] M. R. Clarkson, B. Finkbeiner, M. Koleini, K. K. Micinski, M. N. Rabe, and C. Sánchez. Temporal logics for hyperproperties. In Proceedings of the 3rd Conference on Principles of Security and Trust POST, pages 265-284, 2014.
[14] Giuseppe De Giacomo, Luca Iocchi, Marco Favorito, and Fabio Patrizi. Foundations for restraining bolts: Reinforcement learning with ltf//dlff restraining specifications. In Proceedings of the international conference on automated planning and scheduling, volume 29, pages 128-136,70 2019.
(15) Yann-Michael De Hauwere, Peter Vrancx, and Ann Nowé. Learning multi-agent state space representations. In Proceedings of the 9th International Conference on Autonomous Agents and Multiagent Systems: Volume 1 Volume 1, AAMAS 100 page 715-722, Richland, SC, 2010. In- ternational Foundation for Autonomous Agents and Multiagent Systems. ISBN 9780982657
[16] Ingy FlSayed-Aly and Lu Feng. Logic-based reward shaping for multi-agent reinforcement learning, 2022.
[17] Ingy ElSayed-Aly, Suda Bharadwaj. Christopher Amato, Rüdiger Ehlers, Ufuk Topcu, and Lu Feng. Safe multi-agent reinforcement learning via shielding. In Proceedings of the 20th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS '21 page 483-491, Richland, SC, 2021. International Foundation for Autonomous Agents and Multiagent Systems. ISBN 978 450383077.

---

[18] Ky Fan. Minimax theorems. Proceedings of the National Academy of Sciences, 39(1):42-4) 47, 1953.
[19] B. Finkbeiner and C. Hahn. Deciding hyperproperties. In Proceedings of the 27th International Conference Concurrency Theory (CONCUR), pages 13:1-13:14, 2016.
[20] Lewis Hammond, Alessandro Abate, Julian Gutierrez, and Michael Wooldridge. Multi-agent reinforcement learning with temporal logic specifications, 2021.
[21] Mohammadhosein Hasanbeig. Alessandro Abate, and Daniel Kroening. Logically-constrained reinforcement learning. arXiv preprint arXiv: Perxivv:800.... 000011001.0999 2018.
[22] Mohammadhosein Hasanbeig, Yiannis Kantaros, Alessandro Abate, Daniel Kroening, George J Pappas, and Insup Lee. Reinforcement learning for temporal logic control synthesis with probabilistic satisfaction guarantees. In 2019 IEEE 58th conference on decision and control (CDC), pages 5338-5343. IEEE, 2019.
[23] Kishor Jothimurugan, Rajeev Alur, and Osbert Bastani. A composable specification language for reinforcement learning tasks. Advances in Neural Information Processing Systems, 32, 2019.
[24] Kishor Jothimurugan, Suguman Bansal, Osbert Bastani, and Rajeev Alur. Compositional reinforcement learning from logical specifications. Advances in Neural Information Processing Systems, 34: 10026-0000, 2021.
[25] Kishor Jothimurugan, Suguman Bansal, Osbert Bastani, and Rajeev Alur. Specification guided learning of nash equilibria with high social welfare. In International Conference on Computer Aided Verification, pages 343-363. Springer, 2022.
[26] Bettina Könighofer, Florian Lorber, Nils Jansen, and Roderick Bloem. Shield synthesis for reinforcement learning. In Leveraging Applications of Formal Methods, Verification and Verification Principles: 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part I pages 290-306. Springer, 2020.
Validation:
[27] Bettina Könighofer, Julian Rudolf, Alexander Palmisano, Martin Tappler, and Roderick Bloem. Online shielding for reinforcement learning. Innovations in Systems and Software Engineering, 19(4):379-394, 2023.
[28] Yen-Ling Kuo, Boris Katz, and Andrei Barbu. Encoding formulas as deep networks: Rein- forcement learning for zero-shot execution of Itl formulas. In 2020 JEEE/RSI International Conference on Intelligent Robots and Systems (IROS), pages 5604-5610. IEEE, 2020.
[29] Orna Kupferman and Moshe Y. Vardi. Model checking of safety properties. In International Conference on Computer Aided Verificution, CAV 1999, 1999.
[30] Xuan-Bach Le, Dominík Wagner, Leon Witzman, Alexander Rabinovich, and Luke Ong. Reinforcement learning with LTL and Slomegaß-regee regullr objectives via cetimality--reservii translation to average rewards. In The Thirty-eighth Anmual Conference on Neural Information Processing Systems, 2024.
[31] Borja G. León and Francesco Belardinelli. Extended markov games learn multiple tasks in multi-agent reinforcement learning, 2020.
[32] Xiao Li, Cristian-loan Vasile, and Calin Belta. Reinforcement learning with temporal logic rewards. In 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pages 3834-3839, IEEE, 2017.
[33] Chanjuan Liu, Jinmiao Cong, Bingcai Chen, Yaochu Jin, and Enqiang Zhu. Guiding multi- multi-task reinforcement learning by a hierarchical framework with logical reward shaping, 2024.
[34] Daniel Melcer, Christopher Amato, and Stavros Tripakis. Shield decentralization for safe multi-agent reinforcement learning. Advances Neural Information Processing Systems, 35: 13367- 2022.
12

---

[35] Francisco S. Melo and Manuela Veloso. Learning of coordination: exploiting sparse interactions in multiagent systems. In Proceedings of The 8th International Conference on Autonomous A Agents and Multiagent Systems- Volume 2, AAMAS '09, page 773-780, Richland, SC, 2009. In- ternational Foundation for Autonomous Agents and Multiagent Systems. ISBN 97809817381 78.
[36] Volodymyr Mnih, Koray Kavukcuoglu, David Silver, Andrei A. Rusu, Joel Veness, Marc G. Bellemare, Alex Graves, Martin Riedmiller, Andreas K. Fidjeland, Georg Ostrovski, Stig Pe- tersen, Charles Beattie, Amir Sadik, Ioannis Antonoglou, Helen King, Dharshan Kumaran, Daan Wierstra, Shane Legg, and Demis Hassabis. Numan-level control through deep reinforcement learning. Nature, 51 518(7540):529-533 February 2015. ISSN 1476-4687.
[37] A. Pnueli. The temporal logic of programs. In Symposium on Foundations of Computer Science (FOCS), pages 46-57, 1977.
[38] Antonin Rafrin, Ashley Hill, Adam Gleave, Anssi Kanervisto, Maximilian Emestus, and Noah Dormann. Stable- baselines:: Reliable reinforcement learning implementations. Journal of Machine Learning Research, 22(268):1-8, 2021.
[39] John Schulman, Filip Wolski, Prafulla Dhariwal, Alec Radford, and Oleg Klimov. Proximal policy optimization algorithms, 2017.
[40] Thoralf Skolem. boggich-kkombnntoriicee untersuchungen über die erfüllbarkeit oder beweis- barkeit mathematischer sätze nebst einem theoreme über dichte mengen. Videnssapsselskapets Skrifter, I.
Klasse, 1920.
[41] Wolfgang Thomas. Safety-and liveness-properttes in propositional temporal logic: characteriza- tions and decidability. Banach Center Publications, 21(1):403-417, 1988.
[42] Peter Vamplew, Richard Dazeley, Adam Berry, Rustam Issabekov, and Evan Dekker. Empirical evaluation methods for multiobjective reinforcement learning algorithms. Machine Learning, 84(1):51-80, 2011.
[43] S. Winter and M. Zimmermann. Tracy, traces, and transducers: Computable counterexamples and explanations for hyperitl model-checking. 2024.
[44] Z. Xu, Y. Rawat, Y. Wong, M. S. Kankanhalli, and M. Shah. Don't pour cereal into coffee: Dif- ferentiable temporal logic for temporal action segmentation. In Advances in Neural Information Processing Systems, volume 35, pages 14890-14903, 2022.
[45] Zhe Xu and Ufuk Topcu. Transfer of temporal logic formulas in reinforcement learning. In IJCAI: proceedings of the conference, volume 28, page 4010. NIH Public Access, 2019.
[46] Runzhe Yang, Xingyuan Sun, and Karthik Narasimhan. A generalized algorithm for multi- objective reinforcement learning and policy adaptation. In H. Wallach, H. Larochelle, A. Beygelzimer, d'Alché-Buts Buc, E. Fox, and R. Garnett, editors, Advances in Neural In- formation Processing Systems, volume 32. Curran Associates, Inc., 2019.
[47] Lim Zun Yuan, Mohammadhosein Hasanbeig, Alessandro Abate, and Daniel Kroening, Modular deep reinforcement learning with temporal logic specifications. arXiv e-prints, pages arXiv- 1909, 2019.
13

---

NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification: The paper successfully makes the four contributions as we stated explicitly in the abstract and the introduction.
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made the paper.
The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A No or
NA answer to this question will not be perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings.
is fine to include aspirational goals as motivation as long as is clear that these goals not attained by the paper.
2. Limitations
Question:
Does the paper discuss the limitations the work performed by the authors?
Answer: [Yes]
Justification: Yes, elaborate the limitation in Section 7.
Guidelines:
The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors are encouraged to create a separate "Limitations" section their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g., independence assumptions, noiseless settings, model sell-specification, asymptotic approximations only holding locally). The authors should reflect how these assumptions might be violated in practice and what the implications would be.
The authors should reflect on the scope of the claims made, e.g., if the approach was only tested on few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect on the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution is low images are taken in low lighting. Or speech-to-text system might not be used reliably to provide closed captions for online lectures because it fails to handle technical jargon.
The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairness.
While the authors might fear that complete honesty about limitations might used by reviewers as grounds for rejection, worse outcome might be that reviewers discover limitations that aren't 't acknowledged judgment and recognize that individual actions in favor of transparency play impor- tant role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.
the paper. The authors should use their best
3. Theory assumptions and proofs
Question: For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
Answer: [Yes]
14

---

We provide complete proofs in the supplementary material for the both theo- rem and theorem stated in the main paper. Guidelines:
Justification:
The answer NA means that the paper does not include theoretical results.
All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated referenced in the statement of any theorems.
The proofs can either appear in the main paper or the supplemental material, but they appear in the supplemental material, the authors are encouraged to provide short proof sketch provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proof's provided in appendix supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental result reproducibility
Does the paper fully disclose all the information needed to reproduce the main ex- perimental results the paper to the extent that affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided not)?
Question:
Answer: [Yes]
Justification: We detail the steps for reproducing our main experimental results in Sec- tion 1.,,etntoon 5.2, and Section 5.3, and describe the implementation of our framework in Section 6, Additional implementation and experimental details are provided in the supplementary material.
Guidelines:
The answer NA means that the paper does not include experiments.
If the paper includes experiments, a No answer this question will not perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
the contribution is a dataset and/or model, the authors should describe the steps taken make their results reproducible verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is a novel architecture, describing the architecture fully might suffice, or if the contribution be necessary to either make it possible for others to replicate the model with the same dataset, or provide access to the model. In general. releasing code and data often one good way to accomplish this, but reproducibilityy can also be provided via detailed instructions for how to replicate the results, access to a hosted model (e.g., in the case of large language model), releasing of a model checkpoint, or other means that are appropriate to the research performed.
specific model and empirical evaluation, may
While NeurIPS does not require releasing code, the conference does require all submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) If the contribution is primarily a new algorithm, the paper should make it clear how to reproduce that algorithm.
(b) the contribution is primarily a new model architecture, the paper should describe the architecture clearly and fully.
(c) If the contribution is a new model (e.g., a large language model), then there should either be way access this model for reproducing the results or way to reproduce the model (e.g., with an open- open-source dataset or instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which authors are welcome to describe the particular way they provide for reproducibility. the case of closed-source models, may be that access to the model is limited in some way (e.g., to registered users), but it should be possible for other researchers have some path reproducing or verifying the results.
15

---

reproducible, they 5. Open access to data and code
Question: Does the paper provide open access to the data and code, with sufficient instruc- tions faithfully reproduce the main experimental results, described in supplemental material?
Answer: [No]
Justification: Our implementation can be reproduced by following the detailed algorithmic steps in Section 5 and the elaborations of experimental setups for each case in the Appendix.
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurIPS code and data submission guidelines httpss//nips..c/public
Suidds/CCoeSubbiisiooPoolcc for more details.
While we encourage the release of code and data, we understand that this might not be possible, so "No" an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (c.g., for new open-source benchmark).
The instructions should contain the exact command and environment needed to run to reproduce the results. See the NeurlPS code and data submission guidelines (https: for more details.
The authors should provide instructions on data access and preparation, including how access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. If only subset of experiments should state which ones are omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
Providing as much information as possible in supplemental material (appended to the paper) is recommended, but including URLs to data and code is permitted.
6. Experimental setting/details
Question: Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Answer: [Yes]
Justification: We provide all details about hyperparameters and environment setup in supple- mentary material.
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented in the core of the paper to level of detail that is necessary to appreciate the results and make sense of them.
The full details can be provided either with the code, in appendix, or as supplemental material.
7. Experiment statistical significance
Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Question:
Answer: [Yes]
Justification: Standard error is reported in all figures and tables throughout the paper (represented by the color-shaded areas).
Guidelines:
The answer NA means that the paper does not include experiments.
The authors should answer "Yes" if the results are accompanied by emoor bars, confi- dence intervals, or statistical significance tests, least for the experiments that support the main claims of the paper.
16

---

The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall run with given experimental conditions).
The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.)
The assumptions made should be given (e.g.. Normally distributed errors).
It should be clear whether the error bar is the standard deviation the standard error of the mean.
It is OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2-sigma error bar than state that they have 96% CI, if the hypothesis of Normality of errors is not verified.
For asymmetric distributions, the authors should be careful not show in tables figures symmetric error bars that would yield results that are out range (e.g. negative error rates).
error bars are reported in tables or plots, The authors should explain the text how they were calculated and reference the corresponding figures or tables in the text.
8. Experiments compute resources
For each experiment, does the paper provide sufficient information on the com- puter resources (type of compute workers, memory, time of execution) needed reproduce the experiments?
Question:
Answer: [Yes]
Justification: All experiments are conducted on an Apple MI Max (10-core CPU, 24-core GPU).
Guidelines:
The answer NA means that the paper does include experiments.
The paper should indicate type of compute workers CPU or GPU, internal cluster, or cloud provider, including relevant memory and storage.
The paper should provide the amount of compute required for each of the individual experimental runs as well as estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported in the paper (c.g., preliminary or failed experiments that didn't 't make into the paper).
9. Code of ethics
Question: Does the research conducted in the paper conform, in every respect, with the NeurlPS Code of Ethics
Answer: [Yes]
Justification:
We believe we fulfill specifications the ethics guidelines.
Guidelines:
The answer NA means that the authors have reviewed the NeurIPS Code of Ethics.
the authors answer No, they should explain the special circumstances that require deviation from the Code of Ethics.
The authors should make sure to preserve anonymity (c.g.. if there special consid- eration due to laws or regulations in their jurisdiction..
10. Broader impacts
Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [Yes]
Justification: Yes, discussed the societal impacts in Section 7.
Guidelines:
The answer NA means that there is no societal impact of the work performed.
17

---

If the authors answer NA or No, they should explain why their work has no societal impact or why the paper does not address societal impact.
Examples of negative societal impacts include potential malicious or unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.
The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments. However, if there is direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology.
If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition attacks, mechanisms for monitoring misuse, mechanisms to monitor how system learns from feedback over time, improving the efficiency and accessibility of ML).
11. Safeguards
Does the paper describe safeguards that have been put in place for responsible release of data models that have high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Question:
Answer: [NA]
Justification:
This paper poses no such risk.
Guidelines:
The answer NA means that the paper poses no such risks.
Released models that have high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere to usage guidelines or restrictions to access the model or implementing safety filters.
Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images.
We recognize that providing effective safeguards challenging, and many papers do not require this, but we encourage authors to take this into account and make best faith effort.
12. Licenses for existing assets
Are the creators or original owners of assets (e.g.. code, data, models), used in the paper, properly credited and the license and terms of use explicitly mentioned and properly respected?
Question:
Answer: [Yes]
Justification:
We did use existing assets, and we properly cited them in the paper.
Guidelines:
The answer NA means that the paper does not use existing assets.
The authors should cite the original paper that produced the code package dataset.
The authors should state which version of the asset used and, possible, include URL
The name of the license (e.g., CC-BY 4.0) should be included for each asset.
For scraped data from a particular source (e.g., website), the copyright and terms of service of that source should be provided.
18

---

If assets are released, the license, copyright information, and terms of use in the package should be provided. For popular datasets, paperswitheode. com/datasets has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided. If this information is available online, the authors encouraged to reach out the asset's s creators.
13. New assets
Question: Are assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [NA].
Justification: This paper did not release any assets, the main contribution is new framework that leverage on existing learning techniques to solve our target objective.
Guidelines:
The answer NA means that the paper does not release assets. Researchers should communicate the details of the dataset/code/model as part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent was obtained from people whose asset is used.
At submission time, remember anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file.
14. Crowdsoureing and research with human subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well details about compensation (if any)?
Answer: [NA]
Justification:
This paper does not involve crowdsourcing nor research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Including this information in the supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then much detail as possible should be included the main paper.
According to the NeurlPS Code of Ethics, workers involved in data collection, curation, other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional review board (IRB) approvals or equivalent for research with human subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained?
Answer: [NA]
Justification:
This paper does not involve crowdsourcing nor research with human subjects.
Guidelines:
The answer NA means that the paper does involve crowdsourcing nor research with human subjects.
Depending the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
19

---

We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors adhere the NeurIPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if applicable), such as the institution conducting the review.
16. Declaration of LLM usage
Does the paper describe the usage of LLMs if it is an important, original, or non-standard component of the core methods in this research? Note that if the LLM is used only for writing, editing, formatting purposes and does not impact the core methodology, scientific rigorousness, or originality of the research, declaration is not required.
Question:
Answer:[NA)
Justification: The core method development (i.e., technical content) in this paper does not involve LLMs.
Guidelines:
The answer NA means that the core method development in this research does not involve LLMs as any important, original, non-standard components.
Please refer our LLM policy (ttp:://eeuiiscccccoooceeeee/ess for what should or should not be described.
20

---

A Proofs of Theorems
A.1 Proof of Theorem
Recall that given HyperLTL formula y,, Skolem (p) is in the form of:
Skolem(p) 3f. (T......... 100
Skolem(
for each 'EQa
for each JEQ
Assuming that Neqauu (xz) JeQy is the optimal set of policies for the Skolemized i,, then for every k 2 O, it maximizes the probability of converging to Pmar for the inner LTL sub-formula Skolem(p):
IP ( (2TT((((((()) Ug (Tr(S)
()). Skolem(
Pmar
That is, any step k. the zipped path derives a set of paths that instantiate each path variables in the original yo as follows:
For all universal quantified paths Ty, where j Q²:
[Ti + Tr(Si (o:;)]
For all existential quantified paths Tr, where i Q3:
[T (Tr((Si (o:x)) .... Tr(Si [y) and for each 10. if = then Tr(Gi (ox:)) Tr(Si (135))
This instaintiation guarantees that the probability of satisfying y is maximized up to step k. Next, with an optimal action given by its corresponding optimal policy (eq) U (eq) That is, the same path mappings of each universally quantified path variable Sj and existentially quantified Skolem function witnesses f, holds for all k 2 O. Finally, for the original HyperLTL formula & QITI Q2T2.... ... Qn- b by instantiating the trace variables in the same fashion for all of i E Qa and all TÚ of j E Q", the same optimality immediately follows, because the optimal convergence to Pmar means maximizing the probability of satisfying the inner LTL sub-formula. That is, the optimal set of paths (derived from the zipped path) also optimizes the satisfaction of original ip for all steps k 0. To this end, we proved that, an optimal tuple of policies (m²) keq= Ug (Ee) for Skolem (sp) is also an optimal set of policies for yo, that optimizes the probability of satisfying to in M.
the zipped path proceeds to step
A.2 Proof of Theorem
Bellman's 's Principle of Optimality [6] states that "for an optimal policy, no matter what the initial decision is. the remaining decisions must constitute an optimal policy with regard to the state resulting from the initial decision". An extended lemma (proved in [1]) states that for a discounted MDP, there exists an optimal policy, denoted as NN* such that for all (s, a) E S x A, there exists a maximum Q-value achieved by N (denoted QNN") " as introduced in Equation (3):
QN (s, a) A max VN (s, a)
NN
Let us denote NN(a s) as WA's decision to take action a state Our goal is to find an optimized NNN, such that:
E a') R(s, a) + ENN(a s)E(s', NN
max
E'
aEA
where P(s, 0, 8') is the one-step transition probability, R(s, a) the reward taking action a on state is a discount selected factor, and E is the expected reward of keep taking an action a' on a state s'. (as defined in Section 5.3). Recall that in Section 5.2, our immediate reward R(s, a) is associated with robustness value of finite prefix by evaluation only up to the current seen state
21

---

s (i.e., independent from the unseen s' after taking action a). As a result, maximizing N. do not depend on Rss, a). the previous optimization problem is equivalent
R(s, a) + max NW
a(s, S'ES
ENN(( ( s) a0]
aEA
Let us now only focus the optimization part (i.e., the right side of the plus operator in the above formula). Based on the definition of expected reward defined in Section 5.3, the above formula shows that optimal NN is more likely the take action a (by the learned NCA((a s)) that has higher probability (decided by (s,, a, s')) to transit to an unseen state that lead to higher expected value (estimated by [[s',, a') a")). That is, given a state s, NN* outputs an optimal action a, such that:
P )) RR('', d')] ")
which, intuitively, represents an optimal one-step look-ahead. Now, to connect the above formula with the reward function defined in Section 5.3, we have:
NN.
(B..P(s...)) p ( (on)))/ (Tr()) (o.))))()))))))))))))))))))))(
Skolem S.)ssse
iEQR JEQY
where is the state the k-th step of the zipped path. Recall that p is constructed using min-max approach as presented in Figure 3, so the optimal outcome of p can be derived from the Minimax Lemma [18]. That is, if each path always considers the "worst-possbble" scenario that other paths will act during learning, it leads to a set of optimal policy among all paths. Hence, is guaranteed optimal for all steps Ao O, which implies the maximum probability of the following:
P | (ip((TT(S))): ~ Us (Tr(Si D2,))) Skolem (b) ()) 3 Pmox "eQ",JCC)
To this end, we prove that the action chose by N achieves the maximum expected value E for all (s, a) S A. Finally, (fa) and (mÿ)) can be inductively constructed from N (as we elaborated in Section 5.3), which is policies set that optimizes the satisfaction of Skolem
B Additional Algorithmic Details of HypRL
Expected Reward of a Zipped Trace. with discount factor 7 E [0 is:
The expected reward of state 8 after taking an action ag
E(sk, Sk; a3)
y* x R(8k4441,44444
Intuitively, E(sk, as) evaluates "how good" of choosing 4g on Sy in infinite time steps, where each step is discounted by 7. We address that, is often chosen based the optimization goal. For example, for short-term tasks, a lower 7 is preferred because the expected robustness value focuses more immediate p value. We report the setup of these hyperparameters in Appendix D.
C Comprehensive Example of HypRL Algorithm
In this section, we present a comprehensive head-to-toe example that aligns with the algorithmic details presented in Section 5.
Formula Skolemization. In Section 3, we presented the HyperLTL formula for our wildfire
example follows:
Requirements: &PRescue Bro..re
A Usevee thsitt A thsate)
O : thtire ((T,)) A (UT)))
C1 Vidier O Locoaaiio,, Location
O2 t'aave
(l A (())))
C2 Usate
(-ing U4 ( ( cm)
22

---

Following the illustration in Section 5.1, the Skolemized form of the formula Rescuu is as follows:
Skolem Akolemm(RResuu)) (PRescue)
Skolem (Vhre) Skolem (Vsave) Skolem A Skolem (Vaaee)
Skolem (Vhire)
(in) (
Skolem (ave))
(9E)) ^ ((&)
Skolem diet)
[ [ooaaaio Location,, | < <3)
Skolem saaee)
(- 4 (-.) A (- 4 f ( u cn,)
In this context, there are two quantifiers, Q22 so Q [2). and Q1 = so Q^ {1}. Besides, all propositions the existential quantified path variable (originally subscripted by 72) average now subseripted by fy in the Skolemized form. Furthermore, for each inner LTL sub-formula, the propositions subscripted with 72 is substituted with propositions subscripted with fg.
Robustness Optimization. Continuing with the Skolemized formula:
(r))..). Skolem Skolem (Saave) A Skolem (Vdist) Skolem (sasate) Our goal is to optimize the following:
(mt. m²) arg max IP p(zip((Tr((ippp) ~ DA,). Tr((2(o:ka) Drz)l), (2))
Skolem (ehtre A sssve A Vaist A (lsate) + Pmaz
Notice that, by applying Ug. the order of the quantified traces are the right order with respect to the original Hy formula
D
Implementation and Experimental Details
D.1 From HyperLTTI Formulas to Robustness Functions
In our implementation, we use the theory developed in Section 5.1 to obtain the Skolemized form of the formula, denoted Skolem(p). We then generate the corresponding robustness function using the approach presented Section 5.2 (see [32] for details on translating temporal properties into robustness functions). We elaborate the following term from the quantitative semantics introduced in Figure 3:
p (Tr((Geea) < <)))= c (((se)
This equation lies at the core of transitioning from logical properties (which yield Boolean outputs) robustness functions (which produce real-valued outputs). To apply this transformation, must define the function f and the constant for each property considered in this paper. We now provide details explanations how we define such functions and constants for each formula introduced in this paper.
The HyperLTL formula defined for safe reinforcement learning (SRL), denoted as PsRl: For the property (Mr, .ト (I BG1), define f as a distance function and set = 1. The distance function we have in this case study follows the well-known Manhattan distance definition. That is:
Dist Dist((En,) Vr)) (#G1 Foi)) A (Iz, xcil + lu MGil)
The, by setting e = 1, this yields the following expression:
Dist((xr Vr.) (Ir1, (G1)) < 1,
which expresses that the distance from the first agent (i.e., Ti) to its goal (i.e., G1) is less than one, which implies that the first agent has indeed reached the specified goal location. The corresponding equation is:
Dist((En, Vn), (IGI, 3G1))
The optimal value achieved when the agent exactly at the location of the goal position, giving - 0 0== 1.
23

---

For the property (Zr,, (r,) (TG2, VG2), the same definition for the distance function similarly defined. That is:
Dist(( Urg), (#G2, UG2)) < 1,
which expresses that the distance from the second agent to its goal less than one, so the corresponding equation is:
- Dist(((rr) yo.), (#G2, VG2))
The optimal value is achieved when the second agent exactly at the goal position, giving = For the property (Er, Vn.) & (Er,, Bru), we define as distance function and set -1. This yields the condition:
-Dist(( Un)), (Figg) Ur.)) < -1,
which expresses that the distance between the first and second agent (i.e., Ti and T2)
is greater than one; i.e., the agents are not in the same location. The corresponding equation is:
-1 + Dist Mr.), (Erg Vry)).
This equation is maximized when the two agents are far apart, and it evaluates to -1 when they in same location.
The HyperLTT formula defined for deep sea treasure (DST), denoted as PDst:
For the properties 71, 72, ... we define f for each treasure Ti a distance function between the position of the submarine driver (7,) and the treasure location (Ti), and set = 1. This yields the condition:
Dist((Mr, Un)) (FT1, Urr)) <
which expresses that the distance from the first agent to TI is less than one. The corresponding equation is:
- Distt(ssss)) vrrr (FT1, 9T1))
The same approach is applied to 72, 73.... and the remaining properties.
For the property slepre < ō, we use the same approach and obtain the following equation:
-
step
For the property ppos,, pos This yields the condition:
< 1, we define f as a distance function and set 1.
Dist ( Vr,), (Eig Vr.)) < 1,
which expresses that the distance between the first and second agent is less than one. That is, the agents are in the same location. The corresponding equation is:
Dist((z,, vr.), (Erz, Vrr))
This equation is maximized when the agents in the location.
The formula defined for the Post Correspondence Problem (PCP), denoted as yPcp:
To address the properties such as (p1 <+ P2), where p means a sequence of alphabets (that forms string), we define as function of evaluating whether strings matching and set c = The matching function we have in this case study is as follows:
(2) {
pı and p2 are equal,
otherwise.
This yields the condition:
Match(pi, P2) 1,
which expresses whether the two compared alphabets and p2 are equal or not. The corresponding equation is:
Match(pI, P2)

---

(a) ISR
(b) MIT
(c) Pentagon
(d) SUNY
Figure 7: Maps of Grid World [35] benchmarks.
For the symbol #, we are checking whether the alphabet under consideration equal to #. This is expressed as the logical condition #
The HyperLTL formula defined for the wildfire scenario, denoted as (PRescue
For the properties V7, V2, ... and FI, F2, ...,, we the same distance function Dist (as in SRL and DST) to calculate the distance from agents to victims and fire zones, with 1. That is, the reachability of the two objectives.
For the property [Location, Location,, < 3, we use the distance function Dist with 3. This constraints make sure that for the optimized strategy, the two agents are always staying within the safe communication range.
D.2 Safe RL (SRL)
Case Study Setup. In the Safe RL case study (see Figure 7), the blue circle (denoted A1) and the orange circle (denoted A2) are agents that aim to learn optimal policies to navigate from their initial positions their respective targets: the blue square (G1) and the orange square (G2), while avoiding collisions. The state space is represented as tuple (x, y), and the action space is defined as a {stay, up, down, left, right). The following HyperLTL formula SSRI. specifies the required objectives:
Vn 3r2 (o (OVG,, A V/G2,, A C (CAA,.
SPSRI.
where the subformulas defined as:
vG.,,
(KrT Vmm) ( vG1),
VG22,, & ( (ra) (xG2, WC2),
d'AA (Ir, Vni) + (Erzy Vra)-
Here, VGI-, and vhee., express that A1 and A2 eventually reach G1 and G2, respectively. The subformula @CAr ensures that the agents avoid collisions while navigating toward their goals.
First Experminent Setup. In the first experiment, ensure fair comparison, evaluate HYPRL combined with CQ-Learning against the shielding method [17] also using CQ-Learning. The implementation and hyperparameters of CQ-Learning are taken from [17]. Since CQ-Learning initially employs a decentralized phase (i.c., a single-agent state space), we modify the formula SSRL remove inter-agent dependencies:
VTI-VT2- (OVGI. A 1G22,, T
25

---

In this setting, Skolemization is unnecessary. and the agents act independently. When the algorithm transitions into a joint phase, expanding the state space to include inter-agent interactions, we use the original specification SSRI.. At this stage, HYPRI. guides the learning process effectively to achieve both goal completion and collision avoidance.
Second Experminemt Setup. We employ DQN as our learning algorithm, utilizing a neural network with three hidden layers of 512 nodes and ReLU activation functions. We set the discount factor to 7 = 1.0, the learning rate to 0.001, the initial to 1.0 with decay rate of 0.995 down to minimum of 0.01, and use the Adam optimizer. We set the number of training episodes 200 for the SUNY, ISR, and Pentagon maps, and to 300 for the MIT map due to its increased complexity, Each episode consists of 300 steps (see Figure for the map setups).
Baselines Reward Functions.
The manually designed reward functions have the following form:
if both agents reach their respective goals, if one agent reaches its goal. the agents collide.
RSRL.
The function R addresses all objectives and safety constraints of the problem. The manually designed reward function is tested with the following values:
* a = 10, b = 5, c= = -5 (R.RI)
a = 2, 1,c = -1 (RRSKL)
20, b 10,
10 (RISL))
* a = 100, b = 50, c = 10 (IRSLL)
a 10, = 5, c = 110 (RSRL)
In the main paper, we report the results obtained using values a = 10, =, (RSRI) for the baseline reward function. Figure 8 presents the results corresponding all different reward functions R², R2, RS, R2,, and R2 we introduced above.
D.3 Deep Sea Treasure (DST)
This case study (see Figure 9) was originally proposed by [42]. We adopt the implementation provided in [46]. The state space represented as a tuple (x, y. step), and the action space is defined as = {up, down, left, right). The following HyperLTL formula yDST specifies the required objectives:
Case Study Setup.
PDST Vr, (TT,, A (TT2, A (TT3,)...)) A A (step,, < 6) A AN ((pos,, - poss, < 1)
The original case study is in single-agent environment with two objectives. We modified it into multi-agent problem by assigning agent with the objective of maximizing collected treasure, and another agent with the task of keeping the number of steps below a certain threshold.
Experminent Setup. For our experiments, we used PPO and DQN implementations from [38]. For DQN, we set the hyperparameters as follows: discount factor y = 0.99, e decaying from 1.0 to 0.07 over a fraction of 0.2, and learning rate of 0.0004. Since the DQN implementation from [38] does not directly support dilli--discrtte actions, we expanded the action spaces of both agents and defined unified action space compatible with this implementation. For PPO, set hyperparameters as following, = 0.99, clipping factor to 0.2, learning rate to 0.0003, and GAE lambda to 0.98.
Additionally, ensure fair comparison, added reward penalty of 10 the baseline reward function whenever the two agents became separated.
D.4 Additional Experiment on DST
We conduct an additional experiment on DST, where the focus is on minimizing the step constraint in problem. In Table 6, we report the number steps required for the cumulative treasure achieved by the treasure collector to exceed values of 1, 5, 10, 15, 20, and 30. The results show that HYPRI consistently and significantly outperforms the baselines in all settings, except when using PPO trained for 1000 episodes.
26

---

100
16
90
Total
100
2001
2100
1800
200
250
300
Espisodes (SSR)
Kyisodes (PENTGONN)
Kgisodes (SUNY)
Eguisdes (MIT)
Collaiens
200
200
Egisodes
Egisodes (PENTAGON)
Egiindes
Epicedis
10
Callitios
100
20d
100
200
1000
2001
150
300
Episudes (ISR)
Egisndes (PENTAGON)
Egisodess (SUNY)
Epieodes (MIT)
Figure 8: Total number of successful goal completions by both agents (top) and number of collisions (bottom). Lines
and correspond to reward functions R R2, RS, RA. and R respectively. Results are averaged over 10 runs.
D.4.1 The Post Correspondence Problem (PCP)
Case Study Setup. PCP (see Figure 11) consists of a set of k dominos, denoted as D domo, domp..... ] Each domino dom; (0 < S k) is represented by pair of nonempty finite words (lop,, bot,) from given alphabet Σ. The objective is to find finite sequence of dominos such that the concatenated words on the top match those on the bottom. our case study, the state space is defined as tuple (top, bot) for each domino. The action space consists of selecting a domino from D, resulting in & possible actions = { {domo, dom domp). Notably, traces (i.e., agents) are unaware of the context of the dominos and can only identify them by their labels (i.e., dom4). The initial state of the MDP encodes empty words on both top and bottom: s (E.e).
Table 6: DST results steps required to achieve the desired treasures, showing average and standard error over 10 evaluations.
Treusures Achieved
Method
Rpisndes
30
PPO
500
199.01-16.55
218.66:1:6.77
244.87=66.68
247.89-26.77
253.16++6.66
268.01+66.70
PPO +HyPRL
500
13.30:11001
29.72=1.57
39.10=:1.81
49.22
56.59-2.03
71.55:2.26
PPO
1000
5.75+t0.30
6.75-t0.30
29.68:10.76
32.29 75
36.09=0.74
39.82:10.72
PPO +HYPRL
1000
55.3743.66
106.89
126.25=6.10
141.06=5.27
153.49.15.35
183.5115.70
DQN
500
332-10999993
997.54.16.99 95
916.40-55.00 63
917.64455.6
917.89-55544
926.33+15.25
DQN +HyPRL
500
114.60:12.67
115.61:12.56
116.61=2.52
117.61+2..0
148.66:1-..44
1.5.3911.558
DQN
1000
893.37 993.37-199.6
953.25.16.55
992. 10 50
992, 12:12.55
996.05-t1.52
997. 19411.14
DON +HYPRI.
303.63 +6664
319.09 6..38
335.20
335.20
337.21
339.90+6.22
27

---

182
88
T9
Figure 10: Job Scheduling bench- mark.
Figure 9: DST Grid Map.
Subsequently, they choose actions from the action space (choosing domino) to construct traces that aims to satisfy the PCP objective.
Before encoding PCP HyperLTTI, problem for the EE fragment of HyperLTT. and the emptiness problem of nondeterministic finite-state hyper automata. Part of the encoding is to ensure that only valid dominos those constraints in our encoding, as the action space of the MDP enforces choosing valid dominos only. This is the reason our that encoding less complex than that of [19, 9].
that in [19, 9], the authors reduce PCP the satisfiability
chosen. We do not need
We formalize valid solution to PCP in HyperLTL. as follows. The set AP of atomic propositions defined such that as Σ 2P U {#), where # encodes termination. Essentially, the HyperLTL formula requires that for all traces T1, where top and bottom words match up to the end of the shorter trace, there exists trace 72 such that is SemiMatch and T2 extends to complete equal top and bottom words:
PPP A BTg.Br2. UsemmMatcc,,, U (V'xtend,, MaMthh-
where SemiMatth means the top and bottom words match up to the length of the shorter word:
(Ptopr, + Pbott,) ) U (# top,, @ #bot,,)
SemiMatch
PEAP
where '0" is the xor operator. The formula (Match indicates that the word constructed on the top and bottom equal:
Matchh
O
A (Prop-, + Pootry)
PEAP
Finally, formula p encodes that trace is successor trace follows:
((PLOP,, ++ (toop-.) A (Whot., + Phhtt.,)) ))] U
(Extend 11112
PEAP
(H#rop,, V #oo ( (-#top,,
- bot
Experminemt Setup. We employ DQN as our learning algorithm, utilizing a neural network with three layers of 512 nodes and ReLUU activation functions. We set the discount factor y to 0.99, the learning rate 0.001, and the initial c to 1.0 with decay rate of 0.995 down to a minimum of 0.001. We use the Adam optimizer and train for 1000 episodes. This experiment is conducted for domino collections containing and dominos.
Baselines Reward Functions.
The manually designed reward functions have the following form:
aa if the same indexed letters the top and bottom equal,
PCP
6 otherwise.
28

---

Semi Match
Collection of & dominos
ab
cuf
dg
fs
at
Match
bc:
dg
huah
dg
ah
ab
cf
hach
bc
dg
ab
P
cf
cafa
dg
Not Match
dg
Aucula
Figure 11: PCP overview
10a
10
of successful match
109
10-1
200
400
600
800
1,000
Episodes
RPCP RiCP
RPCP RPCP
RT
Figure 12: PCP baseline results showing average total matches over 10 runs.
The function RCP addresses all objectives and safety constraints the problem. The manually designed reward function is tested with the following values:
a 1, b - (12P()
5, b - (PPPCP)
a 10, = - (RPEP)
1, b -5 (RPPP)
In the paper, we report results using the baseline reward function with values = 5, b - 2 (RPCP) for & 5, and 1, b -1 (R(CT) for k Figure 12 presents the results corresponding to the different reward functions. The baselines Reter Re and 12PCP for k = 6 did not successfully produce any matches. We visualize this using value of zero in the log-scale plot shown in Figure 12.
Table 7: Wildfire results, avg, and std. enror of 10 trials after 5k episodes.
Size Method
Dist
Steps O
Steps O2
PPO REAIR
2.8+00011
77.13
T/O
32
PPO + FAIR
2.5+0.01
33.43
787.03=31.8
PPO RFAIR
5.640.02
31.2+4.5
7057.8=1047.9
52
PPO REAIR
4.2+0.01
62.749.7
T/O
29

---

D.4.2 Wild Fire Scenario
Case Study Setup. Consider a wildfire scenario in a grid-world environment as we introduced in Section I. Three locations are on fire, and two victims need to be rescued. Two autonomous agents are deployed from the same position with distinct objectives: the firefighter agent (FF) must extinguish all fire zones, and the medical agent (Med) must rescue all victims. The agents must also satisfy two constraints: which requires them to always remain within a 2-cell communication range; and which prohibits Med from entering any fire zone before FF has extinguished the fire in that zone. The state space is represented
tuple (z, y). and the action space is defined as a = {stay, up, down, left, right). The goal is to learn optimal policies for FF and Med that maximize the probability of satisfying all these requirements. The following HyperLTL formula captures the objectives of this case study:
Rassuue VTI.Bra. A gleve A Vdia A vssate)
O1 : Phire
(1n,)) (l (crr) C1 Pliist e [((oocation,
Location,.l 3) C2 Masaee - (-irg U in)) ) A (-f-2 ( U o-))
O2 Vsave =0(=2) A ((fm))
Experiment Setup. We use the PPO implementation from [38], with the following hyperparameters: a learning rate of 0.0003, clipping parameter of 0.2, discount factor 0.995, and GAE lambda of 0.95. We conduct our experiments on 3 3 and 5 5 grid world environments. The timeout is set to 1000 steps for the 3 x 3 grid and 10,000 steps for the 5 x 5 grid.
Baselines.
We evaluated (see Table 7) two baseline reward functions in this experiment:
REAIR; extinguishing fire: +50, rescuing a victim: +10, agent out of range: -100, and Med in a fire zone: - 100.
IEAIR, Extinguishing fire: +10, rescuing vietim: +50, agent out of range: 1000, and Med in a fire zone: - -100.
We used REAIR in the paper, although in x 5 RH performs better than I25AI (in terms of only Steps Oj and Steps O2). However, we chose include REAIR in the main paper because its performance in the 3 x 3 grid is consistently better than RTAIR across all metrics. This trend does not hold in the 5 x 5 grid, where REAI outperforms RFAIRR only in Steps O₁ and Steps Oz.
D.5 Additional Experiment
Case Study Setup. In this case study (see Figure 10), a single permanent resource is placed on a grid with multiple agents, which must learn to share resources. The objective here is to maximize the overall utility of all agents while ensuring fair allocation of the resource. other words, the goal is not merely to maximize utility by allocating the resource to single agent but to distribute equitably among all agents. The action space is defined as a = {stay, up, down, left, right). The state space is extended by (I, Energy). We expresses our allocation and fairness objectives by the following HyperLTL formula:
FFAIR VT1.Vz2- ( Resource, JO Resource
[ ([Energy,, Energy < <8)
That is, all agents should eventually gain access to the resource at every step, while ensuring that the difference in their Energy levels (i.e., allocated resources) remains less than threshold 8, which can be set as a hyperparameter'. In our setup, agents start with Energy = 0, and each time an agent reaches the resource position, its energy level increments by one while maintaining the same action space.
Experiment Setup. We employ PPO as our learning algorithm, using two neural networks: a policy network and value network. Both networks consist of three hidden layers with 512 nodes and ReLU activation functions. The policy network uses softmax activation in the output layer, while the value network uses a linear output. We set the learning rate to 0.001, the discount factor 7 = 0.95, and the clipping factor to 0.2. Optimization is performed using the Adam optimizer. We also set ö 10.
We acknowledge that O is a Büchi condition and is strange to be use in finite semantics. Nevertheless, when it is interpreted in the context of robustness values, function P attempts to maximize the occurrence of Resource, which is the intended objective.
30

---

Baselines Reward Functions.
The manually designed reward functions have the following form:
a if resource allocated either of agents, Agent
REAIR
b
|Energy Agent Energy Agemt >
The function RFAIR addresses all objectives and safety constraints of the problem. The manually designed reward function is tested with the following values:
a = 2, b -1 (12FAIR)
a 20, = -5 (REAIIR)
a 10, = -5 (IE5ARR)
5, b -5 (TRFAIR)
The evaluation (see Figure 13) demonstrates how the learning process maximizes utility for both agents while minimizing the difference in their utilities. Figure 13a, using HYPRL, we observe that the two agents initially start with low resource utilization. Although this issue is addressed over time, there is noticeable gap in resource allocation between episodes 150 and 270. HYPRL gradually reduces this disparity, and after episode 400, it achieves high resource utilization while maintaining fairness. This is evident from the fact that the gap between the maximum and minimum utilization becomes nearly invisible between episodes 400 and 500. By the end of training, each agent receives approximately 40 45 resources per episode (with 100 steps), while the optimal allocation is 50 resources per agent. These results highlight the effectiveness of HYPRI. in achieving fairness in MARL..
Analysis and Results.
On the other hand, using PPO with the baseline reward functions does not successfully yield a policy that both maximizes the average utility of the agents and minimizes the gap between the minimum and maximum allocated resources. For example, I2 (see Figure 13b) succeeds in maximizing the average resource allocation the optimal level but fails to minimize the disparity between agents in terms of resource allocation. The other baseline reward functions R REAIR and R exhibit similar behavior (see Figures 13c to 13e, respectively). While they perform better than R RFAIR in minimizing the min-max range of resource allocation, they still fall short compared to HYPRI. in achieving both fairness and optimal utility.
E
Why HyPRL is Important?
In this work, propose method named HyPRL, which introduces novel fusion between reinforce- ment learning and recently developed class of logics known as hyperpropertics. Hyperpropertics have gained increasing attention in the formal methods community due to their expressive power in capturing system-level behaviors that span across multiple execution traces. We observe that many objectives and constraints in MARL naturally align with the expressive capabilities of hyperproperties. Motivated by this insight, we present a framework that first formally specifies the objectives and constraints of given RL problem using hyperproperties and then learns policies that aim to maximize the probability of satisfying these specifications.
We believe that our approach provides solid theoretical foundation for direction in reinforce- ment learning, where users can formally express their high-level requirements using hyperpropertics and then synthesize policies that satisfy them. Importantly, hyperproperties are not limited to specify- ing objectives of individual agents or pairwise dependencies. Recent extensions such as HyperATL. [7] allow reasoning about team-level objectives and inter-team relational dependencies, further expanding the scope of formal specification MARL..
31

---

50
# of allocations
40
30
20
100
200
300
400
500
Episodes
(a) HYPRL
# of allocations
80
# of allocations
50
60
40
30
20
10
100
200
300
400
100
200
300
400
Episodes
Episodes
(b) FRAIR baseline reward function.
(c) PEAIR baseline reward function.
# of allocations
# of allocations
50
50
30
3
30
10
100
200
300
400
100
200
300
400
Episodes
Episodes
(d) 1e FAIR baseline reward function.
(c) I2 baseline reward function.
Figure 13: Fair resource allocation results under various baseline reward functions. Boundaries
represent the minimum and maximum allocated resources per episode. Dashed lines indicate average usage, dashed-dotted lines show optimal allocations, and solid lines represent polynomial trend fits. Results based on 10 independent runs in 4 x grid with two agents, each consisting of 500 episodes with 100 steps per episode.
32


Reviews:
[{"review_id": "0D7EnD8vL6", "reviewer": "Reviewer_UWS5", "summary": "This paper introduces HYPRL, a reinforcement learning framework that solves the difficult problem of designing rewards for complex multi-agent tasks described using hyperproperties. The framework allows users to define intricate objectives and dependencies between agents using the formal logic of HyperLTL which is then automatically translated into a numerical reward signal (i.e., a robustness score). This is  maximized via a centralized reinforcement learning (RL) algorithm to find coordinated policies that satisfy the original requirements.", "questions": "1. What are the scalability limits of the approach in terms of the state-space and action-space dimensions studied?\n2. How would the system prioritize safety (less collisions) without a manually constructed shield?\n3. How are max-min in the robustness semantics differentiated through? Have “soft” versions of max-min been used?\n4. What are the exact state-space or action-space augmentations used in the RL algorithm? Is there a way to decentralize execution?", "limitations": "- Only shown on a 2-agent case (scaling to n-agents may pose challenges)\n- The algorithm is centralized making it unsuitable for large agent populations.", "rating": 4, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 2, "significance": 3, "originality": 3, "strengths_and_weaknesses": "## Strengths:\n\n- HyperLTL captures multi-agent tasks not describable easily by vanilla LTL such as quantifier logic dependent on different agents. It solves the tasks by means of Skolemization of the existential quantified agent policy which is then fed to a centralized RL algorithm.\n- The reward shaping is automatic from the specification and the approach is shown to be agnostic to the RL algorithm used with applications using PPO, DQN and CQ-Learning.\n\n## Weaknesses:\n\n- Only considers the 2-agent setting and a single universal plus existential quantifier in sequence in the experiments.\n- Assumes fully observed environments which may be hard in the presence of multiple other agents.\n- It appears that collisions are **more** than the vanilla case of CQ in the SRL environments (albeit in a shorter completion time). Given that safety is part of the specification, this is concerning.", "was_revised": true, "final_justification": "The paper's core contribution, i.e. using hyperproperties to reason over the joint traces of all agents, is a significant and welcome departure from typical multi-agent methods that focus on specifications for individual agents. However, the primary claim of scalability is not yet substantiated. While the case studies are insightful, the validation is limited to a two-agent setting ($N=2$). Consequently, the argument for scalability to the general N-agent case remains tenuous, especially given the inherent complexity of the specifications considered. The concept is promising, but its broader applicability requires more extensive empirical evidence.", "rebuttal": "# Reviewer UWS5\n\nThank you very much for your thoughtful and constructive review. We truly appreciate the time and care you put into reading our paper. Below, we provide detailed responses to each of your questions and concerns.\n\n## Clarifications\n\n1.\t**HYPRL is Not Limited to Two Agents:**\nWhile our case studies focus on two agents for clarity, the HYPRL framework theoretically supports arbitrary quantifier structures and is likely to empirically scale to larger number of agents. We will make this generality more explicit in the paper.\n2.\t**HYPRL Does Not Require a Shield:**\nUnlike shielding approaches that rely on pre-synthesized safety mechanisms, HYPRL directly encodes relational safety and coordination constraints as HyperLTL specifications. This allows reasoning over complex inter-agent dependencies without the need for external shielding, which is a key strength of HYPRL. That said, HYPRL does not provide safety guarantees during training.\n\n3.\t**Exact Min–Max in the Robustness Function:**\nIn our framework, we obtain scalar reward signals using the robustness function; therefore, the gradient flow is independent of the min/max operations performed in the robustness computation. Moreover, we do not use soft min/max approximations for this purpose.\n\n## Response to Detailed Comments\n\n> [W1] Only considers the 2-agent ....\n\nThank you for raising this point. While our experiments focus on a two-agent setting with a single $\\forall\\exists$ quantifier alternation, our framework is not limited to this configuration. The Skolemization technique we introduce is general and can handle **arbitrary numbers of agents and arbitrary quantifier alternations** (e.g., $ \\lbrace \\forall^* \\exists ^ * \\rbrace^ * $, $ \\lbrace \\exists ^* \\forall^ * \\rbrace ^* $). Importantly, even within this setting, the tasks we address, such as the **undecidable problem** PCP, remain highly nontrivial and demonstrate the capability of our approach to handle complex relational requirements. We also note that our work is truly the first in addressing specification-guided RL for multi-agent settings with inter-agent dependencies and paves the path for future engineering extension with a large number of agents. We also believe these results serve as a strong proof of concept that HYPRL not only introduces a novel way to leverage HyperLTL formulas for reward shaping in theory but also demonstrates **practical improvements** over existing approaches such as manually designed rewards and shielding-based in safe RL benchmark (which we conducted thorough comparisons in our paper).\n\n> [W2] Assumes fully observed environments ....\n\nWe sincerely thank the reviewer for highlighting this exciting future direction. We fully agree with your comment. In this work, we began with fully observable MDP-based environments to clearly establish the core contribution of using HyperLTL for reward shaping. Extending HYPRL's strong theoretical framework to partially observable environments, such as Decentralized Partially Observable Markov Decision Process (i.e., Dec-POMDPs), where agents have different observation spaces, is promising. Indeed, we are currently working on this very problem.\n\n\n> [W3] It appears that collisions ....\n\nThank you for this observation. We would like to clarify that, in **SUNY** and **MIT** (please check Table 3), HYPRL achieves **zero collision** while maintaining shorter completion times. In **ISR**, CQ and CQ+HYPRL perform almost identically regarding safety. The only notable difference is in **PENTAGON**, where CQ+HYPRL shows a slightly higher collision rate compared to CQ. However, HYPRL achieves significantly faster task completion in this case. One can always combine HYPRL with shielding to achieve full safety.\n\n## Questions\n\n> [Q1] What are the scalability limits of the approach in terms of the state-space and action-space dimensions studied?\n\nWe do not expect the Skolemization-based transformation and robustness function to introduce significant scalability bottlenecks. They are general and can handle arbitrary numbers of agents and quantifier alternations without adding complexity beyond the underlying RL training. The scalability challenges arise primarily from centralized training. However, while we pay the cost of centralized learning, our approach also addresses a key challenge in centralized training: **agent laziness** in cooperative tasks, where some agents may contribute less toward satisfying the overall objective.\n\n> [Q2] How would the system prioritize safety (less collisions) without a manually constructed shield?\n\nThank you for this question. This point highlights one of the key advantages of HYPRL, that is, we do not require **a pre-synthesized shield** to enforce safety. Instead, we express the safety constraints directly in HyperLTL and use HYPRL to shape rewards derived from this specification. This reward shaping guides policy synthesis toward behaviors that preserve safety without the need of an external safety module. More broadly, this approach is not limited to safety; any relational or inter-agent dependency can be captured in HyperLTL and automatically incorporated into the robustness function via HYPRL.\n\n> [Q3] How are max-min in the robustness semantics differentiated through? Have “soft” versions of max-min been used?\n\nWe use exact min/max operations. After we apply Skolemization in Section 4.1, we use the robustness function (which takes the Skolemized HyperLTL formula and zipped traces) mentioned in Figure 2 to compute robustness values that serve as scalar reward signals. Therefore, there is no need to differentiate (i.e., allow gradient flow) through the robustness function in our optimization during the learning process.\n\n> [Q4] What are the exact state-space or action-space augmentations used in the RL algorithm? Is there a way to decentralize execution?\n\nTo address the first part of the question, we have provided detailed descriptions of the state and action spaces for all experiments in Section E of the appendix, included in the supplementary materials. Due to space limitations, this could not be included in the main submission; however, if the paper is accepted, we will integrate these details into the final version to improve clarity and completeness \n\nTo address the second part of the question, we believe this work opens exciting new directions by applying hyperproperties to multi-agent policy synthesis. While our initial focus is on centralized MDPs, we fully agree that extending the framework to decentralized settings, such as Dec-POMDPs, is a natural and important next step. This extension would enable integration with centralized training and decentralized execution (CTDE) algorithms within the synthesis process. We sincerely thank the reviewer for highlighting this valuable perspective, which aligns closely with our ongoing efforts. We are actively exploring this direction and have observed promising early results.\n\n## Additional Experiment\n\nTo better address the reviewer’s concern regarding the scalability of HYPRL (regarding [Q1]), we conducted additional experiments on the Wildfire scenario with larger grids. We believe Wildfire is a challenging problem due to its complex constraints and requirements, and expanding the environment significantly increases the difficulty of the problem, making it a suitable setting to demonstrate scalability. The table below reports the averages and standard errors over 10 trials, each consisting of 5k episodes, repeated across 10 runs. We set the time-out (T/O) to 20,000 steps for the $8 \\times 8$ grid experiments and 30,000 steps for the $10 \\times 10$ grid experiments, respectively.\n\n|Grid| Method    | Dist | Step $ O_1 $    | Step $ O_2 $  | \n| -------- | -------- | ------- | -------- | ------- |\n8 * 8 | PPO  | 11.27 ± 0.03    | 16801.8 ± 2144.0 | T/O    |\n8 * 8| PPO + HYPRL | **6.94** ± 0.07    | **4149.6** ± 1743.1 | **386.2** ± 80.5     |\n10 * 10 | PPO  | 10.90 ± 0.01    | T/O | 29023.6 ± 976.4   |\n10 * 10| PPO + HYPRL | **5.39** ± 0.06    | **21272.8** ± 3579.0 | **570.3** ± 52.2    |\n\n**If our responses have addressed your initial comments, we respectfully ask you to consider raising the score.**"}, {"review_id": "a9rFQTh4nP", "reviewer": "Reviewer_16CQ", "summary": "This paper introduces HYPRL for learning multi-agent control policies using HyperLTL specifications. The key contributions include using Skolemization to handle quantifier alternation and quantitative semantics for reward shaping. Through experiments, the authors show HYPRL outperforms basedline on safety-aware planning and  the deep sea treasure problem.", "questions": "How does the complexity of HYPRL scale with the size of the HyperLTL formula (e.g., number of operators, quantifier alternations) and the number of agents involved? Can you provide any theoretical bounds or empirical insights into the practical limits of the approach?", "limitations": "Yes", "rating": 4, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 2, "significance": 2, "originality": 3, "strengths_and_weaknesses": "Strengths:\n1. The idea of incorporating HyperLTL for expressing complex multi-agent objectives is novel to me. As HyperLTL can capture relational properties and dependencies among agents, the proposed approach has advantage over standard LTL based approaches. \n2. The definition of quantitative semantics for HyperLTL, which translate satisfaction checking into an optimization problem, is a clever way to enable reward shaping for RL.\n3. This paper provides a thorough empirical evaluation on different benchmarks. The results demonstrate significant improvements. \n\nWeaknesses:\n1. While HyperLTL is natural for multi-agent tasks, it is also much more complex compared to other simpler logics, which could be more expensive to solve. The paper could have discussed more about the scalability of the HYPRL approach, both in terms of the number of agents and the complexity of the HyperLTL specifications, and how it compares to alternative approaches.\n2. When comparing to other baselines like PPO, the reward function is not carefully designed for your use cases. I believe one can learn/design a more powerful reward function with IRL or imitation learning.", "was_revised": true, "final_justification": "The author has addressed my concerns of scalability. I have adapted my scores accordingly.", "rebuttal": "# Reviewer 16CQ\n\nThank you very much for your thoughtful and constructive review. We truly appreciate the time and care you dedicated to reading our paper. Below, we provide clarifications and detailed responses to each of your questions and concerns.\n\n## Clarifications\n\n1.\t**Comparison with IRL/Imitation Learning:**\nHYPRL operates without expert demonstrations, unlike IRL or imitation learning, which rely on such inputs. That is, HYPRL is specification-guided, while IRL/Imitation learning are demonstration-guided. Since the assumptions and goals differ fundamentally, a direct comparison would be inappropriate. We’ll clarify this distinction in the final version of the paper if it's accepted.\n\n2.\t**Scalability of HyperLTL Reasoning:**\nWe appreciate the reviewer’s concern. HYPRL does not involve any logical reasoning. While HyperLTL logical decision procedures such as model checking and synthesis are expensive, the core technical procedure of HYPRL (Skolemization and robustness-based reward shaping) is based on typical numerical computations and is interactable. We’ll emphasize this important point if our paper is accepted.\n\n\n## Response to Detailed Comments\n\n> [W1] While HyperLTL is natural ... expensive to solve ... scalability of the HYPRL approach ... and how it compares to alternative approaches.\n\nThank you for this question. We do not expect any significant scalability issues in HYPRL in either the skolemization or computation of robustness functions. HyperLTL is computationally expensive in exhaustive decision procedures, such as model checking and synthesis, but our approach does not require any such decision procedure. Regarding comparable approaches in terms of scalability, to the best of our knowledge, there is no prior work that synthesizes policies to **maximize the probability of satisfying an arbitrary hyperproperty using RL**. Moreover, while there are studies that use temporal logics, they either cannot be applied in MARL settings, or cannot reason about inter-agent dependencies. Please refer to page 2, lines 59–67, and page 3, lines 68–79 for elaborations.\n\n> [W2] When comparing ... IRL or imitation learning.\n\nIn both IRL and Imitation Learning (e.g., [1], [2]), one of the inputs to the system is a set of traces performed by expert agents. In HYPRL, we do not assume access to such expert traces. Instead, we use a HyperLTL formula that captures all the system requirements and aim to synthesize optimal policies that sample sets of traces which maximize the probability of satisfying the HyperLTL formula. Therefore, we believe that **comparing IRL or IL with HYPRL is not an apple-to-apple comparison** due to the different system inputs. In addition, in all our experiments, except for DST (where we use the original reward function from citation [35]), we have tried several reward functions that consider the requirements of the problem for fair comparison and report the *best one* as the baseline (please check Section E of the appendix for elaborations on these reward functions).\n\n[1] Lin, Xiaomin, Stephen C. Adams, and Peter A. Beling. \"Multi-agent inverse reinforcement learning for certain general-sum stochastic games.\" Journal of Artificial Intelligence Research 66 (2019)\n\n[2] Yang, Fan, et al. \"Bayesian multi-type mean field multi-agent imitation learning.\" Advances in Neural Information Processing Systems 33 (2020)\n\n## Questions\n\n> [Q1] How does the complexity ... any theoretical bounds or empirical insights ...?\n\nThank you for pointing this out. We acknowledge that HYPRL does not provide theoretical bounds or guarantees. In the SRL example, where we have a reachability goal accompanied by a safety constraint, HYPRL improved upon the shielding baseline in terms of steps required to reach the goal by up to 85\\% (i.e., 75.2 for CQ+Shield and 11.90 for CQ+HYPRL in the Pentagon case) while also preserving safety in two cases (i.e., SUNY and MIT, CQ+HYPRL both guarantee 0.0 collisions). Our improvements are not limited to planning benchmarks; we also observed significant gains in solving the PCP problem, which is undecidable. In the setting with six dominos, HYPRL drastically outperformed the ad-hoc reward mechanism, solving more than 150 instances within 1,000 episodes, whereas the ad-hoc approach could not solve any. These experiments provide empirical insight into how HYPRL accelerates learning in multi-agent settings with relational dependencies.\n\n## Additional Experiment\n\nWe conducted additional experiments on the Wildfire domain with larger grids to better support reviewer’s concern regarding the scalability of HYPRL and provide more empirical insights (on [Q1]). We believe Wildfire is a challenging problem due to its complex constraints and requirements, and expanding the domain significantly increases the difficulty of the problem, making it a suitable setting to demonstrate scalability. \n\nThe table below reports the averages and standard errors over 10 trials, each consisting of 5k episodes, repeated across 10 runs. We set the time-out (T/O) to 20,000 steps for the $8 \\times 8$ grid experiments and 30,000 steps for the $10 \\times 10$ grid experiments, respectively.\n\n|Grid| Method    | Dist | Step $ O_1 $    | Step $ O_2 $  | \n| -------- | -------- | ------- | -------- | ------- |\n8 * 8 | PPO  | 11.27 ± 0.03    | 16801.8 ± 2144.0 | T/O    |\n8 * 8| PPO + HYPRL | **6.94** ± 0.07    | **4149.6** ± 1743.1 | **386.2** ± 80.5     |\n10 * 10 | PPO  | 10.90 ± 0.01    | T/O | 29023.6 ± 976.4   |\n10 * 10| PPO + HYPRL | **5.39** ± 0.06    | **21272.8** ± 3579.0 | **570.3** ± 52.2    |\n\n\n**If our responses have addressed your initial comments, we respectfully ask you to consider raising the score.**"}, {"review_id": "vbqJ4wbicu", "reviewer": "Reviewer_McAK", "summary": "This paper proposes HypRL, a reinforcement learning framework that learns multi-agent control policies guided by specifications written in HyperLTL, a logic for expressing properties over multiple execution traces. Unlike traditional approaches that rely on manually crafted rewards, HypRL derives reward signals from logical robustness values, enabling it to handle complex relational constraints between agents.\n\nThe framework uses Skolemization to manage quantifier alternation in HyperLTL and trains policies using standard RL algorithms. Evaluations across tasks like Deep Sea Treasure, and the Post Correspondence Problem show that HypRL significantly outperforms standard RL baselines.", "questions": "Do the authors have any intuition or preliminary ideas on how HypRL could be extended to handle partially observable environments?", "limitations": "yes", "rating": 5, "confidence": 2, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 2, "significance": 2, "originality": 3, "strengths_and_weaknesses": "## Strengths\n- [S1] The wildfire scenario offers an intuitive and accessible introduction to the problem and why standard reward shaping fails.\n- [S2] The method uses HyperLTL and Skolemization to define a novel, theoretically grounded framework for learning multi-agent policies under complex constraints.\n- [S3] The paper avoids ad hoc reward engineering by using logical robustness values as a principled reward signal.\n\n## Weaknesses\n- [W1] The environments, while varied, are still relatively small in size and abstraction. It would be valuable to evaluate HypRL on more complex domains, if possible.\n- [W2] Although HypRL outperforms PPO in the wildfire scenario, the number of steps required remains large compared to the optimal policy, raising concerns about sample efficiency and scalability.\n- [W3] The technical content, especially the use of Skolemization and robustness evaluation, is quite dense and may hinder accessibility for a broader audience.", "was_revised": true, "final_justification": "After considering the author response and discussion, I have increased my score by 1. The authors addressed my main concerns as follows:\n- Additional experiments on larger grid sizes demonstrate improved scalability.\n- Clarifications show HYPRL improves performance within the same training budget.\n- The authors outlined a clear path toward extending HypRL to Dec-POMDPs, which is a promising direction.\n- While the paper remains dense, the authors plan to enhance accessibility in the final version.\n\nOverall, the paper presents a novel and technically sound approach.", "rebuttal": "# Reviewer McAK\n\n\nThank you very much for your thoughtful and constructive review. We truly appreciate the time and care you put into reading our paper. Below, we provide detailed responses to each of your questions and concerns.\n\n## Clarifications\n\n1.\t**Complex Domain:**\nWe thank the reviewer for this suggestion. We have added experiments on larger grids ($8 \\times 8$ and $10 \\times 10$, see details below) for the Wildfire domain to demonstrate HYPRL’s effectiveness in more complex environments. If the paper is accepted, we will ensure these results are clearly highlighted in the final version.\n\n2.\t**Extension to Partially Observable Environments:**\nWhile this paper focuses on MDPs, the HYPRL framework is naturally extendable to Dec-POMDPs, allowing for reasoning under partial observability. We will be sure to include a discussion of this promising direction in the final version if accepted.\n\n\n## Response to Detailed Comments\n\n> [W1] The environments, while varied, ... complex domains, if possible.\n\nYes, we agree that the environments in our experiments are abstracted due to limited computational power. However, we aimed to include a variety of experiments to address this limitation. For example, the SRL environments are standard and widely used benchmarks in the (Safe) RL community (e.g., [1], [2], [3]). Furthermore, cases such as the PCP remain challenging to handle because the underlying problem is **undecidable**. Regarding the wildfire domain, for this rebuttal, we extended the environment to $8 \\times 8$ and $10 \\times 10$ grids (2 victims and 3 firezones). The table below reports the averages and standard errors over 10 trials, each consisting of 5k episodes, repeated across 10 runs. We set (T/O) to 20,000 steps for the $8 \\times 8$ grid experiments and 30,000 steps for the $10 \\times 10$ grid experiments, respectively.\n\n\n|Grid| Method    | Dist | Step $ O_1 $    | Step $ O_2 $  | \n| -------- | -------- | ------- | -------- | ------- |\n8 * 8 | PPO  | 11.27 ± 0.03    | 16801.8 ± 2144.0 | T/O    |\n8 * 8| PPO + HYPRL | **6.94** ± 0.07    | **4149.6** ± 1743.1 | **386.2** ± 80.5     |\n10 * 10 | PPO  | 10.90 ± 0.01    | T/O | 29023.6 ± 976.4   |\n10 * 10| PPO + HYPRL | **5.39** ± 0.06    | **21272.8** ± 3579.0 | **570.3** ± 52.2    |\n\n\n[1] ElSayed-Aly, I., Bharadwaj, S., Amato, C., Ehlers, R., Topcu, U., & Feng, L. (2021). Safe multi-agent reinforcement learning via shielding.\n\n[2] Melo, F. S., & Veloso, M. (2009, May). Learning of coordination: Exploiting sparse interactions in multiagent systems.\n\n[3] Melcer, D., Amato, C., & Tripakis, S. (2022). Shield decentralization for safe multi-agent reinforcement learning.\n\n> [W2] Although HYPRL outperforms PPO in the wildfire scenario ... sample efficiency and scalability.\n\nThank you for this comment. The purpose of this experiment is to demonstrate that, **under the same number of training episodes, HYPRL+PPO outperforms PPO**. This suggests that, given the same training budget, HYPRL guides the agents to achieve the task objectives quicker. The wildfire scenario is particularly challenging because each agent has multiple objectives that are dependent (i.e., the FireFighter drone must extinguish fire zones, while the medical drone must rescue victims, and a victim may locate in a fire zone). In addition, they must satisfy complex constraints (i.e., maintaining a safe distance, while ensuring that the medical drone does not enter fire zones before the firefighter extinguishes the fires). These requirements make solving this problem challenging and hence, require training over a large number of episodes.\n\n> [W3] The technical content ... is quite dense and may hinder accessibility for a broader audience.\n\nThank you for this comment. We agree the technical content is dense, but the mathematical rigor is necessary to ensure soundness. To support the reader, we have included additional material in the appendix. If the paper is accepted (which allows an extra page in the camera-ready version), we will use the additional space to provide further explanation and illustrative examples to improve readability.\n\n## Questions\n\n> [Q1] Do the authors have any intuition or preliminary ideas on how HYPRL could be extended to handle partially observable environments?\n\nWe sincerely thank the reviewer for this insightful and forward-looking perspective on HYPRL. We are, in fact, currently working on partial observability. We believe HYPRL offers a strong theoretical foundation with the potential to open an exciting new line of research. Extending the current setting from MDPs to Decentralized Partially Observable Markov Decision Process (i.e., Dec-POMDPs) would not only allow HYPRL to handle partially observable environments but also address scalability challenges inherent to centralized training. As a preliminary direction, we envision replacing full environment states with **belief states** for trace sampling, while retaining HYPRL’s foundations to evaluate those traces and provide meaningful feedback to the learning algorithm.\n\n\n\n\n\n**If our responses have addressed your initial comments, we respectfully ask you to consider raising the score.**"}, {"review_id": "Flv59o2C0q", "reviewer": "Reviewer_xQCo", "summary": "This paper introduces a novel formal specification guided multi-agent reinforcement learning (MARL) framework where specifications are given as hyperproperties. In particular, they adopt the HyperLTL logic which extends LTL with existential and universal quantifiers over  traces. The authors claim that HyperLTL, in the context of MARL, allows greater flexibility in specifying interdependencies between agent behaviors using quantifier alternations and they demonstrate this with a relevant example. Their method involves first considering a Skolemized version of the specification and using some quantitative semantics of LTL as a reward to train off-the-shelf RL algorithms that gives a centralized policy producing actions for all the agents. They implement their method and test it on three discrete environments.", "questions": "My main confusion is about the problem formalization and problem statement. If we have just a single MDP, what does it mean to synthesize multiple policies? How does the quantifier alternation affect optimization?", "limitations": "yes", "rating": 4, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 2, "clarity": 1, "significance": 2, "originality": 3, "strengths_and_weaknesses": "Strengths\nThe introduction of hyperproperties in the context of multi-agent reinforcement learning has not been explored before to the best of our knowledge so this is indeed a novel direction.\n\nWeaknesses\nFirstly, we believe that the problem statement and the benchmarks used do not show the utility of using hyperproperties. In the current formulation of the problem statement (page 4), it is unclear what is the role of the quantifier alternation because it is trying to maximize the probability that a tuple of traces sampled from the agents' policies together satisfy the specification. In particular, this probability is not dependent on the quantifiers in the specification.\n \nConsider the case of the motivating example used in the introduction. Here, we could define the same specification as an LTL formula over a zipped trace of the firefighter and medical agents and the problem statement would remain the same. This is also the case with all the other benchmark specifications that are considered. In fact, the final policy produced also does not depend on the quantifiers since it is a centralized policy that predicts actions simultaneously for all the agents.  \n\nTo make this more concrete, if we fix the policies for all the agents, then we can resolve the MDP into a Markov chain for each agent. Then the quantifier-free LTL part of the specifications presented in this paper can be seen as an LTL formula over the product of these Markov chains. So these specifications do not define hyperproperties over this product Markov chain. In other words, interdependence between traces in the Markov chains of each agent specified with an LTL formula is not a hyperproperty. Furthermore, if we did want to consider hyperproperties over the product, it is unclear whether HyperLTL has well defined probabilistic semantics over a Markov chain. We refer to Abraham and Bonakdarpour [1] and Dimitrova et al [2] who define different probabilistic temporal logics to specify hyperproperties over Markov chains and MDPs respectively.\n\nThe above problem is accompanied by a lack of a sound and complete formalization. Despite multi-agent reinforcement learning being the focus of the paper, the initial definitions do not specify these multiple agents and how their traces are represented in the MDP. Next, in the definition of the semantics of HyperLTL, it is stated that a tuple of traces $\\mathcal{T}$ satisfies the specification $\\forall \\pi.\\phi$, if for all $t\\in \\mathcal{T}$, $(\\mathcal{T}, \\Pi[\\pi \\to t]) \\models \\phi$, which means that $\\phi$ is satisfied by all assignments of traces to $\\pi$. However, in the remainder of the paper, the convention seems to arbitrarily shift to being such that the tuple of traces $\\mathcal{T}$ represents a sequence of assignments for the quantified variables in the formula. This again seems to point to the fact that the quantifiers play no role.\n\nFinally, the proposed training procedure does not present any novel insights since it uses off-the-shelf RL algorithms with rewards given by quantitative semantics of the LTL formula and only trains a centralized policy that controls all the agents at the same time. Essentially, the multi-agent control problem is turned into a single-agent control problem.\n\n[1] E. Abraham and B. Bonakdarpour. HyperPCTL: A temporal logic for probabilistic hyperproperties. In Quantitative Evaluation of Systems, QEST 2018, Proc., 2018.\n\n[2] Rayna Dimitrova, Bernd Finkbeiner, Hazem Torfah. Probabilistic Hyperproperties of Markov Decision Processes. In ATVA 2020.", "was_revised": true, "final_justification": "The original paper had a mistake in formalization of the problem. After extensive back-and-forth with the authors, we trust them to fix the mistake.", "rebuttal": "# Reviewer xQCo\nWe deeply thank you for your detailed feedback. We admit we made an unfortunate mistake in formalization of the problem statement, which led to your comments. We are strongly confident that this error can be fixed easily.\n## Clarifications\n1. **Probabilities and sampling** First, we clarify a misunderstanding by the reviewer. Please note that in model-free RL, the environment is given by an MDP, where the transitions are unknown to the agents but known to the environment. Since sampling is done by the agent, the transition probabilities only contribute at sampling time (i.e.,transitions with higher probabilities are more likely to appear in sampled traces). After sampling, we have set(s) of traces, and the transition probability function, no longer plays a role in evaluation of the specification or the learning process. This means logics such as HyperPCTL or PHL are irrelevant and not needed.\n2. **Problem Statement:** Each quantifier is associated to the behavior of an agent. Our goal is to identity a policy per quantifier such that the induced sampled traces are more likely to satisfy the specification. This likelihood (i.e., probability $\\mathbb{P}$ in the problem statement) is simply measured by counting the number of cases where sampled traces satisfy the specification divided by the total number of evaluations. Since a policy renders a distribution (i.e., a DTMC), we will easily modify the semantics of HyperLTL to account for choosing traces for each quantifier from the distribution induced by the associated policy.\nLet an *interpretation* be $\\mathcal{T} =\\langle T_{\\tau_i}\\rangle_{i \\in\\lbrace1,\\ldots,|\\mathit{Vars}(\\varphi)|\\rbrace}$, where each $\\tau_i$ (associated with agent $i$) ranges over a set $T_{\\tau_i}$ of traces induced by policy $\\pi_i$. This ensures that agent-specific behaviors and quantifier alternations are correctly represented during evaluation. We will mend the semantics of the universal quantifier (analogously for $\\exists$) as follows:\n$$(\\mathcal{T}, \\Pi, 0)\\models\\forall\\tau\\,\\psi\\quad\\text{iff}\\quad\\text{for all }t\\in T_{\\tau}\\text{ such that }(\\mathcal{T},\\Pi[\\tau\\rightarrow t],0)\\models\\psi$$\nNow, consider formula $\\varphi=\\forall\\tau _ 1.\\exists\\tau _ 2.\\psi$, where our goal is to identify policies $\\pi^* _ 1$ and $\\pi^* _ 2$, such that the sets of sampled traces $T_{\\tau_1}$ and $T_{\\tau_2}$ from the induced DTMCs (which we denote by \"distributions\" $\\mathcal{D _ {\\pi_i}}$), are more likely to satisfy $\\varphi$ among all other policies. Formally, $\\tau _ i$ for $i \\in\\lbrace 1,2\\rbrace$ ranges over $T _ {\\tau _ i} = \\mathsf{Traces}(\\mathcal{Z} _ {\\tau _ i}\\sim\\mathcal{D} _ {\\pi_i})$, where each $\\mathcal{Z} _ {\\tau _ i}$ is a set of traces sampled from the distribution induced by policy $\\pi_i$. The correct formal problem statement will be:\n$$\\langle \\pi_i^\\star\\rangle_{i\\in\\lbrace1,\\ldots,n\\rbrace}\\in \n\\Big[ \\arg\\max _ {\\langle\\pi_i\\rangle} \n\\mathbb{P}\\left(\\langle \\mathsf{Traces}(\\mathcal{Z} _ {\\tau_i}\\sim\\mathcal{D} _ {\\pi_i})\\rangle\\models\\varphi\\right) \n\\Big] _ {i\\in\\lbrace1,\\ldots,n\\rbrace}$$\nSubsequent sections will be revised easily by replacing all instances of $\\mathsf{Tr}(\\zeta_i)$ by $\\mathsf{Traces}(\\mathcal{Z} _ {\\tau_i}\\sim\\mathcal{D} _ {\\pi_i})$. \n1. **Illustrative Example:**  We will add the following example to explain all the concepts more clearly using the additional page. Consider the MDP below for a $3\\times3$ grid (Fig.1), where each state is $<x,y>$ with $x,y \\in\\lbrace 0,1,2\\rbrace $, labeled by $\\lbrace a,b,...,i\\rbrace$, and $act=\\lbrace0,1,2,3\\rbrace$.\n```\n  <2,0>(a)\n   /  \\\n  0    1  \n  ↓    ↓  ↘\n  1   .5   .5\n  ↓   ↙      ↘\n<2,1>(b)   <1,0>(d)  \n/   \\      ↗  | \\  ↖     \n3    0    1 ← 0  1   ↖\n↓    ↓ ↘         ↓     ↖\n1   .5  .5       1       1\n↓   ↙     ↘       ↘         ↖\n<1,1>(e) <2,2>(c)  <0,0>(g) - 0\n  |  \\     |\n  3   0    1\n  ↓   ↓    ↓                         \n  1   1    1\n  ↓    ↘   ↓\n<0,1>(h) <1,2>(f)\n  |        |\n  1        3\n  ↓        ↓\n  1        1\n   ↘      ↙\n   <0,2>(i) \n```\nSuppose agent $A$ with $\\pi _ 1$ draws samples $\\mathcal{Z} _ {\\tau _ 1} =\\lbrace\\zeta^1_A,\\zeta^2_A\\rbrace$ from the above MDP (the number of samples can be more than 2):\n$$\\zeta_A^1:\\underbrace{\\langle 2,0\\rangle} _ {a}\\overset{\\text{0}}{\\rightarrow}\\underbrace{\\langle2,1\\rangle} _ {b} \\overset{\\text{0}}{\\rightarrow}\\underbrace{\\langle 2,2\\rangle} _ {c}\\overset{\\text{1}}{\\rightarrow}\\underbrace{\\langle 1,2\\rangle} _ {f}\\overset{\\text{3}}{\\rightarrow}\\underbrace{\\langle0,2\\rangle} _ {i}$$\n$$\\zeta_A^2:\\underbrace{\\langle 2,0\\rangle} _ {a}\\overset{\\text{0}}{\\rightarrow}\\underbrace{\\langle2,1\\rangle} _ {b}\\overset{\\text{0}}{\\rightarrow}\\underbrace{\\langle 1,1\\rangle} _ {e}\\overset{\\text{3}}{\\rightarrow}\\underbrace{\\langle 0,1\\rangle} _ {h}\\overset{\\text{1}}{\\rightarrow}\\underbrace{\\langle0,2\\rangle} _ {i}$$  \nAgent $B$ with policy $\\pi _ 2$ draws $\\mathcal{Z} _ {\\tau _ 2} =\\lbrace \\zeta^1_B,\\zeta^2_B\\rbrace$:  \n$$\\zeta_B^1:\\underbrace{\\langle 2,0\\rangle} _ {a}\\overset{\\text{1}}{\\rightarrow}\\underbrace{\\langle1,0\\rangle} _ {d}\\overset{\\text{1}}{\\rightarrow}\\underbrace{\\langle 0,0\\rangle} _ {g}\\overset{\\text{0}}{\\rightarrow}\\underbrace{\\langle 1,0\\rangle} _ {d}\\overset{\\text{0}}{\\rightarrow}\\underbrace{\\langle1,0\\rangle} _ {d}$$\n$$\\zeta_B^2:\\underbrace{\\langle 2,0\\rangle} _ {a}\\overset{\\text{1}}{\\rightarrow}\\underbrace{\\langle2,1\\rangle} _ {b}\\overset{\\text{3}}{\\rightarrow}\\underbrace{\\langle 1,1\\rangle} _ {e} \\overset{\\text{0}}{\\rightarrow}\\underbrace{\\langle 1,2\\rangle} _ {f} \\overset{\\text{3}}{\\rightarrow}\\underbrace{\\langle0,2\\rangle} _ {i}$$\nNow, consider the following HyperLTL formula:\n$$\\varphi _ {\\mathsf{exp}}\\triangleq\\forall\\tau _ 1.\\exists\\tau _ 2.\\Big(\\Diamond i _ {\\tau _ 1}\\wedge\\Box dist(\\langle x,y\\rangle_ {\\tau _ 1},\\langle x, y\\rangle_ {\\tau _ 2})<3\\Big)$$\nWe calculate the probability of satisfying $\\varphi $ using $\\mathcal{Z}_{\\tau_1}$ and $\\mathcal{Z} _ {\\tau _ 2}$ (obtained by $\\pi _ 1$ and $\\pi _ 2$) as follows:\n$$\\mathsf{Traces}(\\langle\\lbrace \\zeta_A^1\\rbrace,\\mathcal{Z} _ {\\tau _ 2}\\rangle)\\models\\varphi _ {\\mathsf{exp}} ~(\\text{where } \\zeta_B^2\\text{ is a witness to } \\exists\\tau _ 2)$$\n$$\\mathsf{Traces}(\\langle\\lbrace \\zeta_A^2\\rbrace,\\mathcal{Z} _ {\\tau _ 2}\\rangle)\\models\\varphi _ {\\mathsf{exp}} ~(\\text{where } \\zeta_B^2\\text{ is a witness to } \\exists\\tau _ 2)$$\n\nHence: \n$$\\mathbb{P} _ {\\langle \\pi _ 1, \\pi _ 2\\rangle}\\Big[ \\mathsf{Traces}(\\langle\\mathcal{Z} _ {\\tau _ 1},\\mathcal{Z} _ {\\tau _ 2}\\rangle)\\models\\varphi _ {\\mathsf{exp}}\\Big]=1$$\nAgain, note that, computing the probability in the problem statement ($\\mathbb{P}$) is not related to the probability distributions of the MDP.\nNow, if $\\varphi _ {\\mathsf{exp}}$ was of the form $\\forall\\forall$, evaluation has to go over all combinations between traces between $\\mathcal{Z} _ {\\tau _ 1}$ and $\\mathcal{Z} _ {\\tau _ 2}$, that is:\n$$\\mathsf{Traces}(\\langle\\lbrace\\zeta_A^1\\rbrace,\\lbrace\\zeta_B^1\\rbrace\\rangle)\\not\\models\\varphi _ {\\mathsf{exp}}\n~\\mathsf{Traces}(\\langle\\lbrace\\zeta_A^1\\rbrace,\\lbrace\\zeta_B^2\\rbrace\\rangle)\\models\\varphi _ {\\mathsf{exp}}$$\n$$\\mathsf{Traces}(\\langle\\lbrace\\zeta_A^2\\rbrace,\\lbrace\\zeta_B^1\\rbrace\\rangle)\\not\\models\\varphi_{\\mathsf{exp}} \n~\\mathsf{Traces}(\\langle\\lbrace\\zeta_A^2\\rbrace,\\lbrace\\zeta_B^2\\rbrace\\rangle)\\models\\varphi_{\\mathsf{exp}}$$\nThus, the probability of satisfaction of $\\forall\\forall\\psi$ would have been 0.5. This example illustrates that the probability of satisfying the HyperLTL formula depends on the form of quantifiers in the given HyperLTL formula.\n## Response to Detailed Comments and Question\n> [C1] Firstly...Problem Statement...depend on the quantifiers...agents.\n\n> [C2] To make... product of these Markov chains...LTL is not a hyperproperty.\n\n> [C4] In the definition...(T,Π[π→t])⊨ϕ...fact that the quantifiers play no role.\n\nAs explained above, after mending the semantics of $\\forall$ and $\\exists$ to multi-model and the problem statement, quantifier alternation plays a crucial role in evaluation of $\\varphi$ and computing $\\mathbb{P}$. The product of the induced DTMCs and verifying an LTL formula can only solve the problem for alternation-free formulas.\n> [C3] Furthermore,...[1] and [2]...problem is accompanied...in the MDP.\n\nAs noted in the clarification, MDP probabilities are not used in evaluating $\\varphi$ and logics such as HyperPCTL[1] or PHL[2] are irrelevant.\n> [C5] Finally, the proposed training procedure does not...single-agent control problem.\n\nOur solution renders a multi-agent solution, but with a centralized controller. We introduce a general reward shaping framework that can be integrated with any off-the-shelf RL algorithm. We do not propose a new RL algorithm and in fact, we do not intend to. Synthesizing a decentralized controller is a whole different line of work. We believe our work is the first step towards hyperproperty-based RL and future papers will study more complex variations. One cannot solve all problems in the first step.\n\n> [Q] Confusion...problem statement...single MDP...? How does the quantifier...?\n\nWe again sincerely thank the reviewer for carefully reading the paper and providing constructive feedback. We hope our clarification section addresses the core concerns. \n## Plans to Resolve the Confusions\nIf the paper is accepted, we will obviously fix the mistake and use the additional page to elaborate:\n(1) how the probability of satisfaction of the multi-model semantics HyperLTL formula is calculated using the above example;\n(2) explain the key role of quantifier alternation and how this quantifier alternation affects the calculation of probabilities and consequently affects the optimization problem.\nWe believe these minor revisions will resolve the reviewer’s concerns and significantly improve the clarity of the technical meat (Sec. 3–4).\n\n**If our responses have addressed your initial comments and points of confusion, we respectfully ask you to consider raising the score.**"}]

Author rebuttal:

Meta-review: The paper proposes a specification-guided MARL framework that uses HyperLTL to express relational objectives across agents, applies Skolemisation to handle quantifier alternation, and converts formula robustness into a scalar reward usable by standard RL under centralised training. Across multiple environments, HYPRL improves learning efficiency and outcomes over baselines. During rebuttal the authors corrected inconsistencies in the formal problem statement, clarified evaluation over sets of sampled joint traces and added evidence on larger tasks and a three-agent setting; these clarifications and results led multiple reviewers to raise their scores.

Overall the paper is not without its problems: claims of scalability are only partly demonstrated (small environments, limited agent counts, and centralised training), the formulation assumes full observability rather than (Dec-)POMDPs, and the original presentation contained semantic inconsistencies that must be corrected. However, it *is* the first to bring hyperproperties to MARL in a practical way, using HyperLTL to provide principled, algorithm-agnostic reward shaping that reduces ad hoc engineering, with consistent improvements under the same training budget and added evidence on larger grids and a three-agent setup.

Given that the paper is the first to propose the framework, I feel that the shortcomings, though present, need not be addressed in this work. I encourage the authors to include the additional results and corrected semantics in the finalised version of the paper.
Decision: Accept (poster)