Safe reinforcement learning for dynamical systems using barrier certificates

Abstract

Safety control is a fundamental problem in policy design. Basic reinforcement learning is effective at learning policy with goal-reaching property. However, it does not guarantee safety property of the learned policy. This paper integrates barrier certificates into actor-critic-based reinforcement learning methods in a feedback-driven framework to learn safe policies for dynamical systems. The safe reinforcement learning framework is composed of two interactive parts: Learner and Verifier. Learner trains the policy to satisfy goal-reaching and safety properties. Since the policy is trained on training datasets, the two properties may not be retained on the whole system. Verifier validates the learned policy on the whole system. If the validation fails, Verifier returns the counterexamples to Learner for retraining the policy in the next iteration. We implement a safe policy learning tool SRLBC and evaluate its performance on three control tasks. Experimental results show that SRLBC achieves safety with no more than 0.5× time overhead compared to the baseline reinforcement learning method, showing the feasibility and effectiveness of our framework.

Keywords:

• Safe reinforcement learning
• safety control
• dynamical systems
• barrier certificates
• neural networks

1. Introduction

The synthesis of control policies for heating, ventilation and air conditioning systems, autonomous vehicles, and robotics is a fundamental problem for cyber-physical systems (Lin et al., 2018; Wei et al., 2017; Xu et al., 2018). Researchers have demonstrated that reinforcement learning is effective at learning policies to achieve goal-reaching property to solve complex tasks, i.e. controlling the system to obtain the expected long-term reward (Dong et al., 2020; Haarnoja et al., 2018). However, basic reinforcement learning methods do not provide safety guarantees and face the threat of unsafe behaviours, which is an obstacle to the use of reinforcement learning in safety-critical fields (Berkenkamp et al., 2017; Fulton & Platzer, 2018).

There is some recent work towards safe reinforcement learning, which tries to deal with the possible risk of unsafe behaviours (Garcıa & Fernández, 2015; Yang, Vamvoudakis, et al., 2020). A category of work takes into account uncertainty and applies appropriate risk measure costs to the reward, reducing the probability of unsafe behaviours by minimising the expectation of safety violations (Stooke et al., 2020; Thananjeyan et al., 2021). However, because safety is specified through safety costs, these methods only reduce safety violations and do not eliminate them (Srinivasan et al., 2020; T. Y. Yang et al., 2020).

To completely avoid unsafe behaviours, another category of work integrates external safety techniques, including control barrier functions, control Lyapunov functions, and safe backup policies into reinforcement learning (Alshiekh et al., 2018; Cohen & Belta, 2020; Ohnishi et al., 2019). These works propose sufficient conditions to guarantee safety property. However, the limitation of these methods is that the control barrier functions, control Lyapunov functions and safe backup policies usually need to be provided manually, or some prior knowledge is required (Bastani, 2019; Ravanbakhsh & Sankaranarayanan, 2019).

To guarantee safety property without relying on prior knowledge, this work integrates barrier certificates into actor-critic-based reinforcement learning methods in a feedback-driven framework to learn safe policies for dynamical systems. The barrier certificate guarantees that the system trajectories will not cross its zero level set to enter the unsafe states (Prajna & Jadbabaie, 2004). Therefore, the existence of a barrier certificate is a sufficient condition for system safety property. The insight of the proposed framework is that the barrier certificate is represented by a neural network, which is simultaneously learned along with the policy. Therefore, safety is naturally considered in the policy learning process and it does not need prior knowledge.

The framework of our approach is composed of two interactive parts: Learner and Verifier, as shown in Figure 1. Learner simultaneously trains three neural networks: the actor network, the critic network and the barrier network. The actor network represents the control policy; the critic network guides the actor to satisfy goal-reaching property; the barrier network is used as the barrier certificate to guarantee safety property. Since neural networks are trained on training datasets, the goal-reaching and safety properties that the actor satisfies on training datasets may not be retained on the whole system. Therefore, Verifier validates the two properties on the whole system. If the validation succeeds, the actor is a safe policy satisfying goal-reaching and safety properties. Otherwise, Verifier returns some failure experience or counterexamples to Learner to retrain the networks in the next iteration.

Figure 1. Framework of the feedback-driven approach.

The main contributions of the paper are summarised as follows:

• We propose a novel feedback-driven framework, which integrates barrier certificates into actor-critic-based reinforcement learning methods to learn safe policies for dynamical systems.

• We introduce how to synthesise safe policies without prior knowledge based on iterations between Learner and Verifier. The proposed workflow and techniques enable the policy to be trained and verified efficiently.

• We implement a safe policy learning tool SRLBC based on the deep deterministic policy gradient (DDPG) method, which only focuses on goal-reaching property for the learned policy. SRLBC is evaluated on three control tasks: Continuous Mountain Car, Pendulum, and CartPole. Experimental results show that SRLBC achieves both goal-reaching and safety properties with no more than 0.5× time overhead compared to DDPG, showing the feasibility and effectiveness of our framework.

The rest of this paper is organised as follows. Section 2 introduces some notions and definitions used in the paper. Section 3 shows how Learner trains the policy to satisfy goal-reaching and safety properties. Section 4 presents how Verifier validates the two properties. Experiments are displayed in Section 5. Section 6 discusses related work. Finally, Section 7 concludes the paper.

2. Preliminaries

This section briefly introduces the feedforward neural network, dynamical system, reinforcement learning and the definitions of goal-reaching and safety properties, followed by the introduction of the barrier certificate. Let $\mathbb{R}$ denote the field of real number.

2.1. Feedforward neural network

This paper focuses on the control policies that are represented by feedforward neural networks. A feedforward neural network $\mathcal{N}$ with n + 1 layers (from the 0-th layer to the n-th layer) is a tuple $⟨\mathcal{X},w,b,\varphi ⟩$ defined as follows:

• $\mathcal{X}=\{x_0,\dots ,x_n\}$ is a set of neuron outputs of each layer;

• $w=\{w_1,\dots ,w_n\}$ is a set of weight matrices;

• $b=\{b_1,\dots ,b_n\}$ is a set of bias vectors;

• ϕ is the activation function.

Let $z_k,k=1,\dots ,n-1,$ denote the neuron outputs in the kth layer before applying activation function ϕ, and the network forward propagation is defined as follows: (1) $\{\begin{array}{ll}{z}_k=w_k{x}_{k-1}+b_k,& k=1,\dots ,n-1,\\ x_k=\varphi (z_k),& k=1,\dots ,n-1,\\ x_n=w_n{x}_{n-1}+b_n.& \end{array}$(1) A feedforward neural network (hereinafter referred to as neural network for simplicity) receives the external input as the input layer neuron value $x_0$. The output of neural network $\mathcal{N}$ is the value of the output layer neuron, i.e. $\mathcal{N}(x_0)=x_n.$

2.2. Dynamical system

A dynamical system $\mathcal{H}$ is composed of a plant model and a control policy, which consists of a tuple $⟨s,\mathrm{\Psi },I,f,g⟩$ defined as follows:

• $s=⟨s^1,\dots ,s^n⟩$ denotes the system variable vector;

• $\mathrm{\Psi }\subseteq {\mathbb{R}}^n$ denotes the system space;

• $I\subseteq \mathrm{\Psi }$ denotes the initial states of the system;

• f denotes the local Lipschitz continuous vector field, representing the system evolution;

• g denotes the observation model of the system such as the observation output $y=g(s)$.

The system $\mathcal{H}$ considered in the paper is continuous and modelled by the ordinary differential equation as follows: (2) $\dot{s}=f(s,a),$(2) where $a$ is the control signal produced by the control policy π. The control policy π receives the observation of real-time system state x and outputs the signal $a=\pi (g(s))$ to control the system $\mathcal{H}$. It is assumed that the system variables are directly exported to the observation model, which means g is an identical function, i.e. $g(s)=s$. Then, the output of the control policy is determined as $a=\pi (s)$.

For a dynamical system $\mathcal{H}$, a neural network $\mathcal{N}$ serves as the control policy π, receiving system state $s$ as input to output the control signal $a=\mathcal{N}(s)$. Figure 2 displays a dynamical system controlled by a neural network policy.

Figure 2. A dynamical system controlled by a neural network policy.

2.3. Reinforcement learning

A reinforcement learning system consists of an agent interacting with the environment in continuous or discrete-time steps, represented as a Markov decision process (MDP). A MDP $\mathcal{M}=(\mathcal{S},\mathcal{O},\mathcal{P},\mathcal{R})$ is defined as follows:

• $\mathcal{S}$ denotes the system states of $\mathcal{M}$;

• $\mathcal{O}$ denotes the action space of $\mathcal{M}$;

• $\mathcal{P}:\mathcal{S}\times \mathcal{O}\to P_r(\mathcal{S})$ denotes the probabilistic transition function about $\mathcal{S}$ and $\mathcal{O}$;

• $\mathcal{R}:\mathcal{S}\times \mathcal{O}\to \mathbb{R}$ denotes the reward obtained after transiting from s to $s^{\prime }$ due to action a.

It is assumed that the MDP $\mathcal{M}$ starts from a set of initial states $I\subseteq \mathcal{S}$ and the environment is fully observed to the agent.

The behaviour of the agent is determined by a policy π, which maps system states to a probability distribution over the actions. This paper considers deterministic policies, so the policy $\pi :\mathcal{S}\to \mathcal{O}$ maps a state to a deterministic action. At each time step t, the agent receives an observation of state $s_t$, chooses and then performs action $a_t=\pi (s_t)$. The agent transits to the next state $s_{t+1}$ and the environment returns the reward $r_t=r(s_t,a_t)$ about this transition. The goal of the system is to learn a policy π for the agent that maximises the expected long-term reward $\mathcal{J}(t)$, which is defined as follows: (3) $\mathcal{J}(t)={\mathbb{E}}_{\pi }[\sum _{i=0}^t{\kappa }^{i}r(s_i,a_i)],a_i=\pi (s_i),$(3) where $\mathcal{J}(t)$ is the accumulative discounted reward from time step 0 to t, and $\kappa \in (0,1]$ denotes the discount factor.

The proposed safe reinforcement learning method in this paper is model-based. That is, we know the accurate dynamics and constraints of the system. In addition, to enable reinforcement learning to be used to learn control policies on continuous-time dynamical systems, we divide the time steps into small pieces by discrete sampling and approximate the behaviours of continuous-time systems.

2.4. Goal-reaching and safety properties

This paper considers two properties of the learned policy: goal-reaching and safety. Goal-reaching property requires that the learned policy can control the agent to obtain the expected long-term reward, while safety property requires that the agent must not run into unsafe states.

Definition 2.1

Goal-reaching

For the initial state $s_0\in I$, goal-reaching property requires learning a policy π to control the agent to obtain the accumulative reward $\mathcal{J}(t)$ not less than the given reward threshold ${\mathcal{J}}_{min}$ in some time step t: (4) $\mathrm{\forall }{s}_0\in I,\mathrm{\exists }t\ge 0,\mathcal{J}(t)\ge {\mathcal{J}}_{min}.$(4)

Definition 2.2

Safety

For the given unsafe states U, when the agent starts from the initial states I, safety property requires learning a policy π to control the agent not to enter U in any time step t: (5) $\mathrm{\forall }{s}_0\in I,\mathrm{\forall }t\ge 0,s_t\notin U.$(5)

2.5. Barrier certificate

Before introducing barrier certificates, we introduce the Lie derivative first. Given a continuously differentiable function $k:{\mathbb{R}}^n\to \mathbb{R}$, the Lie derivative of $k(s)$ with respect to vector field $f(s,a)$ is defined as the inner product of $\mathrm{\nabla }k$ and f: (6) ${\mathcal{L}}_{f(s,a)}k(s)=(\mathrm{\nabla }k)\cdot f(s,a)=\sum _{i=1}^n\frac{\mathrm{\partial }k}{\mathrm{\partial }{s}^i}(s)\cdot f^i(s,a),$(6) where $s^i$ and $f^i(s,a)$ denote the ith elements of $s$ and $f(s,a)$, respectively.

A barrier certificate is a continuously differentiable function of system states, preventing system trajectories from passing it and invading the unsafe states. A continuously differentiable function becomes a barrier certificate of a dynamical system if it satisfies the following conditions (Prajna & Jadbabaie, 2004):

Theorem 2.3

Barrier certificate conditions

Given a dynamical system $\mathcal{H}:⟨s,\mathrm{\Psi },I,f,g⟩$ with unsafe states U, the following conditions guarantee that the function $\mathcal{B}$ is a barrier certificate: (7) $\{\begin{array}{ll}\mathcal{B}(s)>0& \mathrm{\forall }s\in U,\\ \mathcal{B}(s)\le 0& \mathrm{\forall }s\in I,\\ {\mathcal{L}}_{f(s,a)}\mathcal{B}(s)\le 0& \mathrm{\forall }\mathcal{B}(s)=0.\end{array}$(7)

In Theorem 2.3, the first and second conditions require $\mathcal{B}(s)=0$ to separate unsafe states and initial states with positive and nonpositive values, respectively. The third condition guarantees that $\mathcal{B}(s)$ cannot become positive from a nonpositive state when the system evolves. If all three conditions are satisfied, $\mathcal{B}$ is a barrier certificate of $\mathcal{H}$, and the safety of $\mathcal{H}$ is certified.

3. Learner: training policies with goal-reaching and safety properties

Given a dynamical system $\mathcal{H}$, our approach learns a safe policy π with goal-reaching and safety properties to control the system. The framework consists of two interactive parts: Learner and Verifier. The former trains the policy on training datasets, while the latter validates whether the trained policy satisfies the two properties on the whole system.

This section introduces how Learner works. To learn safe policy π, the key idea of Learner is to simultaneously train three neural networks based on the two training datasets. Figure 3 shows the workflow of Learner. In Learner, actor $\mathcal{A}$ represents the policy π to be learned. Critic $\mathcal{C}$ guides the policy to meet goal-reaching property. Barrier $\mathcal{B}$ guarantees the policy to satisfy safety property. The following subsections introduce how to define neural network structures, generate training datasets and construct loss functions to train three networks. Finally, the algorithm of Learner is presented.

Figure 3. Workflow of Learner.

3.1. Defining neural network structures

The structures of actor $\mathcal{A}$, barrier $\mathcal{B}$ and critic $\mathcal{C}$ are predefined and not changed during the training process. Actor $\mathcal{A}$ receives the current state $s_t$ and outputs the action $a_t=\mathcal{A}(s_t)$ to control the agent. For dynamical system $\mathcal{H}$, the value of state $s_t$ is that of system state x. Therefore, the number of neurons in the input layer is the same as the dimension of system variables. The number of neurons in the output layer is the same as the dimension of action $a_t$. The hidden layers can contain an arbitrary number of layers and neurons.

Barrier $\mathcal{B}$ receives system state $s$ and outputs value $\mathcal{B}(s)$. Therefore, the neuron number of the input layer is the same as the system variable number, and the output layer contains one neuron. The number of hidden layers and neurons has no limitation.

Critic $\mathcal{C}$ receives the current state $s_t$ and the action $a_t$ to output evaluation $q_t=\mathcal{C}(s_t,a_t)$ to quantify the chosen action $a_t=\mathcal{A}(s_t)$. Therefore, the neuron number of the input layer is the same as the sum dimensions of state $s_t$ and action $a_t$. The output layer contains one neuron. Also, there is no limitation on hidden layers and neurons.

3.2. Generating training datasets

3.2.1. Sampling data for experience replay buffer $D_1$

Experience replay buffer $D_1$ is used to train actor $\mathcal{A}$ and critic $\mathcal{C}$ to satisfy goal-reaching property. The data in experience replay buffer $D_1$ are in the form called a transition: $(s_t,a_t,s_{t+1},r_t)$. Before starting network training, actor $\mathcal{A}$ is randomly initialised, and noise μ is added to action $a_t$, i.e. $a_t=\mathcal{A}(s_t)+{\mu }_t$. By choosing a time bound T and time interval ${\delta }_t$ between two time steps, a sequence of transitions is sampled: $(s_0,a_0,s_1,r_0),(s_1,a_1,s_2,r_1),\dots ,(s_{n-1},a_{n-1},s_n,r_{n-1}),$where $s_0\in I\wedge t_0=0\wedge t_i-t_{i-1}={\delta }_t\wedge t_n\le T.$During network training, the agent continues to explore the environment and produce new transitions, which are added to $D_1$ to replace old ones.

3.2.2. Sampling data for state point dataset $D_2$

State point dataset $D_2$ is used to train barrier $\mathcal{B}$ to be a real barrier certificate for the system controlled by actor $\mathcal{A}$. According to Theorem 2.3, if barrier $\mathcal{B}$ satisfies the barrier certificate conditions, safety property is guaranteed.

To satisfy the first barrier certificate condition, we randomly sample data points $s_U$ from unsafe states U and construct the dataset $D_{21}=\{s_U\in U\}$. When training barrier $\mathcal{B}$ with data points in $D_{21}$, the expected outputs should be positive, i.e. $\mathcal{B}(s_U)>0$. Similarly, to satisfy the second condition, $D_{22}=\{s_I\in I\}$ contains the data points sampled from initial states I. The expected outputs of barrier $\mathcal{B}$ on $D_{22}$ should be nonpositive. To satisfy the third condition, we need to sample data points $D_{23}=\{s|\mathcal{B}(s)=0\}$. However, during network training, the parameters of barrier $\mathcal{B}$ continue to update, so the data points belonging to $D_{23}$ are constantly changing. In addition, the constraint $\mathcal{B}(s)=0$ is too strict to be satisfied due to the errors in floating-point computation. Instead, the data points are sampled from system space Ψ and tested at run-time to pick suitable points. Let ${\eta }_1>0$ and ${\eta }_2>0$ be small positive numbers, $D_{23}$ is relaxed as $\{s_{\mathrm{\Psi }}\in \mathrm{\Psi }|-{\eta }_1\le \mathcal{B}(s_{\mathrm{\Psi }})\le {\eta }_2\}$.

The state point dataset $D_2$ is composed of the above three parts: $D_2=\{D_{21},D_{22},D_{23}\}$.

3.3. Constructing loss functions

3.3.1. Constructing loss functions for goal-reaching property

The optimisation for goal-reaching property involves actor $\mathcal{A}$ and critic $\mathcal{C}$. Actor $\mathcal{A}$ chooses the action $a_t=\mathcal{A}(s_t)$, and critic $\mathcal{C}$ evaluates how much rewards the agent will obtain after this transition by $q_t=\mathcal{C}(s_t,a_t)$. The goal of training for actor $\mathcal{A}$ is to make the selected action $a_t$ obtain higher estimation $q_t$. For critic $\mathcal{C}$, the goal is to make its evaluation $q_t$ more accurate.

This paper adopts the temporal difference (TD) algorithm (Sutton et al., 2008) to update critic $\mathcal{C}$. As $q_t=\mathcal{C}(s_t,a_t)$ is the estimation of future reward at time step t, it is considered that $q_t$ is not as accurate as the TD target $y_t$ computed as follows: (8) $y_t=r_t+\kappa \cdot q_{t+1},q_{t+1}=\mathcal{C}(s_{t+1},\mathcal{A}(s_{t+1})),$(8) where $\kappa$ denotes the discount factor. The updating of critic $\mathcal{C}$ is to reduce the difference between the estimation $q_t$ and TD target $y_t$. Let ${\theta }^{\mathcal{C}}$ denote the parameters of critic $\mathcal{C}$, critic $\mathcal{C}$ is trained by minimising the following loss function $L_1$: (9) $L_1({\theta }^{\mathcal{C}})={\mathbb{E}}_{(s_t,a_t,s_{t+1},r_t)\sim D_1}[|\mathcal{C}(s_t,a_t)-(r_t+\kappa \cdot \mathcal{C}(s_{t+1},\mathcal{A}(s_{t+1})))|].$(9) To update actor $\mathcal{A}$, the policy gradient technique (Silver et al., 2014) is used. The goal of actor $\mathcal{A}$ is to make $q_t=\mathcal{C}(s_t,a_t)$ higher. Let ${\theta }^{\mathcal{A}}$ denote the parameters of actor $\mathcal{A}$; its gradient is computed as follows by applying the chain rule (10) $\begin{array}{rl}\frac{\mathrm{\partial }{q}_t}{\mathrm{\partial }{\theta }^{\mathcal{A}}}& =\frac{\mathrm{\partial }{q}_t}{\mathrm{\partial }{a}_t}\cdot \frac{\mathrm{\partial }{a}_t}{\mathrm{\partial }{\theta }^{\mathcal{A}}},\\ {\mathrm{\nabla }}_{{\theta }^{\mathcal{A}}}{q}_t& ={\mathbb{E}}_{(s_t,a_t,s_{t+1},r_t)\sim D_1}[{\mathrm{\nabla }}_{a_t}\mathcal{C}(s_t,a_t){\mathrm{\nabla }}_{{\theta }^{\mathcal{A}}}\mathcal{A}(s_t)].\end{array}$(10) Then, let $\iota >0$ be the step length of gradient ascent, and ${\theta }^{\mathcal{A}}$ is updated as follows: (11) ${\theta }^{\mathcal{A}}={\theta }^{\mathcal{A}}+\iota \cdot {\mathrm{\nabla }}_{{\theta }^{\mathcal{A}}}{q}_t.$(11)

3.3.2. Constructing loss functions for safety property

Then we consider safety property of actor $\mathcal{A}$, which is guaranteed by the simultaneously trained barrier $\mathcal{B}$. The goal is to train barrier $\mathcal{B}$ as a real barrier certificate, satisfying the barrier certificate conditions in Theorem 2.3. Therefore, the expected outputs for three parts in state point dataset $D_2$ are characterised as follows: (12) $\{\begin{array}{ll}\mathcal{B}(s_U)>0& \mathrm{\forall }{s}_U\in D_{21},\\ \mathcal{B}(s_I)\le 0& \mathrm{\forall }{s}_I\in D_{22},\\ {\mathcal{L}}_{f(s_{\mathrm{\Psi }},\mathcal{A}(s_{\mathrm{\Psi }}))}\mathcal{B}(s_{\mathrm{\Psi }})\le 0& \mathrm{\forall }{s}_{\mathrm{\Psi }}\in D_{23}.\end{array}$(12) Then, let $ϵ>0$ be a small positive number, and the following sub-loss functions are designed to meet the constraints in Equation (12(12) $\{\begin{array}{ll}\mathcal{B}(s_U)>0& \mathrm{\forall }{s}_U\in D_{21},\\ \mathcal{B}(s_I)\le 0& \mathrm{\forall }{s}_I\in D_{22},\\ {\mathcal{L}}_{f(s_{\mathrm{\Psi }},\mathcal{A}(s_{\mathrm{\Psi }}))}\mathcal{B}(s_{\mathrm{\Psi }})\le 0& \mathrm{\forall }{s}_{\mathrm{\Psi }}\in D_{23}.\end{array}$(12) ): (13) $\{\begin{array}{l}{l}_1={\mathbb{E}}_{s_U\sim D_{21}}[-min(\mathcal{B}(s_U)-ϵ,0)],\\ l_2={\mathbb{E}}_{s_I\sim D_{22}}[max(\mathcal{B}(s_I),0)],\\ l_3={\mathbb{E}}_{s_{\mathrm{\Psi }}\sim D_{23}}[max({\mathcal{L}}_{f(s_{\mathrm{\Psi }},\mathcal{A}(s_{\mathrm{\Psi }}))}\mathcal{B}(s_{\mathrm{\Psi }}),0)].\end{array}$(13) Let $\alpha >0,\beta >0,\gamma >0$ denote the coefficients among $l_1,l_2,l_3$, and ${\theta }^{\mathcal{A}},{\theta }^{\mathcal{B}}$ denote the parameters of $\mathcal{A},\mathcal{B}$, and the network training is processed by minimising the following loss function $L_2$: (14) $L_2({\theta }^{\mathcal{A}},{\theta }^{\mathcal{B}})={\mathbb{E}}_{s\sim D_2}[\alpha \cdot l_1+\beta \cdot l_2+\gamma \cdot l_3].$(14) Note that the Lie derivative ${\mathcal{L}}_{f(s_{\mathrm{\Psi }},\mathcal{A}(s_{\mathrm{\Psi }}))}\mathcal{B}(s_{\mathrm{\Psi }})$ involves actor $\mathcal{A}$ and barrier $\mathcal{B}$, so the optimisation of $L_2$ is over ${\theta }^{\mathcal{A}}$ and ${\theta }^{\mathcal{B}}$. If $L_2$ is minimised to 0, barrier $\mathcal{B}$ is a barrier certificate on $D_2$, and actor $\mathcal{A}$ satisfies safety property.

3.4. Algorithm of Learner

The algorithm of Learner is presented in Algorithm 1. Learner trains a policy π with goal-reaching and safety properties. Before training the policy, networks $\mathcal{A}$, $\mathcal{B}$, $\mathcal{C}$ and datasets $D_1$, $D_2$ are initialised. In each episode, the agent explores the environment from a random initial state $s_0$ with the noise μ. For each step, it performs action $a_t$ based on the current state $s_t$ and noise ${\mu }_t$, then steps into next state $s_{t+1}$ and obtains reward $r_t$. The transitions are stored in $D_1$. Then Learner updates the networks $\mathcal{A}$, $\mathcal{B}$ and $\mathcal{C}$ according to Equations (11(11) ${\theta }^{\mathcal{A}}={\theta }^{\mathcal{A}}+\iota \cdot {\mathrm{\nabla }}_{{\theta }^{\mathcal{A}}}{q}_t.$(11) ), (14(14) $L_2({\theta }^{\mathcal{A}},{\theta }^{\mathcal{B}})={\mathbb{E}}_{s\sim D_2}[\alpha \cdot l_1+\beta \cdot l_2+\gamma \cdot l_3].$(14) ) and (9(9) $L_1({\theta }^{\mathcal{C}})={\mathbb{E}}_{(s_t,a_t,s_{t+1},r_t)\sim D_1}[|\mathcal{C}(s_t,a_t)-(r_t+\kappa \cdot \mathcal{C}(s_{t+1},\mathcal{A}(s_{t+1})))|].$(9) ).

Algorithm 1 terminates when reaching the maximum episode or learning a policy with goal-reaching and safety properties on training datasets. During network training, if the average reward of 100 consecutive episodes is greater than the threshold, the learned policy is considered stable, satisfying goal-reaching property. If the loss $L_2({\theta }^{\mathcal{A}},{\theta }^{\mathcal{B}})$ in Equation (14(14) $L_2({\theta }^{\mathcal{A}},{\theta }^{\mathcal{B}})={\mathbb{E}}_{s\sim D_2}[\alpha \cdot l_1+\beta \cdot l_2+\gamma \cdot l_3].$(14) ) is 0 for 10 consecutive episodes, the learned policy is considered to satisfy safety property. When goal-reaching and safety properties are both satisfied, Algorithm 1 terminates early and returns $\mathcal{A}$, $\mathcal{B}$ and $\mathcal{C}$. Since $\mathcal{A}$ is trained on training datasets, goal-reaching and safety properties may not be retained on the whole system $\mathcal{H}$. The following section introduces how to validate whether actor $\mathcal{A}$ satisfies the two properties on the whole system.

4. Verifier: validating safe policies using simulations and verification

This section validates whether the learned policy, i.e. actor $\mathcal{A}$, satisfies goal-reaching and safety properties on the whole system using large-scale simulations and formal verification before presenting the algorithm of Verifier.

4.1. Validating goal-reaching property using large-scale simulations

This work carries out large-scale simulations to ensure that actor $\mathcal{A}$ satisfies goal-reaching property (Wang et al., 2019). The basic idea is to determine whether the agent can obtain the expected long-term reward by repeatedly simulating. The simulation steps are presented in Algorithm 2.

Algorithm 2 returns failure experience dataset $D_f$. If $D_f$ is empty, actor $\mathcal{A}$ is considered to satisfy goal-reaching property. Otherwise, actor $\mathcal{A}$ does not meet goal-reaching property at some initial states. In this situation, Verifier returns $D_f$ to the experience replay buffer $D_1$ in Learner to retrain actor $\mathcal{A}$.

4.2. Validating safety property using formal verification

If actor $\mathcal{A}$ is validated to satisfy goal-reaching property, the next step is to check whether it meets safety property. As introduced in Section 2.5, for a dynamical system, if there is a barrier certificate satisfying the three conditions in Theorem 2.3, the system is safe. In the last section, Learner trains a barrier $\mathcal{B}$ as the barrier certificate of the system controlled by actor $\mathcal{A}$. This subsection checks whether $\mathcal{B}$ is a real barrier certificate on the whole system.

If $\mathcal{B}$ satisfies the barrier certificate conditions in Theorem 2.3, it is a real barrier certificate and guarantees safety property of $\mathcal{A}$. In our previous work (Zhao et al., 2022), we propose an optimisation problem solving-based method to verify safety property. The key idea is to transform the verification of barrier certificate conditions into corresponding optimisation problems to perform validation. The following briefly introduces the method. For more details, please refer to our former paper.

4.2.1. Validating the first barrier certificate condition

We first consider the first barrier certificate condition $\mathcal{B}(s)>0\mathrm{\forall }s\in U$ . Assume barrier $\mathcal{B}$ is a n + 1 layer (from the 0-th layer to the n-th layer) neural network. For any state $s_0\in U$ as the network input $x_0$, i.e. $x_0=s_0$, if the output layer neuron value $x_n>0$, the first barrier certificate condition is verified to be satisfied. Based on Equation (1(1) $\{\begin{array}{ll}{z}_k=w_k{x}_{k-1}+b_k,& k=1,\dots ,n-1,\\ x_k=\varphi (z_k),& k=1,\dots ,n-1,\\ x_n=w_n{x}_{n-1}+b_n.& \end{array}$(1) ), the verification of the first barrier certificate condition is transformed into an optimisation problem about the minimum value of the barrier output layer neuron on the unsafe states, which is formalised as follows: (15) $\{\begin{array}{lll}\underset{x_0}{\mathrm{minimise}}& x_n& \\ \mathrm{s}.\mathrm{t}.& x_0\in U,& \\ & x_n=w_n{x}_{n-1}+b_n,& \\ & x_k=\varphi (z_k),& k=1,\dots ,n-1,\\ & z_k=w_k{x}_{k-1}+b_k,& k=1,\dots ,n-1.\end{array}$(15) It is observed that if the global minimum of Problem (15(15) $\{\begin{array}{lll}\underset{x_0}{\mathrm{minimise}}& x_n& \\ \mathrm{s}.\mathrm{t}.& x_0\in U,& \\ & x_n=w_n{x}_{n-1}+b_n,& \\ & x_k=\varphi (z_k),& k=1,\dots ,n-1,\\ & z_k=w_k{x}_{k-1}+b_k,& k=1,\dots ,n-1.\end{array}$(15) ) is > 0, $\mathcal{B}$ satisfies the first barrier certificate condition. To solve Problem (15(15) $\{\begin{array}{lll}\underset{x_0}{\mathrm{minimise}}& x_n& \\ \mathrm{s}.\mathrm{t}.& x_0\in U,& \\ & x_n=w_n{x}_{n-1}+b_n,& \\ & x_k=\varphi (z_k),& k=1,\dots ,n-1,\\ & z_k=w_k{x}_{k-1}+b_k,& k=1,\dots ,n-1.\end{array}$(15) ), we utilise the optimiser Gurobi 9.5 (Gurobi Optimization, 2022) to find the global optimum. However, it is difficult to find the global optimum exactly due to the nonlinearity, nonconvexity and floating-point error. The following introduces how to get a formally guaranteed solution based on the current optimum returned by the optimiser.

4.2.2. Getting formally guaranteed solutions

When optimising Problem (15(15) $\{\begin{array}{lll}\underset{x_0}{\mathrm{minimise}}& x_n& \\ \mathrm{s}.\mathrm{t}.& x_0\in U,& \\ & x_n=w_n{x}_{n-1}+b_n,& \\ & x_k=\varphi (z_k),& k=1,\dots ,n-1,\\ & z_k=w_k{x}_{k-1}+b_k,& k=1,\dots ,n-1.\end{array}$(15) ), the basic idea to handle the nonlinearity is using the piece-wise linear approximation to transform nonlinear constraints into piece-wise linear ones. However, the transformed problem may be nonconvex. Since the transformed problem is composed of piece-wise linear constraints, it can be split into a group of sub-problems that are convex. (Note that the linear approximation and splits are done by the optimiser automatically.) To bound the error about linear approximation and floating-point computation, the optimiser in real-time returns a current optimum p and an error bound ξ, which measures the maximum relative error between the current optimum p and the real global optimum $p^{\ast }$, satisfying: (16) $\xi \ge \frac{|p-p^{\ast }|}{|p|}.$(16) For Equation (16(16) $\xi \ge \frac{|p-p^{\ast }|}{|p|}.$(16) ), assuming $p\ne 0$, there are $\xi |p|\ge |p-p^{\ast }|\Rightarrow {\xi }^2{p}^2\ge p^2+(p^{\ast }{)}^2-2p{p}^{\ast }\Rightarrow 2p{p}^{\ast }\ge (1-{\xi }^2)p^2+(p^{\ast }{)}^2\ge 0.$ It can be found if $\xi <1\wedge p\ne 0$, $p{p}^{\ast }>0$, which means the sign of $p^{\ast }$ can be inferred based on p and ξ.

Theorem 4.1

When optimising Problem (15(15) $\{\begin{array}{lll}\underset{x_0}{\mathrm{minimise}}& x_n& \\ \mathrm{s}.\mathrm{t}.& x_0\in U,& \\ & x_n=w_n{x}_{n-1}+b_n,& \\ & x_k=\varphi (z_k),& k=1,\dots ,n-1,\\ & z_k=w_k{x}_{k-1}+b_k,& k=1,\dots ,n-1.\end{array}$(15) ), let p be a current optimum, $p^{\ast }$ be the global optimum, ξ be the error bound, if $p>0\wedge \xi <1$, $p^{\ast }>0$. Then, barrier $\mathcal{B}$ is proven to satisfy the first barrier certificate condition.

4.2.3. Validating the second barrier certificate condition

The verification of the second barrier certificate condition is isomorphic with the first one, except for the region of $x_0$ and the optimisation direction. We transform it into a problem optimising for the maximum of $\mathcal{B}(x_0)$ on initial states I, which is defined as follows: (17) $\{\begin{array}{lll}\underset{x_0}{\mathrm{maximise}}& x_n& \\ \mathrm{s}.\mathrm{t}.& x_0\in I,& \\ & x_n=w_n{x}_{n-1}+b_n,& \\ & x_k=\varphi (z_k),& k=1,\dots ,n-1,\\ & z_k=w_k{x}_{k-1}+b_k,& k=1,\dots ,n-1.\end{array}$(17)

Theorem 4.2

When optimising Problem (17(17) $\{\begin{array}{lll}\underset{x_0}{\mathrm{maximise}}& x_n& \\ \mathrm{s}.\mathrm{t}.& x_0\in I,& \\ & x_n=w_n{x}_{n-1}+b_n,& \\ & x_k=\varphi (z_k),& k=1,\dots ,n-1,\\ & z_k=w_k{x}_{k-1}+b_k,& k=1,\dots ,n-1.\end{array}$(17) ), let p be a current optimum, $p^{\ast }$ be the global optimum, ξ be the error bound, if $p<0\wedge \xi <1$, $p^{\ast }<0$. Then, barrier $\mathcal{B}$ is proven to satisfy the second barrier certificate condition.

4.2.4. Validating the third barrier certificate condition

The third barrier certificate condition requires that once a system trajectory reaches the zero level set of barrier $\mathcal{B}$, i.e. $\mathcal{B}(x)=0$, it travels along or is rebounded from the curve. The requirement involves the constraint that the Lie derivatives of those states are $\le 0$. By transforming the Lie derivative as the inner product form in Equation (6(6) ${\mathcal{L}}_{f(s,a)}k(s)=(\mathrm{\nabla }k)\cdot f(s,a)=\sum _{i=1}^n\frac{\mathrm{\partial }k}{\mathrm{\partial }{s}^i}(s)\cdot f^i(s,a),$(6) ) and denoting the layered representations of the two neural networks $\mathcal{A}(x)$ and $\mathcal{B}(x)$, the optimisation problem corresponding to the third barrier certificate condition is formalised as follows: (18) $\{\begin{array}{lll}\underset{x_0}{\mathrm{maximise}}& t& \\ \mathrm{s}.\mathrm{t}.& x_0\in \mathrm{\Psi },& \\ & t={\displaystyle \frac{\mathrm{\partial }\mathcal{B}(x_0)}{\mathrm{\partial }{x}_0}\cdot f(x_0,y_m),}& \\ & w_n{x}_{n-1}+b_n=0,& \\ & x_k=\varphi (w_k{x}_{k-1}+b_k),& k=1,\dots ,n-1,\\ & y_m=p_m{y}_{m-1}+q_m,& \\ & y_k=\psi (p_k{y}_{k-1}+q_k),& k=2,\dots ,m-1,\\ & y_1=\psi (p_1{x}_0+q_1).\end{array}$(18) In Problem (18(18) $\{\begin{array}{lll}\underset{x_0}{\mathrm{maximise}}& t& \\ \mathrm{s}.\mathrm{t}.& x_0\in \mathrm{\Psi },& \\ & t={\displaystyle \frac{\mathrm{\partial }\mathcal{B}(x_0)}{\mathrm{\partial }{x}_0}\cdot f(x_0,y_m),}& \\ & w_n{x}_{n-1}+b_n=0,& \\ & x_k=\varphi (w_k{x}_{k-1}+b_k),& k=1,\dots ,n-1,\\ & y_m=p_m{y}_{m-1}+q_m,& \\ & y_k=\psi (p_k{y}_{k-1}+q_k),& k=2,\dots ,m-1,\\ & y_1=\psi (p_1{x}_0+q_1).\end{array}$(18) ), t is an intermediate variable denoting the Lie derivative. $w_k$ and $b_k$ are the weight matrix and the bias vector of barrier $\mathcal{B}$, respectively. Actor $\mathcal{A}$ is assumed to be a m + 1 layer (from the 0-th layer to the m-th layer) neural network. $y_k$ denotes the layer output of actor $\mathcal{A}$. $p_k$ and $q_k$ are the weight matrix and the bias vector of actor $\mathcal{A}$, respectively. $\varphi (x)$ and $\psi (x)$ are activation functions of barrier $\mathcal{B}$ and actor $\mathcal{A}$, respectively. If the maximum of Problem (18(18) $\{\begin{array}{lll}\underset{x_0}{\mathrm{maximise}}& t& \\ \mathrm{s}.\mathrm{t}.& x_0\in \mathrm{\Psi },& \\ & t={\displaystyle \frac{\mathrm{\partial }\mathcal{B}(x_0)}{\mathrm{\partial }{x}_0}\cdot f(x_0,y_m),}& \\ & w_n{x}_{n-1}+b_n=0,& \\ & x_k=\varphi (w_k{x}_{k-1}+b_k),& k=1,\dots ,n-1,\\ & y_m=p_m{y}_{m-1}+q_m,& \\ & y_k=\psi (p_k{y}_{k-1}+q_k),& k=2,\dots ,m-1,\\ & y_1=\psi (p_1{x}_0+q_1).\end{array}$(18) ) is $<0$, the third barrier certificate condition is verified to be satisfied.

Then we consider the encoding of $\mathrm{\partial }\mathcal{B}(x_0)/\mathrm{\partial }{x}_0$ . Based on Equation (1(1) $\{\begin{array}{ll}{z}_k=w_k{x}_{k-1}+b_k,& k=1,\dots ,n-1,\\ x_k=\varphi (z_k),& k=1,\dots ,n-1,\\ x_n=w_n{x}_{n-1}+b_n.& \end{array}$(1) ) and the fact that $x_n=\mathcal{B}(x_0)$, $\mathrm{\partial }\mathcal{B}(x_0)/\mathrm{\partial }{x}_0$ is computed as (19) $\frac{\mathrm{\partial }\mathcal{B}(x_0)}{\mathrm{\partial }{x}_0}=\frac{\mathrm{\partial }{x}_n}{\mathrm{\partial }{x}_0}=w_n\cdot {\varphi }^{\prime }(z_{n-1})\times w_{n-1}\cdots w_2\cdot {\varphi }^{\prime }(z_1)\times w_1.$(19)

Theorem 4.3

When optimising Problem (18(18) $\{\begin{array}{lll}\underset{x_0}{\mathrm{maximise}}& t& \\ \mathrm{s}.\mathrm{t}.& x_0\in \mathrm{\Psi },& \\ & t={\displaystyle \frac{\mathrm{\partial }\mathcal{B}(x_0)}{\mathrm{\partial }{x}_0}\cdot f(x_0,y_m),}& \\ & w_n{x}_{n-1}+b_n=0,& \\ & x_k=\varphi (w_k{x}_{k-1}+b_k),& k=1,\dots ,n-1,\\ & y_m=p_m{y}_{m-1}+q_m,& \\ & y_k=\psi (p_k{y}_{k-1}+q_k),& k=2,\dots ,m-1,\\ & y_1=\psi (p_1{x}_0+q_1).\end{array}$(18) ), let p be a current optimum, $p^{\ast }$ be the global optimum, ξ be the error bound, if $p<0\wedge \xi <1$, $p^{\ast }<0$. Then, barrier $\mathcal{B}$ is proven to satisfy the third barrier certificate condition.

When solving Problems (15(15) $\{\begin{array}{lll}\underset{x_0}{\mathrm{minimise}}& x_n& \\ \mathrm{s}.\mathrm{t}.& x_0\in U,& \\ & x_n=w_n{x}_{n-1}+b_n,& \\ & x_k=\varphi (z_k),& k=1,\dots ,n-1,\\ & z_k=w_k{x}_{k-1}+b_k,& k=1,\dots ,n-1.\end{array}$(15) ), (17(17) $\{\begin{array}{lll}\underset{x_0}{\mathrm{maximise}}& x_n& \\ \mathrm{s}.\mathrm{t}.& x_0\in I,& \\ & x_n=w_n{x}_{n-1}+b_n,& \\ & x_k=\varphi (z_k),& k=1,\dots ,n-1,\\ & z_k=w_k{x}_{k-1}+b_k,& k=1,\dots ,n-1.\end{array}$(17) ) or (18(18) $\{\begin{array}{lll}\underset{x_0}{\mathrm{maximise}}& t& \\ \mathrm{s}.\mathrm{t}.& x_0\in \mathrm{\Psi },& \\ & t={\displaystyle \frac{\mathrm{\partial }\mathcal{B}(x_0)}{\mathrm{\partial }{x}_0}\cdot f(x_0,y_m),}& \\ & w_n{x}_{n-1}+b_n=0,& \\ & x_k=\varphi (w_k{x}_{k-1}+b_k),& k=1,\dots ,n-1,\\ & y_m=p_m{y}_{m-1}+q_m,& \\ & y_k=\psi (p_k{y}_{k-1}+q_k),& k=2,\dots ,m-1,\\ & y_1=\psi (p_1{x}_0+q_1).\end{array}$(18) ), if the optimiser gets a current optimum p with an unexpected sign and the error bound $\xi <1$, e.g. $p<0\wedge \xi <1$ for Problem (15(15) $\{\begin{array}{lll}\underset{x_0}{\mathrm{minimise}}& x_n& \\ \mathrm{s}.\mathrm{t}.& x_0\in U,& \\ & x_n=w_n{x}_{n-1}+b_n,& \\ & x_k=\varphi (z_k),& k=1,\dots ,n-1,\\ & z_k=w_k{x}_{k-1}+b_k,& k=1,\dots ,n-1.\end{array}$(15) ), the optimisation variable configuration of p corresponds to a counterexample. In this situation, $\mathcal{B}$ is not a real barrier certificate, and safety property of $\mathcal{A}$ is not guaranteed. Then Verifier returns the counterexample to the state point dataset $D_2$ in Learner to retrain actor $\mathcal{A}$.

4.3. Algorithm of Verifier

The algorithm of Verifier is presented in Algorithm 3. Verifier validates whether learned actor $\mathcal{A}$ satisfies goal-reaching and safety properties on the whole dynamical system. To check goal-reaching property, Verifier repeatedly performs simulations. For safety property, Verifier constructs three optimisation problems and verifies them. If the simulations and verification both succeed, $\mathcal{A}$ is a safe policy satisfying goal-reaching and safety properties. Otherwise, Verifier exits and returns the failure experience or counterexamples to Learner to retrain actor $\mathcal{A}$.

5. Implementation and experiments

This section first introduces the implementation of our safe policy learning tool SRLBC. Then we demonstrate the application of SRLBC by treating three control tasks selected from the OpenAI gym environment (Brockman et al., 2016) and compare it with the baseline method DDPG (Lillicrap et al., 2016).

5.1. Implementation

Algorithm 4 presents our Safe Reinforcement Learning method using Barrier Certificates, called SRLBC. SRLBC can be applied to any actor-critic-based reinforcement learning method to provide safety guarantees for them. This work implements SRLBC based on DDPG, which focuses on learning policies with goal-reaching property. Note that our framework is also suitable for other actor-critic-based methods such as soft actor-critic (SAC), asynchronous advantage actor-critic (A3C) and proximal policy optimization (PPO).

SRLBC combines Learner with Verifier to learn safe policies for dynamical systems. SRLBC is not complete, since it cannot guarantee to learn a safe policy before reaching the maximum iteration. On the one hand, SRLBC is sound for the verification of safety property. However, on the other hand, it cannot provide formal guarantees for the simulations of goal-reaching property.

The computational complexity of SRLBC consists of those about Learner and Verifier. Learner's complexity is approximately related to the number of training episodes, while the Verifier's complexity is related to the learned policy, i.e. Actor $\mathcal{A}$. For actors using ReLU activation functions, the complexity is exponentially related to the number of neurons in the worst case.

SRLBC is implemented on top of TensorFlow 2.0 (Abadi et al., 2016) and invokes optimiser Gurobi 9.5 (Gurobi Optimization, 2022) to solve optimisation problems on a workstation running Ubuntu 18.04 with 320 GB RAM, two 3.20 GHz Intel Xeon Gold 6146 CPUs, and three NVIDIA TITAN V GPUs. The default settings of the hyperparameters are ${\eta }_1={\eta }_2=0.05$, $ϵ=0.005$, $\alpha =\beta =\gamma =1$, $\kappa =0.95$ and $\iota =0.01$. Besides, there are some hyperparameters that vary significantly among different dynamical systems due to special characteristics, such as the time bound T, time interval ${\delta }_t$, the neural network structures, etc. These hyperparameters are set heuristically according to the specific examples.

5.2. Case studies

5.2.1. Continuous Mountain Car

Figure 4(a) shows the Continuous Mountain Car environment. The goal is to drive the car up the right mountain. The car's state $s=[p,v]$ is described by two features: position $p\in [-1.2,0.6]$ and velocity $v\in [-0.07,0.07]$. The position of the success flag is 0.45. In exploring, the maximum time is 999, and the time step for each transition is 0.01.

Figure 4. Continuous Mountain Car environment. (a) Original. (b) Safety constrained.

The evolution of the car's state is formulated as follows: $\left[\begin{array}{c}\dot{p}\\ \dot{v}\end{array}\right]=\left[\begin{array}{c}v\\ 0.0015\cdot a-0.0025\cdot \cos (3\cdot p)\end{array}\right].$This paper limits the car's trajectories with some safety constraints. As shown in Figure 4(b), we mark the position p<−1 as unsafe states. The reward for SRLBC is set as follows: $r=\{\begin{array}{ll}-100,& p<-1,\\ -0.1\cdot a^2,& -1\le p<0.45,\\ 100,& p\ge \mathrm{0.45.}\end{array}$The success threshold for the average reward of 100 consecutive explorations is 90. For DDPG, we use the default reward settings.

Figure 5(a) compares SRLBC with DDPG on goal-reaching property, which is evaluated by the average rewards of 100 consecutive episodes. SRLBC converges at 133rd episode using 114.23 s, while DDPG converges at the 108th episode using 82.19 s. After 220 episodes, SRLBC obtains the same level of reward as DDPG and remains stable.

Figure 5. Evaluation of goal-reaching and safety properties on each episode for Continuous Mountain Car environment.

Figure 5(b) displays the evaluation of safety property, which is quantified by the minimum position during the car's exploration. The safe bound is p = 1. At the beginning of training, both SRLBC and DDPG will control the car to enter unsafe states. After the 31st episode, the car controlled by SRLBC no longer enters unsafe states. However, for the car controlled by DDPG, it does not satisfy safety property and will often enter unsafe states.

5.2.2. Pendulum

Figure 6(a) shows the Pendulum swing-up problem. The goal is to learn a policy applying a torque a to the pendulum to swing it up so it stays upright. The pendulum's state $s=[\theta ,\dot{\theta }]$ is described by two features: the angle of the pendulum $\theta \in [-\pi ,\pi )$ and the angular velocity of the swing $\dot{\theta }\in [-8,8]$. In exploration, the maximum time is 200, and the time step for each transition is 0.005. This paper marks $(-(3/8_{\pi },-(5/8)\pi )$ as unsafe states and limits the initial angle $\theta \notin (-(1/4)\pi ,-(3/4)\pi )$ , as shown in Figure 6(b). The reward for this system is set as follows: $r=-({\theta }^2+0.1\cdot {\dot{\theta }}^2+0.001\cdot a^2).$The success threshold for the average reward of 100 consecutive explorations is $-500$.

Figure 6. Pendulum environment. (a) Original. (b) Safety constrained.

Figure 7 shows the performance of SRLBC compared with DDPG. As displayed in Figure 7(a), SRLBC learns a stable policy with goal-reaching property at the 153rd episode using 42.15 s, while DDPG learns the policy at the 129th episode using 37.63 s. Figure 7(b) illustrates the minimum angle of the pendulum to the centre of unsafe states $\theta =-(\pi /2)$ . The safe bound is $\pi /8\approx 0.3927$. At the 161st episode, SRLBC successfully learns a policy with safety property that controls the pendulum to stand up without entering the unsafe states on training datasets. For DDPG, the policy learned by it does not satisfy safety property.

Figure 7. Evaluation of goal-reaching and safety properties on each episode for Pendulum environment.

5.2.3. CartPole

Figure 8 shows the CartPole environment. The system consists of a cart moving along the horizontal direction and a pendulum connected with the cart. The pendulum starts upright, and the goal is to learn a policy controlling the force a applied to the cart to prevent the pendulum from falling over. The system's state $s=[x,\dot{x},\theta ,\dot{\theta }]$ is described by four features: the cart's position $x\in [-2.4,2.4]$, the moving speed of the cart $\dot{x}$, the angle of the pendulum θ and the angular velocity of the pendulum $\dot{\theta }$. In exploring, the maximum time is 200, and the time step for each transition is 0.005. If the angle of the pendulum is too large, i.e. $|\theta -\pi |>\pi /15$ , the exploration is considered failed. Besides, this paper constrains the cart's movement area $x\in [-1,1]$ and marks the remaining states as unsafe. The reward for SRLBC is set as follows: $r=\{\begin{array}{ll}1,& -1\le x\le 1,\\ -1& \mathrm{otherwise}.\end{array}$The success threshold for the average reward of 100 consecutive explorations is 195.

Figure 8. CartPole environment. (a) Original. (b) Safety constrained.

Figure 9 shows the performance of SRLBC compared with DDPG on goal-reaching and safety properties. As shown in Figure 9(a), SRLBC learns a policy to obtain the expected long-term reward at the 270th episode using 232.90 s, while DDPG learns at the 225th episode using 190.46 s. Figure 9(b) displays the maximum distance of the cart to the track centre. The safe bound of maximum distance is 1. It can be found that the policy learned by SRLBC controls the car not to cross the safe bound after the 179th episode. For the policy learned by DDPG, it does not provide safety, and the cart may enter unsafe states.

Figure 9. Evaluation of goal-reaching and safety properties on each episode for CartPole environment.

5.3. Performance evaluation

Table 1 shows the performance evaluation of SRLBC and DDPG. In Table 1, the structures of actor $\mathcal{A}$, barrier $\mathcal{B}$ and critic $\mathcal{C}$ are displayed. For DDPG, the column ‘Goal-reaching’ denotes the average episode and running time of five runs to achieve goal-reaching property, in the form of $episode(time)$. For SRLBC, the columns ‘Goal-reaching’ and ‘Safety’ denote the stage to satisfy goal-reaching and safety properties in the network training process, respectively. The column ‘Validation’ denotes the average running time when SRLBC successfully validates the learned policy.

Table 1. Experimental results.

				DDPG	SRLBC
Example	$\mathcal{A}$	$\mathcal{B}$	$\mathcal{C}$	Goal-reaching	Goal-reaching	Safety	Validation
Continuous Mountain Car	2-64-64-1	2-50-50-1	3-64-64-1	108(82.19 s)	133(114.23 s)	41(39.51 s)	120.15 s
Pendulum	2-30-1	2-20-1	3-30-1	129(37.63 s)	153(42.15 s)	171(61.43 s)	69.12 s
CartPole	4-128-64-32-16-1	4-40-30-20-1	5-128-64-32-16-1	225(190.46 s)	270(232.90 s)	189(154.16 s)	254.71 s

Observing Table 1, it can be found that SRLBC can learn actor networks with 3–6 layers. The layers of barrier networks span from 3 to 5. For goal-reaching property, the episode and running time of DDPG are smaller than those of SRLBC. This is because SRLBC simultaneously trains three networks, which affects the speed of network training. In addition, SRLBC guarantees safety property of learned actor $\mathcal{A}$, which is not considered by DDPG. The training of actor $\mathcal{A}$ to satisfy safety property also influences the convergence speed of goal-reaching property.

When SRLBC successfully learns a policy with goal-reaching and safety properties on training datasets, it calls Verifier to validate it. For Continuous Mountain Car and CartPole, SRLBC iterates once to learn safe policies. For Pendulum, it iterates four times due to the dissatisfaction of safety property. The average running time of SRLBC to learn safe policies for three cases is 147.99 s. Compared with DDPG's 103.43 s, SRLBC achieves safety with no more than 0.5× time overhead, showing the feasibility and effectiveness of our framework.

6. Related work

This work is related to the literature about safety verification and control of dynamical systems.

6.1. Safety verification of dynamical systems

Intuitively, the safety property can be directly checked by computing the exact system reachable set or its overapproximation (Akametalu et al., 2014; Clavière et al., 2020; Hu et al., 2020). To address the computational difficulty arising from neural network control policies (also called controllers), some methods construct a new system approximating the original one and then adopt its reachable set in safety verification (Huang et al., 2019; Ivanov et al., 2020; Sun et al., 2019; Xiang et al., 2020). However, the approximation of dynamical systems and control policies will bring errors. As the reachable set is computed step by step, the errors accumulate quickly.

Another type of method is to separate neural network control policies from dynamical models and analyse each of them individually, where safety verification leads to the problem of output range evaluation of neural network with respect to a given input region (Julian & Kochenderfer, 2019). Many techniques including input refinement (Katz et al., 2017), abstract interpretation (Anderson et al., 2020), interval arithmetic (Wang et al., 2018), abstract domain (Singh et al., 2019), linear approximations (Wong & Kolter, 2018) and mixed integer programming (Dutta et al., 2018b) are proposed to handle the problem.

Recently, neural networks have been adopted as barrier certificates in verifying the safety property of dynamical systems. Zhao et al. (2020) introduce networks with Bent-ReLU activation functions as barrier certificates and rely on the satisfiability modulo theories (SMT) solver iSAT3 (Winterer, 2017) to identify real barrier certificates. Peruffo et al. (2021) propose a counterexample-based, formal, and automated sequential loop to synthesise candidate barrier certificates, and use the SMT solvers dReal (Gao et al., 2013) and Z3 (De Moura & Bjørner, 2008) to certify them. The disadvantage of the above methods is that they only provide safety verification but do not participate in the construction of safe systems.

6.2. Safety control of dynamical systems

The existing methods to learn safe policies based on supervised learning have been widely studied. Dutta et al. (2018a) present an approach to learning and formally verifying feedback laws for data-driven models of neural networks. Taylor et al. (2020) develop a machine learning framework utilising control barrier functions to reduce model uncertainties. The shortcoming of these methods is that they only consider the safety property of the learned policy, but cannot achieve the goal-reaching property. Instead, Jin et al. (2020) construct an optimisation objective and minimise it to learn policies for dynamical systems. Limited to the characteristics of supervised learning, it is not as effective as the methods using reinforcement learning when learning policies to achieve the goal-reaching property.

Towards safe reinforcement learning, many model-free or model-based methods have been proposed (Yang, Ding, et al., 2020; Yang et al., 2021; Yang, Vamvoudakis, et al., 2020). Radac and Precup (2019) propose a neural network-based control scheme in an adaptive actor-critic learning framework designed for output reference model tracking. Ma et al. (2022) propose a model-based safe reinforcement learning framework to account for potential modelling errors by capturing and exploiting model uncertainty. There have been several surveys on safe reinforcement learning (Garcıa & Fernández, 2015; Gu et al., 2022; Thomas, 2015), and this paper briefly introduces the two common categories.

A line of work applies risk measure costs into the reward to design constrained policy optimisation formulation to ensure safety in expectation. Stooke et al. (2020) propose a new set of constrained reinforcement learning solutions for Lagrangian methods utilising derivatives of the constraint functions. Tamar et al. (2016) present the sampling-based algorithms for optimisation under a coherent-risk objective using two new policy gradient style formulas. Thananjeyan et al. (2021) present the recovery reinforcement learning algorithm to effectively balance task performance and constraint satisfaction when learning policies. However, since these methods specify the possible risk of unsafe behaviours through the costs, the safety property is guaranteed by probability and they cannot completely avoid safety violations.

Another line of work utilises external safety techniques to avoid unsafe behaviours, which are sufficient conditions to guarantee the safety property in the exploration process. Deshmukh et al. (2019) propose a verification-in-the-loop training algorithm to synthesise neural network controllers under the safety provided by the control barrier function. Berkenkamp et al. (2017) extend the theoretical results of the control Lyapunov function to safely optimise policies based on statistical models of the dynamics. Cheng et al. (2019) propose an end-to-end architecture for safe reinforcement learning that combines the model-free reinforcement learning-based controller, model-based controller and online learning of unknown system dynamics. Luo and Ma (2021) explore safe reinforcement learning with zero training-time safety violations for the discrete-time system based on a safe initial policy. The limitation of these methods is that the control barrier functions, control Lyapunov functions and safe backup policies usually need to be manually provided, or some prior knowledge is required. Compared with the above work, the approach proposed in this paper simultaneously learns the policy with a barrier certificate, which provides formal safety guarantees for the learned policy and does not need any prior knowledge.

7. Conclusion

This paper proposes a feedback-driven framework to learn safe policies for dynamical systems, which integrates barrier certificates into actor-critic-based reinforcement learning methods to provide safety guarantees. The learned policy satisfies goal-reaching and safety properties. The framework of the approach is composed of two interactive parts: Learner and Verifier. Learner learns a policy with goal-reaching and safety properties on training datasets, while Verifier validates the two properties on the whole system using large-scale simulations and formal verification. We implement a safe policy learning tool SRLBC based on DDPG and evaluate its performance on three control tasks. Experimental results demonstrate that SRLBC achieves safety with no more than 0.5× time overhead compared to DDPG, showing the feasibility and effectiveness of our framework.

Disclosure statement

No potential conflict of interest was reported by the author(s).

Additional information

Funding

This work is supported by the National Natural Science Foundation of China under Grants 62172211, 62172210, 62172200 and the Leading-edge Technology Program of Jiangsu Natural Science Foundation No. BK20202001.