Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees
Authors: Đorđe Žikelić
Mathias Lechner
Abhinav Verma
Krishnendu Chatterjee
Thomas A Henzinger
Venue: NeurIPS 2023 poster (2023)
Keywords: Verification
Compositional learning

Abstract: Reinforcement learning has shown promising results in learning neural network policies for complicated control tasks. However, the lack of formal guarantees about the behavior of such policies remains an impediment to their deployment. We propose a novel method for learning a composition of neural network policies in stochastic environments, along with a formal certificate which guarantees that a specification over the policy's behavior is satisfied with the desired probability. Unlike prior work on verifiable RL, our approach leverages the compositional nature of logical specifications provided in SpectRL, to learn over graphs of probabilistic reach-avoid specifications. The formal guarantees are provided by learning neural network policies together with reach-avoid supermartingales (RASM) for the graph’s sub-tasks and then composing them into a global policy. We also derive a tighter lower bound compared to previous work on the probability of reach-avoidance implied by a RASM, which is required to find a compositional policy with an acceptable probabilistic threshold for complex tasks with multiple edge policies. We implement a prototype of our approach and evaluate it on a Stochastic Nine Rooms environment.

Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees
Dorde Žikelić*
Mathias Lechner"
Institute of Science and Technology Austria (ISTA)
Massachusetts Institute of Technology
Klostemeuburg, Austria
Cambridge, MA, USA
srndje.zikelic@0n ac.at
mlechnerGmit.cr edu
Abhinav Verma
Krishnendu Chatterjee
The Pennsylvania State University University Park, PA, USA verma@psu.ed edu
Institute of Science and Technology Austria (ISTA)
Klosterneuburg, Austria
krishnendu. www.aanddu.caatttrjeeeeiseeeeeee ac.at
Thomas A. Henzinger
Institute of Science and Technology Austria (ISTA)
Klosterneuburg, Austria
ac.
Abstract
Reinforcement learning has shown promising results in learning neural network policies for complicated control tasks. However, the lack of formal guarantees about the behavior of such policies remains impediment to their deployment. We propose novel method for learning a composition of neural network policies in stochastic environments, along with formal certificate which guarantees that a specification over the policy's behavior is satisfied with the desired probability. Unlike prior work on verifiable RL, our approach leverages the compositional nature of logical specifications provided in SPECTRL, to learn over graphs of prob- abilistic reach-avoid specifications. The formal guarantees are provided by learning neural network policies together with reach- avoid supermartingales (RASM) for the graph's 's sub-tasks and then composing them into a global policy. We also derive a tighter lower bound compared to previous work on the probability of reach-avoidance implied by a RASM, which required to find compositional policy with an acceptable probabilistic threshold for complex tasks with multiple edge policies. We implement a prototype of our approach and evaluate it on a Stochastic Nine Rooms environment.
Introduction
Reinforcement learning (RL) has achieved promising results in variety of control tasks. However, the main objective of RL is to maximize expected reward (56] which does not provide guarantees of the system' safety. more recent paradigm in safe RL considers constrained Markov decision 3 21. that in addition to reward function are also equipped with cost function. The goal solving cMDPs to maximize expected reward while keeping expected cost below some tolerable threshold. Recently, keeping cost below the threshold almost-surely and not only expectation was considered [52] While these methods do enhance safety, they only empirically
processes (cMDPs) SS] 26
'Equal contribution.
37th Conference on Neural Information Processing Systems (NcurIPS 2023).

---

try to minimize cost and do not provide guarantees on cost constraint satisfaction. The lack of formal guarantees raises a significant barrier to deployment of these methods in safety-critice applications, where the policies often need to encode complicated, long-horizon reasoning to accomplish task in an environment which unsafe behavior can lead to catastrophic consequences [6]
Recent work [13 32 33 has explored decomposing high-level logical specifications, belonging to different fragments of Linear Temporal Logic (LTL) [4], into simpler logical specification tasks that RL algorithms can solve more easily. In particular, these methods first decompose the high-level logical specification into a number of simpler logical specifications, then learn policies for these simpler tasks and finally compose the learned policies for each task into global policy that solves the high-level control problem at hand. The simpler control tasks are solved by designing reward functions which faithfully encode the simpler logical specifications obtained by the decomposition and using an offelhe-shelf RI. algorithm to solve them.
While these methods present significant advances in deploying RL algorithms for solving complex logical specification tasks, their key limitation is that they also do not provide formal guarantees on the probability of satisfying the logical specification which are imperative for safety-critical applications. This is because reward functions often only "approximate" logical specification objectives, and furthermore RL algorithms are in general not guaranteed to converge to optimal policies over continuous state spaces. Recently, 330 have proposed verification procedures for formally verifying a composition of neural network policies with respect to given system dynamics model. However, these works assume that the underlying control systems have deterministic dynamics. This does not allow modelling stochastic disturbances and uncertainty in the underlying system dynamics. Furthermore, [62 assumes that the underlying control system has linear dynamics function whereas many control tasks have non-linear dynamics.
In this work we propose CLAPS (Compositional Learning for Probabilistic Specifications), new compositional algorithm for solving high-level logical specification tasks with formal guarantees on the probability of the specification being satisfied. We present a method for learning and verifying a composition of neural network policies learned via RL algorithms, which is applicable to stochastic control systems that may be defined via non-linear dynamics functions. Our method only requires that the underlying state space of the system is compact (i.c. closed and bounded) and that the dynamics function of the system is Lipschitz continuous. In terms of the expressiveness of logical specifications, CLAAPS considers the SPECTRL specification language [32. SPECTRL contains all logical specifications that can be obtained by sequential and disjunctive compositions of reach-avoid specifications. Given target and an unsafe region, a reach-avoid specification requires that the system reaches the target region while avoiding the unsafe region.
Our method learns policy along with a formal certificate which guarantees that a specification is satisfied with the desired probability. It consists of three key ingredients (1) high-level planning on directed acyclic graph (DAG) that decomposes the complex logical specification task into sequentially or disjunctively composed low-level reach-avoid tasks, (2) learning policies that solve low-level reach-avoid tasks with formal guarantees on the probability of satisfying reach-avoidance, and (3) composing the low-level reach-avoid policies into a global policy for the high-level task by traversing edges in the DAG. This yields fully compositional algorithm which only requires solving control problems with reach-avoid constraints, while performing high-level planning.
To solve the low-level reach-avoid tasks, we leverage and build upon the recent learning algorithm for stochastic control under reach-avoid constraints (68) This work achieves formal guarantees on the probability of reach-avoidane (RASM), which serves as a formal certificate of probabilistic reach-avoidance. When composing such guarantees for a global probabilistic specification we encounter two fundamental challenges, (i) reducing the certification of unnecessary individual reach-avoid constraints that are not critical for global satisfaction, and (ii) reducing the violation probabilities for individual reach-avoid constraints to improve the possibility of satisfaction of the composed policy. We overcome the first challenge by leveraging the DAG decomposition of complex specifications and by performing forward pass on the DAG which learns edge policies on-demand, and the second one by showing that RASMs prove a strictly tighter lower bound on the probability of reach-avoidance than the bound that was originally proved (68) Our novel bound multiplies the bound of [68] by an exponential asymptotic decay term. This is particularly important when composing large number of edge policies for complex
by learning policy together with reach-avoid supermartingale
2

---

objectives. Furthermore, our new bound is of independent interest and it advances state of the art in stochastic control under reach-avoid constraints.
Contributions Our contributions can be summarized as follows:
1. We prove that RASMs imply a strictly tighter lower bound on the probability of reach- avoidance compared to the bound originally proved in [68] (Section
2. We propose novel method for learning and verifying a composition of neural network policies in stochastic control systems learned in the RL paradigm, which provides formal guarantees the probability of satisfaction of SPECTRL specifications (Section 5).
3. We implement a prototype of our approach and evaluate it on the Stochastic Nine Rooms environment, obtained by injecting stochastic disturbances to the environment of [33. Our experiments demonstrate both the necessity of decomposing high-level logical specifications into simpler control tasks well as the ability of our algorithm to solve complex specification tasks with formal guarantees (Section 6).
2 Related Work
Learning from logical specifications Using high-level specifications with RL algorithms has been
(60] among others. These approaches typically use the specification to guide the reward objective used by RL algorithm to learn policy but usually lack formal guarantee on the satisfaction of the specification. Approaches that provide guarantees on the probability of satisfaction in finite state MDPs have been proposed in
explored [3 32 33
39
43
28 29]
In contrast, we consider stochastic
systems with continuous state spaces.
Control with reachability and safety guarantees Several works propose model- based methods for learning control policies that provide formal guarantees with respect to reachability, safety and reach-avoid specifications. The methods of [2] 16 17
55 I consider deterministic systems and learn a policy together with a Lyapunov or barrier function that guarantees reachability or safety, Control of finite-time horizon stochastic systems with reach-avoid guarantees has been considered in [14, 36 53 61]. These methods compute a finite-state MDP abstraction of the system and solve the constrained control problem for the MDP. The works of [9] [0] consider infinite- timi horizon stochastic systems with linear dynamics and propose abstraction-
48
methods that provide probably approximately correct (PAC) guarantees. Control of polynomial stochastic systems via stochastic
barrier functions and convex optimization was considered 46 49
65 42). Learning- based methods
providing formal guarantees for infinite time horizon stochastic systems that not necessarily polynomial have been proposed in [38 68 20). The work [8] proposes a learning bearning-based method for providing formal guarantees on probability 1 stabilization. To the best of our knowledge, the compositionality of our CLAPS makes it the first method that provides formal guarantees for infinite time horizon stochastic systems with respect to expressive specifications.
Safe exploration RL algorithms fundamentally depend on exploration in order to learn high per- forming actions. A common approach to safe exploration RL is to limit exploration within a high probability safety region which is computed by estimating uncertainty bounds. Existing works achieve this by using Gaussian Processes
34
59] linearized models [2]] robust regression (40)
Bayesian neural networks [37], shielding
4
31 and state augmentation [51].
Model-free methods for stochastic systems The recent work of 66 proposed a model-free approach to learning policy together with a stochastic barrier function, towards enhancing probabilistic safety of the learned policy. Unlike our approach, this method does not formally verify the correctness of the stochastic barrier function hence does not provide any guarantees on safety probability. However, does not assume the knowledge of the system environment and is applicable in model-free fashion. Several model-free methods for learning policies and certificate functions in deterministic systems have also been considered, see [4 for a survey.
Statistical methods Statistical methods [67] provide an effective approach to estimating the proba- bility of specification being satisfied, when satisfaction and violation of the specification can be witnessed via finite execution traces. Consequently, such methods often assume a finite-horizon or the existence of a finite threshold such that the infinite-horizon behavior is captured by traces within that threshold. In environments where these assumptions do not hold, the violation of a reach-avoid (or, more generally, any SPECTRL specification can be witnessed only via infinite traces and
3

---

hence statistical methods are usually not applicable. In this work, we formdderformal verification of infinite-time horizon systems.
Supermartingales for probabilistic programs Supermartingales have also been used for the anal-
ysis of probabilistic programs (PPs) for properties such termination [5] reachability (58) and
safety 18 19I
3 Preliminaries
We consider discrete-time stochastic dynamical system whose dynamics are defined by the equation
X = [(x,, (x)),,);
where t E No is a time step. X; E 2' is a state of the system, u, = x(x,) E Li is a control action and We W is stochastic disturbance vector at the time step t. Here, X C R is the state space of the system, 4 C IR" is the action space and W C IR is the stochastic disturbance space. The system dynamics are defined by the dynamics function ʃ X' U x W X, the control policy X' + 4 and a probability distribution d over W from which a stochastic disturbance vector is sampled independently at each time step. Together, these define a stochastic feedbuck loop system.
sequence (x,, Ue wi)==o of action-disturbance triples is a trajectory of the system, we have that u (x,), Wi E support(d) and X f(x,, (xx,), wy) hold for each time step & No. For every state Xa E X, we use 9x, to denote the set of all trajectories that start in the initial state Xg- The Markov decision process (MDP) semantics of the system define probability space
the set of all trajectories in f2x, under any fixed policy π of the system [47]. We use Fx, and Ex, to denote the probability measure and the expectation operator in this probability space.
Assumptions For system semantics to be mathematically well-defined, we assume that X C R", U C I and W C IR? are all -erell and that f X' x U x W + X' and π X' + U are continuous functions. Furthermore, we assume that X' C R" is compact (i.c. closed and bounded) and that f and π are continuous functions. These are very general and standard assumptions in control theory. Since any continuous function on a compact domain is Lipschitz continuous, our assumptions also imply that f and are Lipschitz continuous.
Probabilistic specifications Let Ω denote the set of all trajectories of the system. A specification is a boolean function Φ Ω - (true, false} which for each trajectory specifies whether it satisfies the specification. We write p F= & whenever trajectory P satisfies the specification ş). A probabilistic specification is then defined as ordered pair (c) p) of specification á and probability parameter p E [0, 1] with which the specification needs to be satisfied. We say that the system satisfies the probabilistic specification (o, p) at the initial state xo X if the probability of any trajectory in Ωx satisfying ó is at least p. i.c. if IP x E 2x, P
+ Φ) 2
SPECTRL and abstract graphs Reach-avoid specifications are one of the most common and practi- cally relevant specifications appearing in safety-critical applications that generalize both reachability and safety specifications [54]. Given a target region and an unsafe region, reach-avoid specifications requires that a system controlled by a policy reaches the target region while avoiding the unsafe region. The SPECTRL specification language 32) allows specifications of reachability and avoidance objectives as well as their sequential or disjunctive composition. See Appendix A for the formal definition of the SPECTRL. syntax and semantics
was shown in 33 that SPECTRL specification can be translated into an abstract graph over reach-avoid specifications. Intuitively, an abstract graph is a directed acyclic graph (DAG) whose vertices represent regions of system states and whose edges are annotated with a safety specification. Hence, each edge can be associated with a reach-avoid specification where the goal is to drive the system from the region corresponding to the source vertex of the edge to the region corresponding to the target vertex of the edge while satisfying the annotated safety specification.
Definition (Abstract graph). An abstract graph G = (V, E, 3, 8, t) is a DAG, where V is the vertex set, E is the edge set, 9 V U E + B(X) maps each vertex and each edge to a subgoal region in X, s E V is the source vertex and t E V is the target vertex. Furthermore, we require that ((s) = Xg-
In Appendix A we also show that SPECTRL strictly subsumes all specifications belonging to the Finitary fragment of LTL, that has been shown to be the lec-mbb--earraale fragment of LTL [66]. However, the converse is not true and SPECTRL is strictly more general since avoidance not finitary.

---

Given a trajectory م = (Xt; ut wi) of the system and an abstract graph G = EV, we say that P satisfies abstract reachability for G (written p == G) if it gives rise to a path in G that traverses G from 8 to and satisfies reach-avoid specifications of all traversed edges. We formalize this notion in Appendix [ It was shown [3 Theorem 3.4] that for each SPECTRL specitication ø once can construct an abstract graph G such that for each trajectory P we have F Φ iff F G. For completeness, we provide this construction in Appendix
Problem Statement We now formally define the problem that we consider in this work. Consider
a stochastic feedback loop system defined as above and let Xo S X be the set of initial states. Let (é. p) be probabilistic specification with & being a specification formula in SPECTRL and E [o, 1] being a probability threshold. Then, our goal is to learn a policy such that the stochastic feedback loop system controlled by the policy т guarantees satisfaction of the probabilistic specification (o.p)
at every initial state Xo E Xg, i.e. that for every Xp E X, we have IF Fxx (p E Pxg | F x) 2 p.
Compositional learning algorithm Our goal is not only to learn policy that guarantees satisfaction of the probabilistic specification, but also learn such a policy in compositional manner. Given SPECTRL specification é. a probability threshold E [0. 1] and an abstract graph G of o, we say that a policy क is a compositional policy for the probabilistic specification (ø, p) if guarantees satisfaction of (Ø, p) and is obtained by composing a number of edge policies learned for reach- avoid tasks associated
edges of G. An algorithm is said be compositional for probabílistic specification (ø. p) if it learns a compositional policy for the probabilistic specification (ø, p). In this work, we present a compositional algorithm for the given probabilistic specification po)
4 Improved Bound for Probabilistic Reach-avoidance
In this section, we define reach-avoid supermartingales (RASMs) and derive an improved lower bound on the probability of reach-avoidance that RASMs can be used to formally certify. RASMs, together with a lower bound on the probability of reach-avoidance that they guarantee and method for learning a control policy and an RASM, were originally proposed in [68). The novelty in this section is that we prove that RASMs imply a strictly stronger bound on the probability of satisfying reach-avoidance, compared to the bound derived in [68]. We achieve this by proposing an alternative formulation of RASMs, which we call multiplicative RASMs. In contrast to the original definition of RASMs which imposes additive expected decrease condition, our formulation of RASMs smposse multiplicative expected decrease condition. In what follows, we define multiplicative RASMs. Then, we first show in Theorem T that they are equivalent to RASMs. Second, we show in Theorem 2 that by analyzing the multiplicative expected decrease, we can derive an exponentially lighter bound on the probability of reach-avoidane to learn policies together with multiplicative RASMs that provide strictly better formal guarantees on the probability reach-avoidance.
These two results imply that we can utilize the procedure of [68]
Prior work reach-avoid supermartingales RASMs [68] are continuous functions that assign real values to system states, are required to be nonnegative and to satisfy the additive expected decrease condition, i.e. to strictly decrease in expected value by some additive term > upon every one-step evolution of the system dynamics until either the target set or the unsafe set is reached. Furthermore, the initial value of the RASM is at most while the value of the RASM needs to exceed some À >>> in order for the system to reach the unsafe set. Thus, an RASM can intuitively be viewed as an invariant of the system which shows that the system has a tendency to converge either to the target or the unsafe set while also being repulsed away from the unsafe set, where this tendency is formalized by the expected decrease condition. To emphasize the additive expected decrease, we refer to RASMs of (88 as additive RASMs.
Definition 2 (Additive reach-avoid supermartingales 688 Let e > O and X > 1. A continuous function V : X + R is an (e, aaddiiiiee reach-avoid supermartingale ((e, A)adddiive RASM) with respect to X₂ and Xu, if:
1. Nonnegativity condition. (xx) 2 0 for each x E X.
2. Initial condition. V(x) < 1 for each x E Xy.
X,. 4. Additive expected decrease condition. For each x E X.,, de at which V(x) & X, we have
3. Safety condition. V(x) 2 for each
V Vxx 2 EV (f((, 7 (x). +
5

---

Table Comparison of the bound Theorem 2 and the bound in 668 for several values of À when 0.99. We set A = 0.1 which bounds the step size in the 9-Rooms environment, and Ly 5 which is an upper bound on the Lipschitz constant that we observe in experiments. Thus, the bound
in Theorem 2 is
7 =1 X 0.992> and in 68 is
10
100
1000
CLAPS bound (ours)
0.91820
0.99866
0.99999
68
0.9
0.99
0.999
Multiplicative RASMs and equivalence In this work we introduce multiplicative RASMs which need to decrease in expected value by at least some multiplicative factor (0, 1). We also impose the strict positivity condition outside of the target set Lz Note that any (e, A)-adiitive RASM satisfies this condition with the lower bound 0.
Definition 3 (Multiplicative reach-avoid supermartingales), Let E (0, 8 and À > 1. continuous function V X R is (7, 6, m)-uliiiplceative reach-avvid supermartingale ((7,8, A,)- multiplicatiiv RASM) with respect to X, and X.. if:
1. Nonnegativity condition. Vxx) 2 ffr each x E X.
2. Strict positivity outside X₂ condition. V(x) 2 8 for each x E X,
3. Initial condition. V(x) < for each x E Xy-
4. Safety condition. V(x) 2 for each Xu.
5. Multiplicative expected decrease condition. For each x E X at which V(x) S X, we
have 7 (xx 2 Ea-aaV (V (x)x(((
We show that a function V X - R is an additive RASM if and only if it is a multiplicative RASM. Theorem 1. [Proof in Apendix
C The following two statements hold:
1. If a continuous function
X + IR is an (eadiiidivvve RASM, then it also (- .miuff, A}, A)-multiplicative RASM.
2. If continuous function V : X + IR is (7, 8, X)-multiplccative RASM, then it is also an
((1 -)- 6, X) adddiivve RASM
Improved bound The following theorem shows that the existence of multiplicative RASM implies a lower bound on the probability with which the system satisfies the reach-avoid specification.
Theorem 2. (Proof in Appendix D Let y E (0, 1). ô > and X > L, and suppose that V X RR is (7,, 5, X) >)mmliippliaative RASM with respect to X, and Xu. Suppose furthermore that V is Lipschitz continuous with a Lipschitz constant Lv, and that the system under policy π satisfies the bounded step property, i.e. that there exists A > 0 such that ||x f(z, (xx), (x), S A holds for each x E X and w E W. Let N 1(> - 1)/(Lv A)]. Then, for every xo E Xy, we have that
1
P
ReachAvoid( Xm) 2
7 AM
Here, N' -(A 1(= A)J is the smallest number of time steps in which the system could hypothetically reach the unsafe set X, This is because, for the system to violate safety, by the Initial and the Safety conditions of multiplicative RASMs the value of V must increase from at most 1 to least A. But the value of V can increase by at most Ly A in any single time step since A the maximal step size of the system and Lv is the Lipschitz constant of V. Hence, the system cannot reach Xx in less than N [(> ()/ A)] time steps.
We conclude this section by comparing our bound to the bound Px |ReachAvoid( Xx)) 2 -
of [68] for additive RASMs. Our bound on the probability of violating reach-avoidance is tighter by factor of 7. Notice that this term decays exponentially as À increases, hence our bound is exponentially tighter A. This is particularly relevant if we want to verify reach-avoidance with high probability that is close to 1, as it allows using a much smaller value of À and significantly relaxing the Safety condition Definition To evaluate the quality of the bound improvement on an example, in Table I we consider the 9-Rooms environment and compare the bounds for multiple values of X when > 0.99. Note that A is the property the system and not the RASM. Thus, the value of is that, in order to verify
the key factor for controlling the quality of the bound. Results in TT probability 99.9% reach-avoidance for an edge policy in the 9-Room example, our new bound allows using À x 100 whereas with the old bound the algorithm needs to use X s 1000.

---

Remark (Comparison of RASMs and stochastic barrier functions). Stochastic barrier functions (SBFs) [55 46) were introduced for proving probabilistic safety in stochastic dynamical systems, i.e. without the additional reachability condition as in reach-avoid specifications. one is only interested in probabilistic safety, RASMs of (68) reduce to SBFs by letting X, = and < = 0 in Definition for additive RASMs, and X₁ 0 and 7y 1 in Definition for multiplicatiive RASMs. The bound on the probability of reaianavoidance Px. |ReachAvoid (0, X,]] 2 1 * of (68) for additive RASMs coincides with the bound on the probability of safety implied by SBFs of 145 466. Hence, our novel bound in Theorem 2 also provides tighter lower bound on the safety probability guarantees via SBFs.
Exponential stochastic barrier functions (exponential SBFs) have been considered in (49 in order to provide tighter bounds on safety probability guarantees via SBFs for finite time horizon systems, in which the length of the time horizon is fixed and known priori. Exponential SBFs also consider multiplicative expected decrease condition, similar to our multiplicative RASMs and provide lower bounds on safety probability which are tighter by factor which is exponential in the length N of the time horizon [49 Theorem 2J. However, as the length of the time horizon N -> DC, their bound shows that our multiplicative RASMs provide a tighter lower bound on safety (or more generally, reach-avoid) probability even in unbounded (i.e.
reduces to the bound of [45 46). In contrast, Theorem shows
indefinite) or infinite time horizon systems.
5
Compositional Learning for Probabilistic Specifications
We now present the CLAPS algorithm for learning a control policy that guarantees satisfaction of probabilistic specification ().p). where á is a SPECTRL. formula. The idea behind our algorithm is as follows. The algorithm first translates é into an abstract graph G = (V, E, 8, s, t) using the translation discussed in Section 3 in order to decompose the problem into a series of reach-avoid tasks associated to abstract graph edges. The algorithm then solves these reach-avoid tasks by learning policies for abstract graph edges. Each edge policy is learned together with a (multiplicative) RASM which provides formal guarantees on the probability of satisfaction of the reach-avoid specification proved in Theorem 2 Finally, the algorithm combines these edge policies in order to obtain a global policy We
that guarantees satisfaction of p). The algorithm pseudocode is presented in Algorithm assume the POLICY+R RSM subprocedure which, given a reach-avoid task and given a probability parameter p'; learns a control policy together with a RASM that proves that the policy guarantees reach-avoidance with probability at least p'. Due to the equivalence of additive and multiplicative RASMs that we proved in Theorem
[] for this we can use the procedure of (68] as an off-the-shelf method. For completeness of our presentation, we also provide details behind the POLICY+RASM subprocedure in Appendix L
Challenges There are two important challenges in designing an algorithm based on the above idea. First, it not immediately clear how probabilistic reach-avoid guarantees provided by edge policies may be used to deduce the probability with which the global specification á is satisfied. Second, since SPECTRL. formulas allow for disjunctive specifications, it might not be necessary to solve reach-avoid tasks associated to each abstract graph edge and naïvely doing so might lead to inefficiency. Our algorithm solves both of these challenges by first topologically ordering the vertices of the abstract graph and then performing a forward pass in which vertices are processed according to the topological ordering. The forward pass is executed in a way which allows our algorithm to keep track of the cumulative probability with which edge policies that have already been learned might violate the global specification o, therefore also allowing the algorithm to learn edge policies on-demand and to identify abstract graph edges for which solving reach- tasks would be redundant.
Forward pass on the abstract graph Since an abstract graph is directed acyelic graph (DAG), we perform a topological sort on G' in order to produce an ordering = 01, 12, . "|v L of its vertices (line 4 in Algorithm I). This ordering satisfies the property that each edge (v,, 02) in G must satisfy i < j. i.c. any each edge must be "forward edge" with respect to topological ordering. Algorithm I now initializes an empty dictionary Prob and sets Prob[s] = 1 for the source vertex s (line 5) and performs a forward pass to process the remaining vertices in the abstract graph according to the topological ordering (lines 6-13). The purpose of the dictionary Prob is to store lower bounds on the probability with which previously processed abstract graph vertices are reached by following the computed edge policies while satisfying reach-avoid specifications of the traversed abstract graph edges. For each newly processed vertex v; A Algorithm| [ learns policies for the reach-avoid tasks associated to all abstract graph edges that are incoming e, It then combines probabilities with
7

---

Algorithm 1 Compositional Learning for Probabilistic Specifications (CLAPS) )
1: Input Dynamics function /. probability distribution d, initial set Xo.
2: SPECTRL specification Φ. probability threshold p E [0. 1]
3: G = E, S, s,t) t abstract graph for Φ
4: s U1, ....... l|l] = + topoloiial ordering of vertices in G
5: Prob 4 empty hash map, Prob[s]
6: for 3.....I.
7: Prob[ed] 0
8: N(u)) - E ( (1) E E Prob[u] 2 p}
9: for all v E (1g) do
10:
T(v,n:), P(n.e;) + use binary search to find the maximal probability P(v.)) for which POLICY+RASM manages to learn a policy T(,,s)) that solves the reach-avoid task associ- ated to edge (v, v4) with probability least P(v,))
11: Prob[u:] + max(Prob(u:), P(n,,)) Prob[u]}
12: end for
13: end for
14: if [Prbb[]] 2 then
15: I + policy obtained by composing edge policies
16: return Policy that guarantees satisfaction of ().p).
else
18: return Policy for the probabilistic specification (ø, p) could not be learned.
end if
which the learned edge policies satisfy associated reach-avoid tasks with the probabilities that have been stored for the previously processed vertices in order to compute the lower bound Prob[ex]-
More concretely, for each 2 < i < [V], Algorithm first stores Prob[u:] = O as a trivial lower bound (line 7). It then computes the set N (v,) of all predecessors of v; for which previously learned edge policies ensure reachability with probability at least while satisfying reach-avoid specification of all traversed abstract graph edged (line 8). Recall, p is the global probability threshold with which the agent needs to satisfy the SPECTRL specification ø and since Algorithm | processes vertices according to the topological ordering all vertices in N(;;)) have already been processed. If (e;)) is empty, then the algorithm concludes that vú cannot be reached in the abstract graph while satisfying reach-avoid specifications of traversed edges with probability at least p. In this case, the algorithm does not try to learn edge policies for the edges with the target vertex and proceeds to processing the next vertex in the topological ordering. Thus, Algorithm Tensures that edge policies are learned on-demand. If (w,)) is not empty, then for each E NN N(x..) the algorithm uses POLICY+RASM together with binary search to find the maximal probability P(e.r.) for which POLICY+RASM manages to learn a policy (v, that solves the reach-avoid task with probability at least P(v,..) (line 10). We run the binary search only up to a pre-specified precision, which is a hyperparameter of our algorithm. Since the reach-avoid specification of the edge (v, v.) is satisfied with probability at least P(e,r.) and since is reached in the abstract graph while satisfying reach- avoid specification of all traversed edges with probability at least Prob/u]. Algorithm I (pddates its current lower bound Prob(e: [v:] for e to P().))) Prob (r) whenever P(r,).) Prob[u) exceeds the stored bound Prob[us] (line 11). This procedure repeated for each v E N(x.).
Composing edge policies into a global policy Once all abstract graph vertices have been processed, Algorithm I checks if Prob(t] 2 (line 14). If so, it composes the learned edge policies into a global policy π that guarantees satisfaction of the probabilistic specification (ø. p) (line 15) and returns the policy (line 16). The composition is performed as follows. First, note that for each vertex v A in the abstract graph for which Prob[u] > O, by lines 7-11 in Algorithm [ there must exist a vertex o E ((r) such that the algorithm has successfully learned a policy a(v",v) w) for the edge (v', v) and such that Prob[u] P(vr, .) Prob(e') (b'). Hence, repeatedly picking such predecessors yields finite path s Vig ....... Vi, = t in the abstract graph such that, for each 1 S j S k, the algorithm has successfully learned edge policy T((xy-1:";,)) and such that Prob/es,1 P(mi--nee))) Prob(uu,-.l
holds. The global policy π starts by following the edge policy ((ag)"")) until the target region 3(v),) ) is reached or until the safety constraint ((v : Vs,) associated to the edge is violated. Then,
8

---

(a) The objective is to navigate from the initial set in the bottom left (in green) the target set in the top right room (in violet).
(b) Visualization of trajectories of end to sode-t--nd learned policy. The policy hits the walls and cannot verified as safe.
(c) Visualization of trajectories of the three verifiable composi- tional policies with intermediate initial/target states shown in grey.
Stochastic Nine Rooms environment for which an end-to-end learned policy cannot be verified safe while our algorithm able to decompose the task into three verifiable subtasks.
Figure 1:
compeaition graph
Ver subtocks
complete path
Figure 2: Decomposition of the Stochastic Nine Rooms task into subtasks, Left: Individual subtasks shown as graph edges. Center: Successfully verifiable subtasks are shown in blue edges, whereas the verification procedure of the gray edges failed. Right: Verified path for solving the complete task.
it follows the edge policy "(vi,e9g) until the target region B(vr,) is reached or until the safety constraint (U) 2122) associated to the edge is violated. This is repeated for each edge along the path & = Vig ......,, Ui, = until the system reaches a state within the target region B(t). If at any point the safety constraint violated prior reaching the target region associated to the edge, policy x follows the current edge policy indefinitely and no longer updates it as the specification á has been violated. As we prove in Theorem 3 violation of the safety constraint associated some edge or the system never reaching the target region associated to some edge happen with probability most p. If Prob[t] < p, then Algorithm returns that could not learn policy that guarantees satisfaction of (é, p). Theorem 3 establishes the correctness of Algorithm [
and its proof shows that the global policy æ obtained as above indeed satisfies the probabilistic specification (Ø.p).
Theorem 3. [Proof in Appendix FF Algorithm iis compositional, and it outputs policy n, then guarantees the probabilistic specification (Ó.P).
6 Experiments
We implement a prototype of Algorithm to validate its effectiveness? Motivated by the experiments of (33), we define an environment which an agent must navigate safely between different rooms. However, different from (33] our Stochastic Nine Rooms environment perturbs the agent by random noise in each step. Concretely, the system is governed by the dynamics function, x4+1 = 24 0.1 min (miin(ma(((a 1), 1) + w,, where is drawn from a triangular noise distribution. The state space of the environment defined as [0, x [0, 3] C R2, The set of the initial states is [0.4, 0.6] x [0.4.066] whereas the target states are defined as [2.4 2.6] x [2.4. 2.6). The state space contains unsafe areas that should be avoided, i.e., the red walls shown in Figure [ Specifically, these unsafe areas cannot be entered by the agent, and coming close to them during the RL training incurs penalty. Note that this defines a reach-avoid task where the goal to reach the target region from the initial region while avoiding the unsafe regions defined by red walls.
We first run the POLICY+RASM procedure (i.e. the method of (68) on this task directly and observe that it is not able to learn policy with any formal guarantees on probability of reach-avoidance.
Our code is available at httttt:::/ggtiiii httppp////gtttae...oa.ca/a/a//// http://wwww..eeaaaaaaoo/oaaaaaee

---

We then translate this task into SPECTRL task which decomposes it into set of simpler reach- avoid tasks by constructing an abstract graph as follows. The vertex set of the abstract graph consists of centers of each of the 9 rooms, and the target regions associated to each room center are [0.4 + z, 0.6 + x] x [0.4 + y, 0.6 + y] for x; y E {0, 1,. Edges of this abstract graph are shown in Figure 2 left. To each edge, we associate an unsafe region to be avoided by taking red walls incident to rooms in which the edge is contained.
For each reach-avoid edge task, we run the proximal policy optimization (PPO) [50] reinforcement learn- ing algorithm to initialize policy parameters. We then run the POLICY+RASM procedure learn policy and RASM which proves probabilistic reach-avoidance. We set the timeout to hours for each reach-avoid subtask. In Figure | b), we visual- ize the PPO policy that was trained to reach the tar- get states directly from the initial states. As shown, the policy occasionally hits a wall and cannot be verified, i.e., POLICY+RASM procedure times out.
Table 2: Verified lower bounds on reach-avoid probability for each edge policy. Initial and target states represented by pairs (z,, y) with [0.4 + x, 0.6 + x] x [0.4 + y. 0.6 + y) for 2, E {0, 1,
Start (r1,y1)
Goal
Reach-avoidance probability
(22, y2)
(0.0)
(1,0)
75.1%
In Figure 2 center, we visualize all successfully verified subtasks in blue. The reach-avoid lower bounds for each of the subtasks are listed in Table Note that the simplest decomposition passing over the bottom right room could not be verified, which shows that the systematic decomposition used in our algorithm has advantages over manual task decom- positions. Finally, in Figure 2 right, we highlight the path from the initial states to the target states via safe intermediate sets. In Figure Te), we visu- alize the trajectories of these three compositional policies. As shown, the trajectories never reach an unsafe area.
(0.0)
(2,0)
57.7%
(0.0)
(0.1)
72.3%
(1,0)
(2,0)
71.4%
(0.1)
(2,1)
61.5%
(0.1)
(1.1)
72.2%
(1.1)
(1,2)
73.3%
(1.2)
(2.1)
68.5%
(2.1)
(2,2)
74.5%
(0.0)
(2,2)
Fail (method of
(68])
(0.0)
(2,2)
33.0% (our method)
7 Concluding Remarks
We propose CLAPS, a novel method for learning and verifying a composition of neural network policies for stochastic control systems. Our method considers control tasks under specifications in the SPECTRL L. lanugange, decomposes the task into an abstract graph of reach-avoid tasks and uses reach-avoid supermartingales to provide formal guarantees on the probability of reach-avoidance in each subtask. We also prove that RASMs imply a strictly tighter lower bound on the probability of reach-avoidance compared to prior work. These results provide confidence in the ability of CLAPS to find meaningful guarantees for global compositional policies, as shown by experimental evaluation in the Stochastic Nine Rooms environment. While our approach has significant conceptual, theoretical and algorithmic novelty, it is only applicable to SPECTRL logical specifications and not to the whole of LTL. Furthermore, our algorithm is not guaranteed to return a policy and does not guarantce tight bounds on the probability of satisfying the logical specification. Overcoming these limitations will provide further confidence in deploying RL based solutions for varied applications.
Acknowledgments
This work was supported in part by the ERC-2020-AdG 101020093 (VAMOS) and the ERC-2020- CoG 863818 18 (FoRM-SMArt).
References
[1] Alessandro Abate, Daniele Ahmed, Alec Edwards, Mirco Giacobbe, and Andrea Peruffo. FOSSIL: software tool for the formal synthesis of Ιyаpunov functions and barrier certificates using neural networks. In Sergiy Bogomolov and Raphaël M. Jungers, editors, HSCC '21: 24th ACM International Conference Hybrid Systems: Computation and Control, Nashville,
10

---

Tennessee, May 19-21, 2021. pages 24:1-24:111 ACM, 2021. doi: 10. 10.114573444992.4456644
URL httpp:///oi. org/ 10. 1145/3447928. 3456646
[2] Alessandro Abate, Daniele Ahmed, Mirco Giacobbe, and Andrea Peruffo. Formal synthesis of Iyapunoy neural networks. IEEE Control. Syst. Lett., ((3):773-778) 2021. doi: 10.1 109/ LCSYS.2020.30055.
URL https: org 10. 1109/LCSYS. 2020. 20...00222222 3005328.
[3] Joshua Achiam, David Held, Aviv Tamar, and Pieter Abbeel. Constrained policy optimization. In International Conference on Machine Learning, pages 22-31. PMLR, 2017.
[4] Mohammed Alshiekh, Roderick Bloem, Rüdiger Ehlers, Bettina Könighofer, Scott Nickum, and Ufuk Topcu. Safe reinforcement learning via shielding. In Sheila A. Mcllraith and Kilian Q Weinberger, editors, Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI-18), the 30th innovative Applications of Artificial Intelligence (1AAI-18), and the 8th AAAI Symposium on Educational Advances in Artificial Intelligence (EAAI-18), New Orleans, Louisiana, USA, February 2-7, 2018, pages 2669-2678. AAAI Press, 2018. URL https: btops::/wwwy aaai org/ ocs/ index.
[5] Eitan Altman. Constrained Markov decision processes, volume 7. CRC Press, 1999.
[6] Dario Amodei, Chris Olah, Jacob Steinhardt, Paul F. Christiano, John Schulman, and Dan Mané. Concrete problems Al safety. CoRR, abs/ 10s.06666,,,, 2016. URL http://att http///axivv.rrr abs/1606.0655
[7] Greg Anderson, Abhinav Verma, Isil Dillig, and Swarat Chaudhuri. Neurosymbolic reinforce- ment learning with formally verified exploration. In Hugo Larochelle, Marc' Aurelio Ranzato, Raia Hadsell, Maria-Florina Balcan, and Hsuan-Tiees Lin, editors, Advances in Neural Informa- tion Processing Systems 33: Anmual Conference on Neural Information Processing Systems 2020, neur NeurlPS 2020, December 6-12, 2020, virtual, 2020. URL Abstraf---bttatt..h.h cc/paper/2020/ http:///0000//aa44444e4//e//9999
[8] Matin Ansaripour, Krishnendu Chatterjee, Thomas A. Henzinger, Mathias Lechner, and Dorde Zikelić. Learning provably stabilizing neural controllers for discrete-time stochastic systems. In Étienne André and Jun Sun, editors, Automated Technology for Verification and Analysis, pages 357-379, Cham, 2023. Springer Nature Switzerland. ISBN 978-3-031--4332--5
[9] Thom S. Badings, Alessandro Abate, Nils Jansen, David Parker, Hasan A. Poonawala, and Mariëlle Stoelinga. Sampling-bass based robust control of autonomous systems with non- gaussian noise. In Thirty-Sixth AAAI Conference on Artificial Intelligence, AAAI 2022, Thirty-Fourth Conference Innovative Applications of Artificial Intelligence, IAAI 2022, The Twelveth Symposium on Educational Advances in Artificial Intelligence, EAAI 2022
Virtual Event, February 22 March 1, 2022, pages https://og aaai org/ index. php/ ALA.T/artiileevie///12222.
AAAI Press, 2022. URL
[10] Thom S. Badings, Licio Romao, Alessandro Abate, and Nils Jansen. Probabilities are not enough: Formal controller synthesis for stochastic dynamical models with epistemic uncertainty. CoRR, abs/2210.0592 2022. doi: 10448550%/axxxv2220005599 URL https:////// LB850//rXXi 2210.05989
[11] Felix Berkenkamp, Matteo Turchetta, Angela P. Schoellig, and Andreas Krause. Safe model-based reinforcement learning with stability guarantees. In Isabelle Guyon, Ulrike von Luxburg, Samy Bengio, Hanna M. Wallach, Rob Fergus, S. V. N. Vishwanathan, and Roman Garnett, editors, Advances in Neural Information Processing Systems 30: Annual Con- ference on Neural Information Processing Systems 2017, December 4-9, 2017, Long Beach, CA, USA, pages 908-918, 2017. https:tttts:::/peeeeeeiiii www.rsenurrpppp httpppsscccpppppe/0//0 .ttml
[12] Alper Kamil Bozkurt, Yu Wang. Michael M. Zavlanos, and Miroslav Pajic. Control synthesis from linear temporal logic specifications using model-free reinforcement learning. 2020 IEEE International Conference on Robotics and Automation, ICRA 2020, Paris, Frunce, May 31 August 31, 2020, pages 10359-10355. IEFF, 2020. doi: 10. 10.1100//CRA 240444999992209999999666
URL https:/ /oi. org/ 10. 1109/ 4094 2020 9196796
11

---

[13] Ronen I. Brafman, Giuseppe De Giacomo, and Fabio Patrizi. Liff/dlf non mon-maooviann rewards. In Sheila A. Mcllraith and Kilian Q. Weinberger, editors, Proceedings the Phirty-Second AAAI Conference Artificial Intelligence, (AAAI-18), the 30th innovative Applications of Artificial Intelligence (IAAI-18), and the 8th AAAI Symposium on Educational Advances Artificial Intelligence (EAAI-18), New Orleans, Louisiana, USA, February 2-7, 2018. pages 1771-1778 AAAI Press, 2018. URL htttps://// /ttw://www... aaai wwtp/////o//toeeeeeeeeeeeeooooot index.ndxxx..... php/ hAtp/AAAT/AAAT1// paper/ view/17342
[14] Nathalie Cauchi and Alessandro Abate. autommad verification and synthesis of stochas- tic processes. In Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, pages 258 2298229,222 2019.
[15] Aleksandar Chakarov and Sriram Sankaranarayanan Probabilistic program analysis with martingales. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. volume 8044 of Lecture Notes in Computer Science, pages 511-526. Springer, 2013. doi: 10. 34. URL htt.:////2bb...o////000007776672
34
[16] Ya-Chien Chang and Sicun Gao. Stabilizing neural control using self-learned almost іyарunov critics. In IEEE International Conference on Robotics and Automation, ICRA 2021, Xi' an. China, May June 5, 2021, pages 1803-1809. IEEE, 2021. doi: 10.1 (009///AAA40..2221..0555.55 URL htLthttps://dat //osi org/ 10. 11111//IIIII0000 2t...0000....... .9500886
[17] Ya-Chien Chang. Nima Roohi, and Sicun Gao. Neural Iyаpunov control. In Hanna M. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence d' Alché-Buc, Emily B. Fox, and Roman Garett,, editors, Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurlPS 2019, December 8-14, 2019, Vancouver, BC, neur paccppppe/20015 Canada, pages 2249,3249, 2019. URL Abstrattbbtttttttbb.... html
[18] Krishnendu Chatterjee, Petr Novotný, and Dorde Žikelić. Stochastic invariants for probabilistic termination. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, Jamuary 18-20, 2017, pages 145-160) ACM, 2017. doi: 10. 10.11455300998333009973 URL https://doii org/ 10. 1111/10009/33111 /0tp///0009837.0008733
[19] Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, and Dorde Zike- lic. Sound and complete certificates for quantitative termination analysis of probabilistic programs. In Sharon Shoham and Yakir Vizel, editors, Computer Aided Verification 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I, volume 13371 of Lecture Notes in Computer Science, pages 55-78. Springer. 2022. doi: 10. (007/978-3-031-13333 3-11--331---------11--- URL httpp:://di..rgg// 1007 3-0000099778--1-111111111-0 -3188 1_4
[20] Krishnendu Chatterjee, Thomas Henzinger, Mathias Lechner, and Dorde Zikelic. A learne- verifier framework for neural network controllers and certificates of stochastic systems. In Sriram Sankaranarayanan and Natasha Sharygina, editors, Tools and Algorithms for the Construction and Analysis of Systems 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part I, volume 13993 of Lecture Notes in Computer Science, pages 3-25. Springer, 2023. doi: 10. 10.1007/9778-3-01-300888 10. 1007//9977 3- 031 30823-9-1
URL https://doi /tt::////oooo//////////
[21] Yinlam Chow, Ofir Nachum, Edgar A. Duéñez-Guzmál and Mohammad Ghavamzadeh. A 'yapunov-based approach safe reinforcement learning. In Samy Bengio, Hanna M. Wal- lach, Hugo Larochelle, Kristen Grauman, Nicolò Cesa-Bianchi and Roman Garnet, editors, Advances in Neural Information Processing Systems 31: Annual Conference on Neural In- formation Processing Systems 2018, NeurlPS 2018, December 3-8, 2018, Montréal, Canada, pages 8103-8112, 2018. URL 4fe51 02551999999222000066666777779900 Awstract. html
12

---

[22] Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Robert M. Graham, Michael A. Harrison, and Ravi Sethi, editors, Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, pages URL https://doi. org/ 10. 1145/
238-252. ACM, 1977. doi: 10. 10.1145/512950.51222 512950.5122 512973
[23] Gal Dalal, Krishnamurthy Dvijotham, Matej Vecerík, Todd Hester, Cosmin Paduraru, and Yuval Tassa. Safe exploration in continuous action spaces. ArXiv, abs/1 012/1880.08877 801.08757, 2018.
[24]
Charles Dawson, Sicun Gao, and Chuchu Fan. Safe control with learned certificates: A survey of neural Iyapunov, barrier, and contraction methods for robotics and control. IEEE Truns. Robotics, 39(3):1749-1766 2023. doi: 10. 1099/TR..222.32225555 URL https //doi.org/10, 1109 TTOO 2.....2223222 3232542
[25] Ingy Elsayed-Aly, Suda Bharadwaj. Christopher Amato, Rüdiger Ehlers, Ufuk Topcu, and Lu Feng. Safe multi-agent reinforcement learning via shielding. In Frank Dignum, Alessio Lomuscio, Ulle Endriss, and Ann Nowé, editors, AAMAS 21: 20th International Conference on Autonomous Agents and Multiagent Systems, Virtual Event, United Kingdom, May 3-7. 5555555533335 3463952 2021, pages 483-491. ACM, 2021. https:/:s://dl acm. org/ wtt.a/......//................/. 3464013
[26] Peter Geibel. Reinforcement learning for mdps with constraints. In Johannes Fürnkranz, Tobias Scheffer, and Myra Spiliopoulou, editors, Machine Learning: ECMI. 2006, 17th European Conference on Machine Learning, Berlin, Germany, September 18-22, 2006, Proceedings, volume 4212 of Lecture Notes Computer Science, pages 646 653. Springer, 2006. doi: 1332 htLphtts::///
org/ 10. 1007
[27] Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Uesato, Relja Arandjelovic, Timothy A. Mann, and Pushmeet Kohli. On the effectiveness of interval bound propagation for training verifiably robust models. CoRR, 0bs/1810.12715, 2018.
URL httt:://arxiii org
www.oorggg//booo..oooo.oooe aa////bbs///1/// 12715
[28] Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, and Dominik Wojtczak. Omega-regular objectives in model-free reinforcement learning. In Tomás Vojnar and Lijun Zhang, editors, Tools and Algorithms for the Construction and Analysis of Systems- 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part I, volume 11427 Lecture Notes in Computer Science, pages 395-412. Springer, 2019. doi: 10. 1007/998---0000 17460000-776--1--1 URL https:://// //ds:///do.. htt///oo..ogg///// or.//o/....0000.. 030---2---77
[29] 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 58th IEEE Con Conference on Decision and Control, CDC 2019, Nice, France, December 11-13, 2019, pages 5338 5343. IEEE, 2019. doi: 10. 1009 EDC40024420199900255
URL http:: //doi. org/ 10. 1 L0C/CD240022 2019. 9028919
[30] Radoslav Ivanov, Kishor Jothimurugan, Steve Hsu, Shaan Vaidya, Rajeev Alur, and Osbert Bastani. Compositional learning and verification of neural network controllers. ACM Truns. Embed. Comput. Syst. 20655))92 2021. doi: 10.1145/3477023. URL htltsttps: //doi
org/10. 1145/3477023
[31] Nils Jansen, Bettina Könighofer, Sebastian Junges, Alex Serban, and Roderick Bloem. Safe rein- forcement learning using probabilistic shields (invited paper). In Igor Konnov and Laura Kovács, editors, st International Conference on Concurrency Theory, CONCUR 2020, September 144, 2020, Vienna, Austria (Virtual Conference), volume 171 of LIPIcs, pages 3:1-3:16. Schloss URL
Dagstuhl - Leibniiz-Zetruum Zentrum für Informatik, 2020. doi: 10.42230PPPs..CONCRRROO
https: sctts://doi. //ooi. org/10. 4230/LIPICs. CONCUR. 2020.3
[32] Kishor Jothimurugan, Rajeev Alur, and Oshert Bastani. composable specification lan- guage for reinforcement learning tasks. In Hanna M. Wallach, Hugo Larochelle, Alina
13

---

Beygelzimer, Florence d' d'Allhé--Boe Emily B. Fox. and Roman Gamett, editors. Advances in Neural Information Processing Systems 32: Anmual Conference on Neural Information Processing Systems 2019, NeurlPS 2019, December 8414, 2019, Vancouver, BC, Canada, wewpeddiinnnnnnniiiniee heurips.co www..ps....ppapereeeeee wttpcc/ppppp////////ea/
pages 13021-13030, 2019. bttps://: cd3.//f333333f3 Abstract.trattttmm
[33] Kishor Jothimurugan, Suguman Bansal, Osbert Bastani, and Rajeev Alur. Composi- tional reinforcement learning from logical specifications. In Mare' Aurelio Ranzato, Alina Beygelzimer, Yann N. Dauphin, Percy Liang, and Jennifer Wortman Vaughan, editors, Advances in Neural Information Processing Systems 34: Anmual Conference on Neu- ral Information Processing Systems 2021, NeurIPS 2021, December 6-14, 2021, virtual, pages 10026-10039, 2021. URL 53 (377599e003330411455555577777
neurips html
[34] Koller, Felix Berkenkamp, Matteo Turchetta, and A. Krause. Learning- based model predictive control for safe exploration. 2018 IEEE Conference on Decision and Control (CDC), pages 6059-6066, 2018.
[35] Harold J. Kushner. A partial history of the early development of contimuous-time nonlinear stochastic systems theory. Autom 50(2):303-334, 2014. doi: 10. 1...1066....ooaaaiiii m0ttomatica.211.111...... (tLLhhtss://doo org 10. htt.://///....mmtitii...... automatica 2013. 013
[36] Abolfazl Lavaei, Mahmoud Khaled, Sadegh Soudjani. and Majid Zamani. AMYTISS: paral- lelized automated controller synthesis for large-scale stochastic systems. In Shuvendu K. Lahiri and Chao Wang. editors, Computer Aided Verification 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II, volume 12225 of Lecture Notes in Computer Science, pages 461 1-44, Springer, 2020. doi: 10. 10007997-330000-5220 24. URL http://ooo.org///// 10. 1007 9977//9783333 3--30003329-----11
[37] Mathias Lechner, Dorde Zikelic, Krishnendu Chatterjee, and Thomas A. Henzinger. In- finite time horizon safety of bayesian neural networks. In Mare' Aurelio Ranzato, Alina Beygelzimer, Yann N. Dauphin, Percy Liang, and Jennifer Wortman Vaughan, editors, Advances in Neural Information Processing Systems 34: Annual Conference on Neu- ral Information Processing Systems 2021, NeurlPS 2021, December 6-14, 2021, virtual, pages 10171-10185, 2021. 344def88radff5ccc337113333333330
www.iinggn...uuinee neurips. cttp:ppp...cpppppp//222111111111 pctpp//a/per/////aaah Abstract.htm
[38] Mathias Lechner, Dorde Zikelic, Krishnendu Chatterjee, and Thomas A. Henzinger. Stability verification in stochastic control systems via neural network supermartingales. In Thirty-Sixth AAAI Conference on Artificial Intelligence, AAAI 2022, Thirty-Fourth Conference Innovative Applications of Artificial Intelligence, IAAI 2022, The Twelveth Symposium on Educational Advances in Artificial Intelligence, EAAI 2022 Virtual Event, February 22 March 1, 2022. pages 7326-7336. AAAI Press, 2022. URL https://ojs aaai. org/ /ts//nndxx...///// php/AAAI article/view/2662.
[39] Xiao Li, Cristian Ioan Vasile, and Calin Belta. Reinforcement learning with temporal logic rewards. In 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems, IROS 2017, Vancouver, BC, Canada, September 24-28. 2017, pages 3834-3839, IEEE, 2017. doi: 10. 109/100000000111111 20008800022117.8002444,, 8206234. URL htRps:ts::// //dopps:://o..... org/ 10. 1100/IRIS..... IROS. 2017 . 8206234
[40] Anqi Liu, Guanya Shi, Soon-Jo Chung, Anima Anandkumar, and Yisong Yue. Robust regression for safe exploration in control. In L4DC, 2020.
[41] Frederik Baymler Mathiesen, Simeon Craig Calvert, and Luca Laurenti. Safety certification for stochastic systems via neural barrier functions. IEEE Control. Syst. Lett., 7:973-978, 2023. doi: 10.1 (T009//CSSS.2022.3.332
URL tattps://doi. org/ 10. 11t..1119/LCCCS 2022. 32298665
[42] Rayan Mazouz, Karan Muvvala, Akash Ratheesh Babu, Luca Laurenti, and Morteza Lahijanian. Safety guarantees for neural network dynamic systems via stochastic barrier functions. In Alice H. Oh, Alekh Agarwal, Danielle Belgrave, and Kyunghyun Cho, editors, Advances in Neural Information Processing Systems, 2022. URL URR.ihttps://ppereviiee net/ foommmidd 9XQa6cgLo21
14

---

[43] Cyrus Neary, Christos K. Verginis, Murat Cubuktepe, and Ufuk Topcu. Verifiable and composi- tional reinforcement learning systems. In Akshat Kumar, Sylvie Thiébaux, Pradeep Varakan- tham, and William Yeoh, editors, Proceedings of the Thirtt-Second International Conference on Automated Planning and Scheduling, ICAPS 2022, Singapore (virtual), June 13-24, 2022, pages 615-623. AAAI Press, 2022. httpst:s::/ view/19849
aaai. org/ /eg//indx.... php/ ICAPS/ article/
[44] Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October- I November 1977, pages 46-57. IEEE Computer Society, 1977. doi: 10.1109/SRCS.1971 10.1109/SFCH /FCCS 1977.32
URL.https://doi org/
[45] Stephen Prajna, Ali Jadbabaie, and George J. Pappas. Stochastic safety verification using barrier certificates. In 43rd IEEE Conference on Decision and Control, CDC 2004, Nassau, Bahamas, December 14-17, 2004, pages 1019//....19/CCC 1ww.//DC.CCCCC 2004. 1428804
IEEE, 2004, doi: 10. 20.1009/CCC.220411100 1428804. URL
https://doi. org/10.
[46] Stephen Prajna, Ali Jadbabaie, and George J. Pappas. A framework for worst-case and stochas- tie safety verification using barrier certificates. JEEE Trans. Autom. Control., 1415- 1428, 2007. doi: 11109//A..2007.9227366 902736
2007
[47] Martin L. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics. Wiley, 1994. ISBN 978-0-47161977-2. doi: 10.1002/ 9780470316887. URL /ttts:://///: 90200007700/77778116666666
[48] Spencer M. Richards, Felix Berkenkamp, and Andreas Krause. The іуарunov neural network: Adaptive stability certification for safe learning of dynamical systems. In 2nd Annual Confer- ence on Robot Learning, CoRL. 2018, Zärich, Switzerland, 29-31 October 2018, Proceedings, volume 87 of Proceedings of Machine Learning Research, pages 466-476. PMLR, 2018. URL http:///rroceedings mlr. www.ppreesssweseeeeeeee http:///r7/rcccards...... hhtml
[49] Cesar Santoyo, Maxence Dutreix, and Samuel Coogan. A barrier function approach finite-time stochastic system verification and control. Autom.,, 125:109439 2021. doi: 10. aut.ammtaaatcaa A020.109439. Jtttpsss::///o1
wrw.ll..rrr...1110 1ttp//0..0001//11 automatica 2020. 109439
[50] John Schulman, Filip Wolski, Prafulla Dhariwal, Alec Radford, and Oleg Klimov. Proximal policy optimization algorithms. arXiv preprint 1iXXvv1777.06377, 2017.
[51] Aivar Sootla, Alexander Cowen-Rivers, Jun Wang, and Haitham Bou Ammar. Enhancing safe exploration using safety state augmentation. Advances in Neural Information Processing Systems, 15:34464-34477 2022.
[52] Aivar Sootla, Alexander I. Cowen-Rivers, Taher Jafferjee, Ziyan Wang, David Henry Mguni, Jun Wang. and Haitham Ammar. Saute RL: almost surely safe reinforcement learning using state augmentation.
Kamalika Chaudhuri, Stefanie Jegelka, Le Song, Csaba Szepesvári, Gang Niu, and Sivan Sabato, editors, International Conference
Machine Learning, ICML 2022, 17-23 July 2022, Baltimore, Maryland, USA, volume 162 of Proceedings of Machine Learning Research, pages 20423-20443 PMLR, 2022. URL https://proceeddnggs mir press/v162/
2012//ootla222. vress/vi62/sootla22aaao html
[53] Sadegh Esmaeil Zadeh Soudjani, Caspar Gevaerts, and Alessandro Abate. FAUST 2 Formal abstractions of uncountable-star stochastic processes. In Christel Baier and Cesare Tinelli, editors, Tools and Algorithms for the Construction and Analysis of Systems - 21 International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 1 11-18, 2015. Proceedings, volume 9035 of Lecture Notes in Computer Science, pages 272-286. Springer, 2015. doi: 10.1007/ 778-3-662-46681-12 -3._2,.. URL https:///oo....... http:///oooorg////// 1110:/10110007777333-----6---611
[54] Sean Summers and John Lygeros. Verification of discrete time stochastic hybrid systems: A stochastic reach-avoid decision problem. Autom., 16(12))1951 2010. doi: 10. 1016/. 20100. URL https: :/do::////ooo// org htt.::/tt//ooo..... 1016/j automatica. 2010 08. 006
15

---

[55] Dawei Sun, Susmit Jha, and Chuchu Fan. Learning certified control using contraction metric. In Jens Kober, Fabio Ramos, and Claire Tomlin, editors, 4th Conference on Robot Learning. CoRI. 2020, 16- 18 November 2020, Viriual Event / Cambridge, MA, USA, volume 155 of Proceedings of Machine Learning Research, pages 1519-1539, PMLR, 2020. URL. https //proceedings.. pte.s/pee////ee prressvv55/ v155/ http//unnlbbbbb.e
[56] Richard Sutton and Andrew G Barto. Reinforcement learning: An introduction. MIT press, 2018.
[57] Christian Szegedy, Wojciech Zaremba, llya Sutskever, Joan Bruna, Dumitru Erhan, Ian J. Goodfellow, and Rob Fergus. Intriguing properties of neural networks. In Yoshua Bengio and Yann LeCun, editors, 2nd International Conference on Learning Representations, ICLR 2014, Banff. AB, Canada, April 14-16, 2014, Conference Track Proceedings, 2014. URL http:// httt://arxiv..
http/axxivvv.ro/ www.vvorg//aaa hbs/ httg/abb/1312.. 13121 6199
[58] Toru Takisaka, Yuichiro Oyabu, Natsuki Urabe, and Ichiro Hasuo. Ranking and repulsing supernartingales for reachability in randomized programs. ACM Trans. Program. Lang. Syst.,
4 2021. doi: 10. 10.1145/3450967. URL httpss/:: wwwpoi..rgr/... 1145//4999//
[59] Matteo Turchetta, Felix Berkenkamp, and A. Krause. Safe exploration for interactive machine learning. In NeurIPS, 2019.
[60] Pashootan Vaezipoor, Andrew C. Li, Rodrigo Toro Icarte, and Sheila A. Mcllraith. Lıl2action: Generalizing LTL instructions for multi-task RL. Marina Meila and Tong Zhang, editors, Proceedings of the 38th International Conference on Machine Learning. ICML 2021, 18-24 July 2021. Virtual Event, volume 139 of Proceedings of Machine Learning Research, pages 10497- 10508. PMLR, 2021. URL http::/pproceeeingg/ mlr, wwwppppwwssswwweweeewww www.1/////vvioor21..... html
[61] Abraham P. Vinod, Joseph D. Gleason, and Meeko M. K. Oishi. Sreachtools: a MATLAB stochastic reachability toolbox. In Necmiye Ozay and Pavithra Prabhakar, editors, Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019, Montreal, QC, Canada, April 16-18, 2019, pages 33-38. ACM, 2019. doi: 10. 10.11433330204.333 1809. URL httthtt:s://o/// htt:://oooooogg////// org/ 1145 3/t///33225503331333
[62] Jun Wang, Samarth Kalluraya, and Yiannis Kantaros. Verified compositions of neural net- work controllers for temporal logic control objectives. In 61st IEEE Conference on De- cision and Control, CDC 2022, Cancun, Mexico. December 6-9, 2022, pages 4004 4009. IEEE, 2022. doi: D0.109/CDCS110532222.99999000000 URL httpp::/ddo org/ 10. 1109/ CDC51059. 201.559..0229990 9993010
[63] Yixuan Wang, Simon Sinong Zhan, Ruochen Jiao, Zhilu Wang, Wanxin Jin, Zhuoran Yang, Zhaoran Wang, Chao Huang, and Qi Zhu. Enforcing hard constraints with soft barriers: Safe reinforcement learning in unknown stochastic environments. In Andreas Krause, Emma Brunskill, Kyunghyun Cho, Barbara Engelhardt, Sivan Sabato, and Jonathan Scarlett, editors, International Conference on Machine Learning, ICML 2023, 23-29 July 2023, Honolulu, Hawaii, USA, volume 202 of Proceedings of Machine Learning Research, pages 36593-36604. PMLR, 2023. Uttp
mlr press/ vttp:/222/////// http///2222/2//222 wang23as html
[64] David Williams. Probability with Martingales. Cambridge mathematical textbooks. Cambridge University Press, 1991. ISBN 978-0-521-400 -406555-55
[65] Bai Xue, Renjue Li, Naijun Zhan, and Martin Fränzle. Reach-avoid analysis for stochastic discrete-time systems. In 2021 American Control Conference, ACC 2021, New Orleans, LA, USA, May 25-28, 2021, pages 4879 4885. IEEE, 2021. doi: 00.23919/ACC5551..20 9483095. URL https:://oo: org/ 10. 23919 At1p//1151111111111 2021100511110011.11.111111111111 9483095
[66] Cambridge Yang, Michael L. Littman, and Michael Carbin. On the (in)tractability of rein- forcement learning for LTL objectives. In Luc De Raedt, editor, Proceedings of the Thirty- First International Join Conference on Artificial Intelligence, IJCAI 2022, Vienna, Austria, 23-29 July 2022, pages 3650-3658. ijcai.org, 2022. doi: 10.24963/ijcai, 2022/507. URL.
https: / /doi. org/ 10..//0.000 24963 11003//jjaa.. 2022/507
16

---

[67] Mojtaba Zarei, Yu Wang, and Miroslav Pajic. Statistical verification of learning- based cyber- physical systems. In Aaron D. Ames, Sanjit Seshia, and Jyotirmoy Deshmukh, editors. HSCC '20: 23rd ACM International Conference on Hybrid Systems: Computation and Control, Sydney, New South Wales, Australia, April 21-24, 2020, pages 12:1-12:7. ACM, 2020. doi: 10.1 00.114553363333333322200
10. 1 1145/ 03655/333665.... 338209
[68] Dorde Zikelic, Mathias Lechner, Thomas A. Henzinger, and Krishnendu Chatterjee. Learning control policies for stochastic systems with reach-avor guarantees. In Brian Williams, Yiling Chen, and Jennifer Neville, editors, Seirtt-Seventh AAAI Conference Artificial Intelligence, AAAI 2023, Thirty-Fifth Conference on Innovative Applications of Artificial Intelligence, IAAI 2023, Thirteenth Symposium Educational Advances in Artificial Intelligence, EAAI 2023, Washington, DC, USA, February 7-14, 2023, pages 11926- 1935, AAAI Press, 2023. doi: 10. 10.1609/aaii..o N371100...771000 [RtLt:tt:///oo
1609/ /00009//aa.... ww7.10. 26407
17

---

Appendix
A SPECTRL syntax and semantics and the proof of Theorem 4
Syntax A specification in SPECTRL is defined in terms of predicates and specification formulas. An atomic predicate is a boolean function a X' + {true, false} which for each system state specifies whether it satisfies the predicate, and predicate is defined as a boolean combination of atomic predicates. Specification formulas in SPECTRL are then defined by the grammar
(I) where b a predicate and Φi and de are specification formulas. Intuitively, achieve requires the agent to reach a state in which the predicate b is satisfied and Φi ensuring b requires the agent to satisfy the specification @ while only visiting states which the predicate is satisfied. The clause Φ1 Ø2 requires the agent to first satisfy specification Φ1 and then satisfy specification Φ2. Finally, Φ1 or 02 requires satisfaction of at least onc of the specifications Φ1 or Φ2.
Φ = achieve |
Φ1 ensuring Φ1: Ø2 Φ1 or Φ2
Semantics Given a trajectory = (x,, W and writing o = (x, u, wr) for its finite prefix of length K, the semantics of each SPECTRL clause are formally defined as follows:
P o
F
3K E No s.t. pK } #
+ achieve
3t Σ K s.t. p(p = true
k
+ éi ensuring p
k - 01 Vt S K. p(pt)) true
+ 01i02
K 3t S K s.t. Plo:t] } Φ1 and Pic: |= d2
pK - Φ1 or 02
p F ΦΙ or px -
Here, p. denotes the t-th state along pK, P(o:s denotes the prefix of pK consisting of the first + 1
K
states along R and P(t.K] denotes the suffix of pK that starts in the (t + 1)-st state along pK
Theorem 4. For each & E Finitary there exists d' E SPECTRL such that, for any word w. the word is accepted by @ iff the word w is accepted by 6'.
Proof. Let é be a finitary specification defined over the set of atomic predicates AP. Since ó is finitary, there exist a finite time horizon H and set L of words over AP of length H such that an infinite word over the alphabet AP is accepted by & iff its prefix of length H is contained in L. Define SPECTRL formula ø' via:
p(w1): p(w2); ...; p(wH)
where each p(w:) is an atomic predicate associated to the i-th letter in the word (Wi,... wH) and denotes sequential composition of SPECTRL specifications. Then, an infinite word accepted by é if and only if the prefix of w of length H is contained in L, which holds if and only if w is accepted by the SpectRL formula ø' This completes our reduction.
B Abstract Reachability Definition and Proof of Theorem! 5
Given a trajectory - = (xt: ut W;,W)) ) of the system and an abstract graph G = (V, E, B, s, t), we say that p satisfies abstract reachability for G (written p + G) if it gives rise to path in G that traverses G from to t and satisfies reach-avoid specifications of all traversed edges. Formally, we require that in and finite path to, U1,..., Uk
there exists sequence of time steps 0 in < é in G such that
1. X4, E ((1y)) holds for each 0 < j < kt and
2. X4 E B(15, Uj+1) holds for each 0 < j < k and in St
Intuitively, the first condition encodes that the trajectory satisfies reachability specifications of traversed vertices in G while the second condition encodes that it satisfies avoidance specifications of traversed edges in G. We then say that policy for the system satisfies abstract reachability for G
with probability E [0, 1] at an initial state Xo E Xy, if we have that Px lp E Ixo | |p= G] 2
We now provide the proof of Theorem 5
18

---

Theorem 5. Consider a stochastic feedback loop system with an initial set of states No C X and let be a SPECTRL specification. Then there exists an abstract graph G = (V, E, B, s, t) with [V in (léá) such that, for each trajectory of the system, we have = Φ if and only if = G. Hence, for
each policy a and initial state Xg E Ng, we have Pxo pp E 9xx P F Φ) = Px lp E 9xx P P
Proof. Given a SPECTRL specification @, one can construct an abstract graph G such that for each trajectory p of the system we have p - ø iff p - G as follows. First, the specification ø is parsed according to the grammar of SPECTRL in eq. | in order to construct the parse tree of abstract graph for each leaf formula in the parse tree, and
é. We then start by constructing traverse the parse tree bottom-up in order to construct abstract graphs of parent formulas. The abstract graph of the specification 6 is then obtained by taking the abstract graph constructed for the root in the parse tree. The leaves of the parse tree are formulas of the form achieve p. for which we construct an abstract graph with two vertices and t, a single edge
(s, and set ((s) = Xn. B(t) = {x E X p(x) = true) and ((e) = X. For a formula Φ ensuring p. we take an abstract graph (V, 8, for the specification Φi which was already constructed for the child node and define the abstract graph G = (V, E, E 8, t) by simply modifying the map / via E. For a formula Φ1; Φ2. we take the abstract graph of the specifications 6i and 62 which were already constructed for the child nodes and merge them by identifying the target node of Φi with the source node of Φ2 and using the region associated to it by the abstract graph of Φ2. Finally, for a formula Φ1 or t22, we introduce a novel source node with ((s) = Xy. take the abstract graph of Φ1 and Φ2 and connect the novel source node to them by an edge. Note that this construction yields graph with V in ((6)).
(e) =(ee) {x E X' p(x)= = true] for each
Since the above construction soundly encodes the semanties of each SPECTRL grammar element as a reach-avoid specification, it follows by induction on the depth of the parse tree that for each trajectory p of the system we have P & iff p F= G. The claim of Theorem 5 follows.
C Proof of Theorem 1
Theorem 1. [Proof in Apendix C The following two statements hold:
1. If a continuous function V X - IR is an (e,A)-additive RASM, then it is also a , }}, m)mulipplicattee RASM.
2. If continuous function V X + R is (7, mimuliipllccatee RASM, then it is also an ((1 - -7)- 8, addddiiivee RASM.
Proof.
1. Let d = min(e, }} and y z To show that V is (7, 8, X\-multipiccatiee RASM, we need to show that the Striet positivity outside X, and the Multiplicative expected decrease conditions hold. By the Additive expected decrease condition, for each x E X,,, at which (xx) < À we have V(x) 2 So as å minfe, A}. the Striet positivity outside X, follows. On the other hand, observe that for every x E X', at which V(x) I X, we have
Eusdd E [V((xx V(x)
V(x) - V(x) S
X =7,
where the first inequality follows by the Additive expected decrease condition and the second inequality follows since ع= is monotonically increasing on the domain 2 > e. Hence, the Multiplicative expected decrease condition holds.
2. Let e = (1 - 7) 5. To show that V is an (e, A)-additive RASM, we need to show that the Additive expected decrease condition holds. We show this by observing that, for each x E X' such that ((x) I X, we have
V(x) Eg (f(x, π (x). W)]l 2 ((x) 7 V(x) = (1 (1-7) 7) V(x) 2 (1 - -7) 77)7)))0 8,
where the first inequality holds by the Multiplicative expected decrease condition and the last inequality holds by the Striet positivity outside X4 condition. Hence, the Additive expected
decrease condition is satisfied.
19

---

D Proof of Theorem 2
We first provide an overview of definitions and results from martingale theory that we use in the proof. We then present the proof.
Probability theory A probability space is triple (1, F,,F,P) of state space Q sigma-algebra JF and probability measure that satisfies Kolmogorov axioms [64]. A random variable in (S2, F,P) is function X 12 + & that is F-measurable, i.e. for each E IR we have {w Q X ((w) S a) F. (discrete-time) stochastic process is a sequence (X,) of random variables in (2, F.P..
Conditional expectation Let X be a random variable in (2, Given sub- uub-sigma-algebra F' S F. a conditional expectation of X given F' is an -mmeaurrable random variable Y such that, for each A E F", we have
E I(A) = E|y I[A]].
Here, 1(AA) Q {0,1} is an indicator function of A. given by [(A)(W) i A, and (w) = 0 if w & A. Intuitively, conditional expectation of X given F an F'-meauurable random variable that behaves like X upon evaluating its expected value events in F. It is known that every nonnegative random variable admits a conditional expectation [64]. Moreover, the conditional expectation is almost- surely unique, meaning that for any two F'-measurable random variables Y and Y' which are conditional expectations of given F we have P[Y = Y = 1. Therefore, pick any such random variable as a canonical conditional expectation and denote it by E[X] [F].
Supermartingales Let (0, F. P) be a probability space and (Fi) o be an increasing sequence of tii--sim--ageeebb in F, i.. Fo S F C S F. A nonnegative supermartinggae with respect to (FF) is stochastic process (X;),= such that each X; is F.-messurable, and X;(w) 2 0 and E[X++1 [i)(w) (i(w)) hold for each w Ω and 2 0. Intuitively, the second condition is the expected decrease condition, and it formally captured via conditional expectation.
We now present two results from martingale theory that will be used in the proof. Let (2, be probability space and (Fi) be an increasing sequence sub-o-algebras in F.
Theorem 6 (Supermartingale convergence theorem (64]). Let (X;);=o be a nonnegative supermartin- gale with respect to (Fi) Then, there exists random variable Xx0 in (Ω, IP) to which the supermartingale converges to with probability 1, i.e. Pllim;->oc X, Xxo =
Theorem ( (35)). Let (x be a nonnegative supermartingale with respect to (F)) Then,
for every X > 0, we have
X[Xo]
IP sup X,
120
Theorem (Proof in Appendix D Lery E (0, 1). 8 > 0 and L, and suppose that : X is (7, 8, A\-multiplicative RASM with respect to X, and X.,. Suppose furthermore that V is Lipschitz continuous with a Lipschitz constant Lv, and that the system under policy π satisfies the bounded step property, i.e. that there exists A > 0 such that ||x fxx m(x),))ll < A holds for each x E X and w W. Let N 1(> (Lv A)J. Then, for every Xa Ny, we have that
P Px, ReachAvoid(X,, Xx) 2 ..
Proof. Fix an initial state E No. We need to show that I R. with N = [(> - 1L A)
Before proceeding with the proof, we define some notions. Consider the probability space (Dxm, Fx Px,)) over the set of all system trajectories that start X E Xo. For each time step t E No. define Fx.,t S Fx, to be a sub-o-algebra which contains events that are defined in terms of the first states along a trajectory. Formally, for each j E No. let C, Oxp + X' assign to each trajectory / (x,, ur ur,wy w.n,,, E 2x the j-th state x, along the trajectory. F; is then defined as the smallest algeera over Qxo with respect to which Co, Ci,..., C2 are all measurable. The sequence ( defines filtration in (8xo F IP )
20

---

Proceeding with the proof, we show that V induces supermartingale in the probability space (0xx Fxx,Pxx)) over the set of all system trajectories that start X, E Xg. For each E No, define random variable X₁ in (Axo Fxo= xxx)) via
(x+),
xf & 23 and ((x.) < A for all 0 s i t
xx(0)=
= 0,
x; E X for some 0 S i S l and V(x;) < X for all 0 S Si
X,
otherwise
for each trajectory p= (xx, Uz Me,wk)enN, E Ωxx Intuitively, X, is equal to V at until either the target set X; is reached upon which X₁ is set to O or some V(x,) 2 is reached upon which X, is set to X. We claim that (X is a nonnegative supermartingale with respect to the filtration =) in the probability space (Ixa: Fxa: Pxx) and that it with probability 1 converges to either 0 or to value that is X.
Clearly, each X₃ is nonnegative. To prove that (X)) a supermartingale, note first that each X, is Fx measurable as it is defined in terms of the ferst t states along trajectory. To show that the expected decrease condition is satisfied, we show that Ex, [X F Fxx.e((p) S (p))) holds for each t E No and (x,, U, wi W.eNN We consider 3 cases based on the definition of V:
1. If Xo, XI,.... X X2 and (xx)) for each 0 < i i L, then
E Ex, [X(+1 (())
+ = Exx Xe+1 [(xx+1 E 2e A ((x(+1) < A) + I(x++1 E 2))+ IIV((x(+1) 2 211) I Fox (p)
= -Pxxo (X++1 [(x++1 & X,) Fx) + +0+ A R[T(V(x(+1) 2 | Fx)
< &EwwalV (V (xx(xx, U1 wi)) I(x++1 & X, A ((Xe+1) < <]]
+ E [V (x((x Ur wi)) ) [[xx+1 E Xx]
Ra [V[((x;; we) I(V(x++1) 2 A)]
E (V((x), ue,ww))
Sy (x,,) & (xx.).
The first equality follows by the law of total probability, the second equality follows by definition of X,, the third inequality follows by observing that V(x++1) 2 (p) if X(+1 E Kr, the fourth equality is just the sum of expectations over disjoint sets, and finally the fifth inequality follows by the Multiplicative expected decrease condition of V and the assumption that x & Xg and V V(x:) < X.
2. If x, X2 for some 0- i S t and V(x,) < À for all 0 s j S i, then we have [X+11| =p).:((p)= = 7 Xx+1 = Xx+1(p) = 0.
3. Otherwise, we must have V(x;) 2 À and Xo. X & X, for some 0 S 4, thus
E Ex, [X (p) = X (p) = A.
Hence, we have proved that (x is a nonnegative supermartingale.
By Supermartingale Convergence Theorem, we then know that (X+) with probability 1 converges to some value. We claim furthermore that this value is either 0 or 2 À and that the value is attained. To see this, recall that in Theorem we showed that V is also an (c, Aeaddiiiee RASM with in the case one above shows that
== 7) 5. Then, the same sequence of inequalities [X+11 (pp) < (p) - e if Xo, xi...., Xx & X, and V(x,) < A for each 0 S iis t. Thus, the limit to which (x)) converges cannot be in the open interval (0, A) and the claim follows.
To prove the theorem claim, we show that (7 converges to value with 2 > with probability at most 1
I .y... Then, since (x converging to 0 implies that system reaches state in which V < 8 while never reaching a state in which V 2 X, which by the Safety and the Strict positivity outside Xr conditions implies that reach-avoidance is satisfied, this will imply the theorem claim. The proof until this point analogous to the proof of 668 Theorem 1].
The technical novelty of our proof begins in the following step. We define another stochastic process ( from (x by letting
X//r Yr-1,
V < x for all 0 Sist
y,
otherwise
21

---

We claim that (o is also a nonnegetive supermartingale with respect to the filtration (Fxx = The nonnegativity part of the claim clearly holds since each X, is nonnegative. To check the expected decrease condition of supermartingales, for each / E No and for each Gxx we have distinguish two cases:
1. If (x,) < A for all 0 Sis t, then
Exo 1Y441 Fp).e(p)
Exx (Y+1 [(V(xx+1) < A) Fxa,)((p) + Exo (Y--1 -VC---I(V(x..... (X(((x++1) 2 A) Fxo,1(0)
get1 Exp [X+11 I(V(xx+1) < 2) Fxo, + Ex, [Y I(V((x+1) 2 A) F Fx)
1
1
70-1 -xx (X++1 [Fxor[(0) 7
Bxx (X411 I(V(xx++1 2 A) Fxx,)(())
- Exx (Y VIV.IVVV (X((x)+1) 2 A) ((p)
1
S g/-1 -8. (x((p)) -Exo get1 X(+1 - Vi) IVV(xx+1) 2 A) Fxx,)((P)
1
= -Y(()- - Exo [1 الFF -x+1-
- Yt) 1(V 2 A) [p))
S (p()).
The first equality holds by the law of total probability. The second equality holds by the definition of Y++1. The third equality holds by the law of total probability. The fourth inequality holds since above we proved that (x
Fxx, S X,, whenever V(x,) < À for all 0 S i I t (cases 1 and 2 above). The fifth equality holds by definition Y. and the assumption that Vx,) < X for all S S t. Finally, the sixth inequality follows by observing that in the case when Vxx) < À for all 0 S < t but V(x++1) 2 X, we have X441/7 (+1 Z a/7 (+1 2 X/7² 2 Y,
2. If (x,, = X for some 0 S i S then Ex, (Y4+) Fx.. Y((p) Y.(p).
Hence, we have proved that f is a nonnegative supermartingale.
We conclude the theorem claim by observing that
Px sup
X₁
< A = Px, sup y- Yt < 11 = Pxo 120
sup 7th 12N
Y. < A
120
P xo 7
supp 7" N Y, < 1
= Pxo
sup
--N N Yr <
7N
A
1
12N
A
1
P x0
sup Y:
< 7
P x
sup Y, 120
2
1
12N
7
Three non-trivial steps are the first and the second equality and the last inequality. The first equality holds since, if sup X, < X, then we also have Y. = X,/>² for each é by the definition of Y, The second equality holds since the system cannot reach a state in which 2 x and so X, 2 X in the inequality in Theorem 7
less than N time steps. On the other hand, for the last inequality Applying the inequality to (Y1) and A and observing that R[Y] E[Xo] < by the Initial 7
condition in Definition 2 yields Pxx,, [suprzo Yt 2 1/7M S x and thus the last inequality.
E
Learning Policies with Reach-avoid Supermartingales
We now present the POLICY+RASM, subprocedure that we use for simultaneously learning a policy Ta and an RASM Vo. both of which are parametrized as neural networks with parameters μ and 6. The subprocedure POLICY+RASM is identical to the algorithm of [68). thus we keep this exposition brief and refer the reader to 68 for details. The reason why we can reuse this algorithm even though learns additive RASMs is that additive and multiplicative RASMs are equivalent by Thereom [ As we show below, the algorithm does not need to explicitly set an additive term or multiplicative factor 7, thus it is applicable to learning both additive and multiplicative RASMs. We then show how to use Vo to extract the bound in Theorem 2
22

---

Analogously as in [68], the value À 2 1 in Definition is an algorithm parameter and we initialize it I-p' so that the Theorem 2 bound 1 x > - = p' implies satisfaction of the desired probabilistic reach-avoid specification. If the algorithm succeeds learning zy and Va with this value of X, then the reach-avoid problem is solved. Otherwise, the algorithm gradually decreases the value of À and tries to relearn тy and Vi so that the resulting bound in Theorem still exceeds p'. Thus, our new bound also yields improvement in the algorithm.
The algorithm consists of two modules called learner and verifier, which are composed into a loop. In each loop iteration, the learner first learns a policy nμ and an RASM candidate Vg. These are then passed to the verifier which formally checks whether Vi satisfies all conditions Definition 2 If the verification is successful, the algorithm returns the policy. Otherwise, the verifier identifies counterexample states which the additive RASM conditions are violated. These are then passed to the learner and are used to fine-tune the previously learned policy and RASM by refining the loss function using the computed counterexamples.
Learner A policy TH and an additive RASM candidate Vo are learned by minimizing the loss function
[(0,v) v) Lini + Unsafe (v) + LDe + LLapschiuo v).
The first three loss terms are constructed from the sets Cina, Cunsate and Cdce which are initialized by computing finite discretizations of Xo, R₂ and X and are later extended by counterexamples computed by the verifier. The loss terms are used to guide the learner towards learning true additive RASM which satisfies the Initial, Safety and Expected decrease conditions. Each loss term is designed to incur loss a counterexample whenever that counterexample violates the corresponding condition. In order for the Nonnegativity condition to be satisfied by default, the algorithm applies the softplus activation function to the output of Vg. The loss term Lipschitz (6, v) is a regularization term that does not enforce any of the defining conditions of additive RASMs, however it helps in decreasing the Lipschitz constants of neural networks. Each loss term is defined as follows:
(ini(V)= = max (x) - 1,0}
xECiii
1
(u)sate(V) = max
V2(x).0}
xECunale
1-p p
1
DDecrense (0, Cdacel
V= To (x), (x))) Vo(x) + K, K.0})
max
N
XE XCCrra
The last loss term L1 Sp.ppchi (0, = L. (pripschit + Liipschnz (v)) is the regularization term used to guide the learner towards learning neural networks whose Lipschitz constants below tolerable threshold p, where t >> 0 is a regularization constant. By preferring networks with small Lipschitz constants, we allow the verifier to use wider mesh and thus make verification condition easier to satisfy. We have The regularization term for To (and analogously for V2) is defined via
L Liipcchite (0) max
II max Σ Was - -1,0
W,bEo
where W and weight matrices and bias vectors for each layer in ne.
Verifier The verifier checks whether Vo satisfies the defining properties of additive RASMs in Definition 2 Recall, the Nonnegativity condition is satisfied by default due to the softplus activation function applied to the output layer of Vg. Hence, the verifier only needs to check the Initial, Safety and Expected decrease conditions.
Since f. म. and Vo are continuous functions defined over compact domain X' thus also Lipschitz continuous, the verifier may check the (both Multiplicative and Additive) expected decrease condition by checking slightly stricter condition at finitely many discretization points. A discretization of the is a finite set X C such that, for every x E X, there exists x X such that ||x x||1 < r. The discretization is computed by taking grid of mesh r. Then, to check the expected decrease condition, it was showed in (68) that it suffices to check for each x e X whose
state space X with mesh
23

---

adjacent discretization grid cells contain non-target state and over which V attains a value that is less than or equal to À that
Eaann Vo Vo(((i (1x (x)))) VV(()) - T K,
where K K= Ly (I.g (T> + 1) + 1) and T,g, T. and Ly are Lipschitz constants of f. n. and Vo. It is assumed that T.5 is provided and T and Ly are computed by the method of (57]. To verify the Initial condition, the verifier collects the set Cellsx, of all cells of the discretization grid that intersect the initial set Xo. Then, for each cell Cellsx. it checks if s cell (x(x) S where the supremum is bounded from above by using interval arithmetic abstract interpretation (IA-AI) (22 p7 to propagate across neural network layers the extreme values that Vú can attain over a cell. Similarly, to verify the Unsafe condition, the verifier collects the set Cells of all cells of the discretization grid that intersect the initial set Nz Then, for each cell E Cellsx.. it uses IA-AI to check if infx cell (x(x) 2 A.
If the verifier shows that Vo satisfies the above checks, it concludes that Vo is additive (and therefore multiplicative) RASM for the system under the policy тμ and returns the policy together with the lower bound on the probability of satisfying the reach-avoid specification in Theorem 2 The fact that the verifier is correct was proved in [68, Theorem 2]. Otherwise, if a counterexample x to any of the checks is found, it is added to one of the three counterexample sets Cinit Cansafe and Case that are then used by the learner to fine-tune V/8 and T...
Soundness and computation of 7. The following theorem establishes that the above is a sound verification procedure and provides a closed-form expression for the values of 8 and y E (0, 1) for which Vo is a (7, 6, A) A)-mutiiplicative RASM. Hence, to compute the lower bound on the probability of satisfying reach-avoidance in Theorem 2 one may the value of implied by the theorem together with A which is fixed by the algorithm, Ly which is computed by the algorithm and the maximal step size A which assume is provided by the user.
Theorem 8. If the verifier returns neural networks Ty and Vo. then Vo is a (7, 8, m)multiplicaatve RASM with
(V((x) - T- K Euwn (V 2), 7 7= SEP
8 X
8 = min
min
Proof. Since it was shown in [68] that the verifier provides a sound verification procedure for checking that Va is an additive RASM, by the equivalence in Theorem [ follows that it is also sound for checking that Va is a (7, 6, A)-multiplicative RASM for some values of and 5. Hence, it remains to show that the values of y and the theorem statement are correct.
First, we show that the Striet positivity outside Xe condition is satisfied with the above value of ó. To see this, let x E X'. Since 8 < X, suppose without loss of generality that (x(x) S X. Then, x is contained in a discretization grid cell which contains non-target state and over which V attains a value that < A. Hence, the verifier has shown that (Vo n ()) < Vo(x) - 7 K
holds for each x E X which is a vertex of this cell. Taking a vertex x E X of this cell for which ||x x|| r. by the definition of Lipsethiz constants we have
(f(x, [w)]
Bund
$ Ewwd
V (f(8, T (x) w))
+ [l, (x), - f(x, x xx)) Lv + ||(,, x (x)) w) (x, (xx., w|ll Lv Ls
v (F(xx (x);, w))
< Ennnd
Ensnd
V (f(x; (xx), w))
+ +||* +| -x||||i LL Lg (1 + La)
Ewwnd
(S(R, (x) w))
+ Ly Lg (1 + Lz).
24

---

Hence, by the Nonnegativity condition we also have
V(x)= 2 V(x) - Bunrd V (f(x, (((xxx((x).))) x(x))
2 V(x) T. Lv - Bundd ((x)
- Lv Tig (1 + Ii=)
(2)
V(x) -- K- - (X(2
26,
since K = Lv (L. (Lx + 1) + 1), which concludes the proof.
Second, show that Multiplicative expected decrease condition with the above value of holds.
Let x E A3 be such that (x)x) < A. We need to show that V(x) 2
+))]
Since we showed in eq. that ((x) 2 V(x) Ra (V ( (x), 2 ō > 0 and since Ve(x)= I A, we have
Euwal ( (x),
V(x) Bund (V (f n (x),
V(x)
V(x)
6
V(x)
This concludes the proof.
F Proof of Theorem
Theorem 3.
[Proof in Appendix Algorithm 7 is compositional, and if it outputs policy æ, then π guarantees the probabilistic specification (6.p).
Proof. In order to prove that æ guarantees satisfaction of the probabilistic specification (d.p), by Theorem i suffices to show that : satisfies abstract reachability for the abstract graph G with probability at least p.
To prove abstract reachability for with probability at least p. we show that random trajectory of the system under policy π satisfies reach-avoid specifications of the edges along the finite path Pio U;..... U1,
exhibited above with probability at least p. To prove this, we proceed by induction on 0 < j S & to show that random trajectory of the system under policy satisfies reach- avoid specificatiins of each edge along prefix s = Vio U/ :....... U; of this path with probability at least Prob(u;,) [.,, Recall, Prob the dictionary computed by Algorithm [
Abstract reachability for G with probability at least p then follows if we set k, since Vi and must have Prob[t] for Algorithm to output a policy (lines 15-17).
The base case = 0 follows trivially since the system starts in the initial region B(s) Xo and since Prob[u.,] = Prob[s]
by line 6. For the inductive step, suppose that 0 S j k: - and that π satisfies reach-avoid specifications of each edge along at least Prob[u;,] The claim for the prefix of length j + 1 then follows by our construction of the finite path s Ugg ..., Ui2 as it implies that Algorithm has successfully learned an edge policy for the edge (Vi,, Uiy+1) that ensures satisfaction of the associated reach-avors specification with probability at least P(r,,,.;,44 .1,4)) and for which Prob[e,,.a = P(e., P(es, Prob[ui,]. Since the -ight-hand-side of this equality is lower bound on the probability of satisfying reach-avoid specifications of each edge along = U/ Uyy..... Va multiplied by a lower bound on the probability
Vigo . Vi, with probability
of satisfying the reach-avoid specification of the edge (Ma Uists ). the claim follows. This concludes the proof by induction.
25


Reviews:
[{"review_id": "ifQ4lgzBk4", "reviewer": "Reviewer_Dssn", "summary": "The paper presents CLAPS, a compositional RL algorithm that also ensures guarantees of correctness when learning from temporal specifications. The core contribution of this work revolves around guarantees. \n\nPrior works in compositional RL with guarantees apply to deterministic environments and/or ones with linear dynamics. This work presents an algorithm that is suitable for stochastic environments with non-linear dynamics. The algorithm builds on two prior works., namely [61] that learns policies for control systems with non-linear dynamics with reach-avoid guarantees and [30] that compositionally learns policies (without guarantees) from temporal specifications. An empirical evaluation on 9-rooms environment over a suite of source and target states shows the efficacy of the approach in learning long-horizon tasks with guarantees.     ", "questions": "I am quite unclear as to how the guarantee extends compositionally. From my understanding, a critical challenge in obtaining guarantees from compositional approaches such as [27] is that one needs to ensure the guarantee at the transition point between two edges, ie., in the region where one policy ends and the other begins. Could you clarify how that is accounted for in the proof of Theorem 5?\n\nThe example I have in mind is as follows: Say, one of the subgoal regions is split by a wall such that a learn policy entering the subgoal region ends before the wall and the policy exiting the subgoal region exits from the other side of the wall. The probability of connecting these two policies is clearly not 1. How is the guarantee in CLAPS accounting for such scenarios?\n \n", "limitations": "See above. I can change my score based on the clarification of the question above. ", "rating": 5, "confidence": 4, "soundness": 2, "presentation": 3, "contribution": 2, "strengths": "RL from temporal logic to learn long-horizon tasks is a promising and thriving research community. This paper makes a strong contribution in that space by learning policies with guarantees in stochastic systems with non-linear dynamics. ", "weaknesses": "The empirical evaluation can be strengthened. Please find concrete comments below:\n\n1. The evaluations have been presented for one environment only. The 9-room environment is somewhat low-dimensional. I am curious about how the approach may scale to higher dimensional environments.\n2. Is there a comparison between the sample complexity of CLAPS with prior compositional approaches such as DiRL? This could offer a study of tradeoffs for guarantees.   \n3. Would it be possible to compare CLAPS to [27] on the benchmarks that would be common to both? It would be interesting to see how the formal guarantees of both approaches compare.  ", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for the valuable feedback. In what follows, we answer the questions raised by the reviewer.\n\nWe clarify that Theorem 5 in the Appendix only states that a trajectory satisfies a SpectRL specification if and only if it satisfies abstract reachability in the abstract graph associated with the specification. Therefore, the probability of a SpectRL specification being satisfied is equal to the probability of abstract reachability being satisfied. However, Theorem 5 does not consider composition of reach-avoid guarantees associated to two edges.\n\nThe composition guarantees are obtained by our composition of edge policies described in l.321-343 and proved correct in Theorem 3.  For each edge $(v_1,v_2)$ in the abstract graph, CLAPS synthesises an edge policy $\\pi_{v_1,v_2}$ together with a lower bound $p_{v_1,v_2}$ on the probability of satisfying the reach-avoid specification associated to the edge (line 10 in Algorithm 1). The lower bound $p_{v_1,v_2}$ is the worst-case lower bound for *any initial state* in the region associated with the source vertex $v_1$.\nHence, when composing guarantees of edges $(v_0, v_1)$ and $(v_1, v_2)$, CLAPS considers the worst-case state in the region associated to $v_1$ in which the agent may end up upon executing the policy associated to $(v_0,v_1)$, before moving on to the policy associated to $(v_1,v_2)$. Hence, the lower bound computed by CLAPS on the probability of satisfying the specification obtained by composing edges is $p_{v_0,v_1} \\cdot p_{v_1,v_2}$. Our composition described in l.321-343 and proved correct in Theorem 3 formalises this reasoning and ensures that the guarantees obtained by composing edge policies are indeed correct. We will clarify this further in the final version of the paper.\n\nIn the example described by the reviewer, this means that CLAPS would compute (1) a lower bound $p_{v_0,v_1}$ on the probability of satisfying the reach-avoid specification of the first edge, (2) a lower bound $p_{v_1,v_2}$ on the probability of satisfying the reach-avoid specification of the second edge (which would be attained in a state before the wall), and would conclude the lower bound of  $p_{v_0,v_1} \\cdot p_{v_1,v_2}$ of satisfying the composition of two reach-avoid specifications."}, {"review_id": "smwgJLUWlN", "reviewer": "Reviewer_kcWZ", "summary": "This paper introduces CLAPS, a compositional method designed for learning and verifying neural network policies in stochastic control systems. By considering control tasks with specifications expressed in the SPECTRL language, CLAPS decomposes the task into an abstract graph of reach-avoid tasks. It utilizes reach-avoid supermartingales to offer formal guarantees on the probability of reach-avoidance in each subtask. Additionally, the paper establishes proof demonstrating that RASMs (Reach-Avoid Supermartingales) provide a significantly more stringent lower bound on the probability of reach-avoidance compared to prior approaches. The experimental evaluation conducted in the Stochastic Nine Rooms environment showcases the ability of CLAPS to derive guarantees for global compositional policies.", "questions": "+ Can the proposed Reach-Avoid Supermartingales (RASMs) approach be formally characterized in relation to exponential barrier certificates?\n\n+ Have you considered applying Statistical Verification of Learning-Based Cyber-Physical Systems (https://cpsl.pratt.duke.edu/sites/cpsl.pratt.duke.edu/files/docs/zarei_hscc20.pdf) to the Nine Rooms environments?", "limitations": "The paper would benefit from a more comprehensive discussion and extensive experimentation regarding the advantages of the probabilistic verification approach over stochastic verification within the context of compositional policy learning.", "rating": 4, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "+ Compositional Learning is an important research direction. The approach presented in this paper provides correctness guarantees for individual sub-policies that can be used to collectively ensure the correctness of the global policy, making the learning and verification approach valuable for applications where safety and reliability are critical. The ability to verify and validate each component of the policy offers a robust and trustworthy framework for developing complex control systems.\n+ Taking inspiration from exponential barrier certificates developed in the control theory community, the paper introduces a conceptually similar concept to improve Reach-Avoid Supermartingales, which provides a more strict lower bound on the probability of reach-avoidance guarantees (compared with prior work [61]).\n+ The main algorithm is easy to understand, follow, and implement.", "weaknesses": "The proposed approach falls short of advancing the state-of-the-art in compositional learning and verification. While Reach-Avoid Supermartingales in prior work makes sense for providing probabilistic correctness guarantees for infinite time horizon systems, the expectation for a global policy composed of sub-policies is that each sub-policy terminates within a finite time horizon. Simpler techniques such as statistical verification, which relies on drawing a large number of samples and employing concentration inequalities, can achieve high-probability correctness guarantees for finite horizons. Consequently, the paper lacks a compelling argument showcasing why their probabilistic verification approach surpasses a straightforward statistical verification approach for compositional policies. Strengthening the paper would involve demonstrating that the probabilistic verification approach indeed outperforms stochastic verification in practice.\n\nIn the specific context of the Stochastic Nine Rooms environment examined in this paper, it seems that the robot can reach the goal within a finite time horizon. Given the convergence of PPO sub-policies, it is reasonable to anticipate that stochastic verification methods can yield substantially higher probabilistic guarantees compared to the reported result of 33% in the paper's probabilistic verification approach.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for the valuable feedback. In what follows, we answer the two questions raised by the reviewer.\n\n**Comparison of RASMs and exponential barrier functions.** Stochastic barrier functions were introduced for proving probabilistic safety in stochastic dynamical systems, i.e. without the additional reachability condition of reach-avoid specs (Prajna et al. “Stochastic Safety Verification Using Barrier Certificates”, CDC 2004). If we are only interested in probabilistic safety, RASMs reduce to stochastic barrier functions by setting $X_t = \\emptyset$ together with $\\epsilon = 0$ in Definition 2 for additive RASMs, and $\\gamma = 1$ in Definition 3 for multiplicative RASMs. This was discussed in Zikelic et al. “Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees”, AAAI 2023, who introduced additive RASMs.\n\nTo the best of our knowledge, exponential barrier functions for stochastic dynamical systems have been considered only for finite time horizon systems in which the time horizon N is fixed and known a priori (Santoyo et al. “A Barrier Function Approach to Finite-Time Stochastic System Verification and Control”, Automatica 2021). Exponential barrier functions also impose a multiplicative expected decrease condition, similar to our multiplicative RASMs. This allows them to provide tighter bounds on safety probability compared to classical stochastic barrier functions, which are tighter by a factor which is exponential in the time horizon N (Theorem 2 in Santoyo et al.). However, as $N \\rightarrow \\infty$, their bound reduces to the bound of Prajna et al.\nIn contrast, Theorem 2 in our paper shows that our multiplicative RASMs provide tighter bounds on safety (or more generally, reach-avoid) probability even in unbounded (i.e. indefinite) or infinite time horizon systems.\n\n**Comparison of CLAPS and statistical verification.** We clarify that, while satisfaction of a reach-avoid specification (and, more generally, any SpectRL specification) can be witnessed by a finite trace, one needs infinite traces to witness that a reach-avoid specification is not satisfied. For instance, in the Nine Rooms environment, one can design a policy under which a trace remains stuck in one room indefinitely without violating safety constraints and without reaching the target room. However, one cannot witness this by sampling finite traces, since any finite trace can also be extended to an infinite trace that eventually leaves the room.\nOne way to overcome this limitation would be to sample traces of some fixed length and then treat all longer traces as either satisfying or violating the specification. However, such an approach would either be overestimating or underestimating the probability of a trace satisfying the specification and would not provide statistical guarantees. This means that statistical methods are applicable to and effective in finite time horizon systems, but they are not applicable to our setting. Our algorithm (CLAPS) provides formal guarantees even for unbounded (i.e. indefinite) or infinite time horizon systems. This is because the guarantees provided by RASMs do not impose any restrictions on the time horizon.\n\nWe will incorporate the above discussions into the final version of the paper, as we believe they will strengthen the paper.\n"}, {"review_id": "fKsQEKINem", "reviewer": "Reviewer_E1c8", "summary": "This paper introduces CLAPS (Compositional Learning for Probabilistic Specifications), a new method for learning a composition of neural network policies in stochastic environments, together with a formal certificate which guarantees that a reach-avoid specification over the policy's behavior is satisfied with the desired probability.\nThe proposed approach is evaluated empirically on a stochastic Nine Rooms environment.", "questions": "p. 4: When the authors say \"if the probability of a random trajectory...\", do they actually mean \"if the probability of any trajectory...\"", "limitations": "p. 9: The authors mention that \"the systematic decomposition used in our algorithm has advantages over manual task decompositions\". They might discuss these advantages further.", "rating": 7, "confidence": 4, "soundness": 4, "presentation": 4, "contribution": 3, "strengths": "1) Different to previous works discussed by the authors, the CLAPS method is applicable to stochastic control systems, that may be defined via non-linear dynamics functions.\n\n2) The approach is compositional. Complex tasks are analysed and solved in terms of simple tasks, that are then combined in order to achieve the overall goal.\n\n3) The literature is discussed in detail. The bibliography, at 61 items, is an excellent overview of current methods in safe RL.\n", "weaknesses": "1) A lot of material appears in the appendix. I did not check it, but the paper appears to be consistent.\n\n3) This work builds on top of [61] as regards the use of supermartingales. However, the bounds obtained are stricter, which seems to justify the claims to novelty (together with the compositional approach). \n\nMinor, p. 3: When discussing the equation for the stochastic feedback loop system, u_t is described as the control action even though no u_t appears in the equation. On the other hand, function \\pi is not described. I understand that \\pi: X -> U is the policy and \\pi(x_t) = u_t.\n", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for the valuable feedback. In what follows, we answer the question raised by the reviewer.\n\nIndeed, on p. 4 we mean “if the probability of any trajectory”. This sentence refers to trajectories sampled from the probability space of all trajectories starting in initial state $x_0$, where the probability space is defined by the Markov chain semantics of the system under a control policy. We will clarify this in the final version of the paper. \n\nWe will also address the minor remark on p. 3 and write $\\pi: X \\rightarrow U$ and $u_t = \\pi(x_t)$ when defining the dynamics. We will also further discuss the advantages of systematic decomposition on p. 9."}, {"review_id": "p4zMzkr16O", "reviewer": "Reviewer_6cWz", "summary": "This paper proposes a verifiable RL framework that learns a composition of NN policies for stochastic control systems, along with a formal supermartingale certificate for the safety probability of satisfying the reach-avoid specification. It decomposes the global reach-avoid task into a DAG with edges denoting subtasks which are solved by policy+RASM. Finally, it composes the low-level subtask's policy into a global safe policy with probability guarantees. The authors evaluate this framework in a relatively simple Stochastic Nine Room environment.  ", "questions": "1. What are the relations between (either additive or multiplicative)  RASM and barrier certificate for stochastic (either continuous or discrete) systems? \nThe definition of the barrier certificate can be found in the following references. \n\nb) Stochastic safety verification using barrier certificates. \n\nc) A Barrier Function Approach to Finite-Time Stochastic System Verification and Control. \n\n2. What's the complexity of the proposed algorithm? It should be feasible to conduct the big  O complexity analysis as the algorithm is built on top of topologic sorting, binary searching, etc. \n\n\n", "limitations": "This paper may face a scalability problem. ", "rating": 6, "confidence": 5, "soundness": 4, "presentation": 4, "contribution": 2, "strengths": "This paper is greatly written and easy to follow. The authors did a good job on the paper presentation. They study an important safe RL problem with step-wise safety chance constraint, which is suitable for safety-critical systems.\n\nThe proposed compositional safe RL framework is novel to me. \n\nThe proposed algorithm and approach are sound.  \n\nControl policy learning with formal guarantees in probability is significant. ", "weaknesses": "1. My biggest concern is the scalability problem of this paper, which might originate from the DAG representation. If the global RL task is too complex, the graph might be too huge to handle. \n\n2. Because of the scalability problem, the experiments in this paper look much simpler than other RL papers. \n\n3. The authors may miss a few recent papers addressing a similar safe RL problem with chance constraints, as in \n\na)  Enforcing Hard Constraints with Soft Barriers: Safe Reinforcement Learning in Unknown Stochastic Environments,\n\nas far as I can tell, this reference also considers continuous control problems with safety probability chance constraints, and its guarantees are also based on the supermartingale property, although the approaches are quite different. ", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for the valuable feedback. In what follows, we answer the two questions raised by the reviewer.\n\n**Relation between RASMs and stochastic barrier functions.** On the high level, the main difference between RASMs and stochastic barrier functions is that RASMs consider reach-avoid specifications, whereas stochastic barrier functions only consider safety specifications.\nHowever, if we are only interested in safety, additive and multiplicative RASMs reduce to stochastic barrier functions by letting $X_t = \\emptyset$ and $\\epsilon = 0$ in Definition 2 for additive RASMs, and $\\gamma = 1$ in Definition 3 for multiplicative RASMs. Here, we are referring to discrete-time stochastic barrier functions defined in Prajna et al. “Stochastic safety verification using barrier certificates”, CDC 2004. This was discussed in Zikelic et al. “Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees”, AAAI 2023, who introduced additive RASMs.\n\nOur multiplicative RASMs in Definition 3 syntactically resemble exponential stochastic barrier functions defined in Santoyo et al. “A Barrier Function Approach to Finite-Time Stochastic System Verification and Control”, Automatica 2021. Exponential stochastic barrier functions also impose a multiplicative expected decrease condition. However, they consider finite time horizon systems, where the time horizon N is given and known a priori, and show that exponential barrier functions provide bounds on safety probability which are tighter by a factor which is exponential in time horizon N . However, as $N \\rightarrow \\infty$, their bound reduces to the bound of Prajna et al. In contrast, in our Theorem 2 we show that our multiplicative RASMs provide tighter bounds on safety (or more generally, reach-avoid) probability even in unbounded (i.e. indefinite) or infinite time horizon systems.\n\n**Computational complexity.** The worst-case complexity of our algorithm is $\\mathcal{O}(|E| \\cdot RA)$, where E is the number of edges in the abstract graph and RA is an upper bound on the computational complexity of learning and verifying a reach-avoid policy. This is because both the topological sort and the forward pass on the abstract graph can be done in time which is linear in the number of edges.\nThe computational complexity of RA is $\\mathcal{O}(I \\cdot (L + V))$, where \\\n$I$ = bound on the number of learner-verifier iterations, \\\n$L$ = complexity of the learner, and \\\n$V$ = complexity of the verifier. \\\nIn general, the learner-verifier procedure is not guaranteed to converge (in which case our algorithm does not output a policy), so we introduce a parameter $I$ which is the maximal number of learner-verifier loop iterations per edge.\nGiven that we consider learning over continuous state spaces and given that our loss function is not convex, we cannot bound $L$ and also need to introduce a timeout parameter.\nFinally, we have $V = \\mathcal{O}((D / \\tau)^n \\cdot N)$ where $D$ is the diameter of the state space, $\\tau$ is the mesh of the discretization used by the verifier, $n$ is the dimension of the state space, and $N$ is the number of neurons in the policy and RASM neural networks. This is because, for each cell in the discretization grid, interval-arithmetic abstract interpretation can verify all RASM defining conditions in time linear in the size of the networks. On the other hand, in the worst case there are $\\mathcal{O}((D / \\tau)^n)$ cells in the discretization grid.\n\nThis results in a final bound on computational complexity\n$\\mathcal{O}(|E| \\cdot I \\cdot (L + (D / \\tau)^n \\cdot N))$\nwith the notation above.\n\nWe will incorporate the above discussions into the final version of the paper. We also thank the reviewer for pointing out the recent ICML 2023 paper. We will discuss the comparison to our work in the final version. In particular, this paper considers a model-free setting and jointly learns a policy and a barrier function-like certificate, however it does not provide guarantees on correctness of the learned certificate."}]

Author rebuttal:

Meta-review: The authors develop a novel framework for verifying properties of a policy given properties of subpolicies that are composed to arrive at the global policy. The approach enables compositional verification of temporal specifications for RL agents, and constitutes a valuable contribution to the literature. Reviewer kcWZ had a thorough and respectful discussion with the authors, and having read through it, I conclude that while the reviewer still leans towards rejection, they do not have any technical objections on the paper. Furthermore, other reviewers favor acceptance. Hence I recommend acceptance.
Decision: Accept (poster)