Automated system for generating approximate safety conditions for monitoring and verification
Described is a system and method for generating safety conditions for a cyber-physical system with state space S, action space A and trajectory data labelled as either safe or unsafe. In operation, the system receives inputs and ten minimizes loss functions to cause a neural network to become a barrier function. Based on the barrier function, the system can then determine if the cyber-physical system is entering an usafe state, such that if the cyber-physical system is entering the usafe state, then the cyber-physical system is caused to initiate a maneuver to position the cyber-physical system into a safe state.
1. A method for generating control barrier functions for ensuring safety conditions for an autonomous vehicle with state space S, action space A and trajectory data labelled as either safe or unsafe, the method comprising an act of:
causing one or more processors to execute instructions encoded on a memory such that upon execution of the instructions, the one or more processors perform operations of:
receiving inputs, the inputs being a discrete or continuous dynamics model, a set of state space data points, a neural network h θ , an initial safety function L, and a method of determining an action a at a given dynamical system state s that is optimal according to the neural network h θ ;
if a discrete dynamics model is part of the input, then minimizing a first loss function and a second loss function then proceeding, otherwise proceeding;
wherein the first loss function minimizes δ 1 ,δ 2 (L) (θ) such that h θ ≈L, and wherein the second loss function minimizes η,δ 1 ,δ 2 (H k−1 ) (θ) such that h θ (s)≈(1−γ)L(s)+
γ
min
{
L
(
s
)
,
η
❘
"\[LeftBracketingBar]"
h
θ
(
s
)
❘
"\[RightBracketingBar]"
+
max
a
∈
A
h
θ
(
τ
(
s
,
a
)
)
}
,
with L replaced by H 0 , H 1 , H 2 , . . . ,
wherein denotes a loss function, δ denotes a fixed threshold value, η represents a barrier function constant, k represents a number of iterations, γ denotes a discount factor, and τ represents a transition function;
refining the neural network h θ to become a control barrier function by minimizing η,α,δ 1 ,δ 2 (θ) such that
(
1
-
η
)
h
θ
(
x
j
)
≤
max
a
∈
A
(
τ
(
x
j
,
a
)
)
for all instantaneously safe x j ϵD such that h θ (x j )>0 and h θ (x j )≤0 for all unsafe x j ϵD, wherein D denotes a data set used to learn an approximate barrier function,
outputting the control barrier function;
determining if the autonomous vehicle is entering an unsafe state using the control barrier function; and
causing the autonomous vehicle to initiate a physical operation when the autonomous vehicle is in the unsafe state.
2. The method as set forth in claim 1 , wherein the physical operation is a maneuver to position the autonomous vehicle into a safe state.
3. The method as set forth in claim 1 , wherein minimizing the first and second loss functions includes operations of:
minimizing the first loss function that causes the neural network h θ to learn an approximation of an initial safety function;
minimizing the second loss function that causes the neural network h θ to satisfy a Bellman equation, which in turn modifies the neural network h θ , resulting in an updated approximation of the control barrier function;
performing an iteration of minimizing the second loss function to cause the neural network h θ to satisfy a Bellman equation, which in turn further modifies the neural network h θ , resulting in an updated approximation of the control barrier function; and
iterating minimization of the second loss function a predetermined number of times.
4. The method as set forth in claim 1 , wherein in minimizing the distinct loss function, the first loss function of η,α,δ 1 ,δ 2 (θ) is minimized for the discrete dynamics model and a loss function of κ,α,δ 1 ,δ 2 cts (θ) is minimized for the continuous dynamics model.
5. The method as set forth in claim 1 , wherein the discrete dynamics model is τ:S×A→S, where S denotes a state space of the dynamical system, A denotes action space, and z denotes a transition function that yields a state of the autonomous vehicle following from an inputted state-action pair.
6. The method as set forth in claim 1 , wherein the continuous dynamics model is {dot over (s)}=f (s,a), where s denotes a state of the system, and a denotes a control action being taken, and {dot over (s)} denotes a time derivative of s, and f denotes a vector field function that yields a time derivative of the state resulting from an inputted state-action pair.
7. A system for generating control barrier functions for ensuring safety conditions for an autonomous vehicle with state space S, action space A and trajectory data labelled as either safe or unsafe, the system comprising:
one or more processors and a memory, the memory being a non-transitory computer-readable medium having executable instructions encoded thereon, such that upon execution of the instructions, the one or more processors perform operations of:
receiving inputs, the inputs being a discrete or continuous dynamics model, a set of state space data points, a neural network h θ , an initial safety function L, and a method of determining an action a at a given dynamical system state s that is optimal according to the neural network h θ ;
if a discrete dynamics model is part of the input, then minimizing a first loss function and a second loss function then proceeding, otherwise proceeding;
wherein the first loss function minimizes δ 1 ,δ 2 (L) (θ) such that h θ ≈L, and wherein the second loss function minimizes η,δ 1 ,δ 2 (H k−1 ) (θ) such that h θ (s)≈(1−γ)L(s)+
γ
min
{
L
(
s
)
,
η
❘
"\[LeftBracketingBar]"
h
θ
(
s
)
❘
"\[RightBracketingBar]"
+
max
a
∈
A
h
θ
(
τ
(
s
,
a
)
)
}
,
with L replaced by H 0 , H 1 , H 2 , . . . ,
wherein denotes a loss function, δ denotes a fixed threshold value, η represents a barrier function constant, k represents a number of iterations, A denotes a set of actions, γ denotes a discount factor, and τ represents a transition function;
refining the neural network h θ to become a control barrier function by minimizing η,α,δ 1 ,δ 2 (θ) such that
(
1
-
η
)
h
θ
(
x
j
)
≤
max
a
∈
A
(
τ
(
x
j
,
a
)
)
for all instantaneously safe x j ϵD such that h θ (x j )>0 and h θ (x j )≤0 for all unsafe x j ϵD, wherein D denotes a data set used to learn an approximate barrier function,
outputting the control barrier function;
determining if the autonomous vehicle is entering an unsafe state using the control barrier function; and
causing the autonomous vehicle to initiate a physical operation when the autonomous vehicle is in the unsafe state.
8. The system as set forth in claim 7 , wherein the physical operation is a maneuver to position the autonomous vehicle into a safe state.
9. The system as set forth in claim 7 , wherein minimizing the first and second loss functions includes operations of:
minimizing the first loss function that causes the neural network h θ to learn an approximation of an initial safety function;
minimizing the second loss function that causes the neural network h θ to satisfy a Bellman equation, which in turn modifies the neural network h θ , resulting in an updated approximation of the control barrier function;
performing an iteration of minimizing the second loss function to cause the neural network h θ to satisfy a Bellman equation, which in turn further modifies the neural network h θ , resulting in an updated approximation of the control barrier function; and
iterating minimization of the second loss function a predetermined number of times.
10. The system as set forth in claim 7 , wherein in minimizing the distinct loss function, the first loss function of η,α,δ 1 ,δ 2 (θ) is minimized for the discrete dynamics model and a loss function of κ,α,δ 1 ,δ 2 (θ) is minimized for the continuous dynamics model.
11. The system as set forth in claim 7 , wherein the discrete dynamics model is τ:S×A→S, where S denotes a state space of the dynamical system, A denotes action space, and τ denotes a transition function that yields a state of the autonomous vehicle following from an inputted state-action pair.
12. The system as set forth in claim 7 , wherein the continuous dynamics model is {dot over (s)}=f(s,a), where s denotes a state of the system, and a denotes a control action being taken, and {dot over (s)} denotes a time derivative of s, and f denotes a vector field function that yields a time derivative of the state resulting from an inputted state-action pair.
13. A computer program product for generating control barrier functions for ensuring safety conditions for an autonomous vehicle with state space S, action space A and trajectory data labelled as either safe or unsafe, the computer program product comprising:
a non-transitory computer-readable medium having executable instructions encoded thereon, such that upon execution of the instructions by one or more processors, the one or more processors perform operations of:
receiving inputs, the inputs being a discrete or continuous dynamics model, a set of state space data points, a neural network h θ , an initial safety function L, and a method of determining an action a at a given dynamical system state s that is optimal according to the neural network h θ ;
if a discrete dynamics model is part of the input, then minimizing a first loss function and a second loss function then proceeding, otherwise proceeding;
wherein the first loss function minimizes δ 1 δ 2 (L) (θ) such that h θ ≈L, and wherein the second loss function minimizes η,δ 1 ,δ 2 (H k−1 ) (θ) such that h θ (s)≈(1−γ)L(s)+
γ
min
{
L
(
s
)
,
η
❘
"\[LeftBracketingBar]"
h
θ
(
s
)
❘
"\[RightBracketingBar]"
+
max
a
∈
A
h
θ
(
τ
(
s
,
a
)
)
}
,
with L replaced by H 0 , H 1 , H 2 , . . . ,
wherein denotes a loss function, δ denotes a fixed threshold value, η represents a barrier function constant, k represents a number of iterations, A denotes a set of actions, γ denotes a discount factor, and τ represents a transition function;
refining the neural network h θ to become a control barrier function by minimizing η,α,δ 1 ,δ 2 (θ) such that
(
1
-
η
)
h
θ
(
x
j
)
≤
max
a
∈
A
(
τ
(
x
j
,
a
)
)
for all instantaneously safe x j ϵD such that h θ (x j )>0 and h θ (x j )≤0 for all unsafe x j ϵD, wherein D denotes a data set used to learn an approximate barrier function,
outputting the control barrier function;
determining if the autonomous vehicle is entering an unsafe state using the control barrier function; and
causing the autonomous vehicle to initiate a physical operation when the autonomous vehicle is in the unsafe state.
14. The computer program product as set forth in claim 13 , wherein the physical operation is a maneuver to position the autonomous vehicle into a safe state.
15. The computer program product as set forth in claim 13 , wherein minimizing the first and second loss functions includes operations of:
minimizing the first loss function that causes the neural network h θ to learn an approximation of an initial safety function;
minimizing the second loss function that causes the neural network h θ to satisfy a Bellman equation, which in turn modifies the neural network h θ , resulting in an updated approximation of the control barrier function;
performing an iteration of minimizing the second loss function to cause the neural network h θ to satisfy a Bellman equation, which in turn further modifies the neural network h θ , resulting in an updated approximation of the control barrier function; and
iterating minimization of the second loss function a predetermined number of times.
16. The computer program product as set forth in claim 13 , wherein in minimizing the distinct loss function, the first loss function of η,α,δ 1 ,δ 2 (θ) is minimized for the discrete dynamics model and a loss function of κ,α,δ 1 ,δ 2 (θ) is minimized for the continuous dynamics model.
17. The computer program product as set forth in claim 13 , wherein the discrete dynamics model is τ:S×A→S, where S denotes a state space of the dynamical system, A denotes action space, and τ denotes a transition function that yields a state of the autonomous vehicle following from an inputted state-action pair.
18. The computer program product as set forth in claim 13 , wherein the continuous dynamics model is {dot over (s)}=f (s,a), where s denotes a state of the system, and a denotes a control action being taken, and {dot over (s)} denotes a time derivative of s, and f denotes a vector field function that yields a time derivative of the state resulting from an inputted state-action pair.