Control barrier certificates (CBCs) are often used to certify the safety of a stochastic systems.
More...
|
| | BarrierCertificate (int T, double gamma, double eta=0, double c=0) |
| | Construct a new BarrierCertificate object.
|
| |
| double | operator() (ConstVectorRef x) const |
| | Evaluate the barrier certificate at the given point.
|
| |
| bool | is_synthesized () const |
| | Check whether the barrier certificate is synthesized.
|
| |
| double | norm () const |
| | Get read-only access to the norm describing the complexity of the barrier of the barrier certificate.
|
| |
| double | gamma () const |
| | Get read-only access to the \( \) \( \) \( \gamma \) \( \) \( \) value in the CBC definition of the barrier certificate.
|
| |
| double | eta () const |
| | Get read-only access to the \( \) \( \) \( \eta \) \( \) \( \) value in the CBC definition of the barrier certificate.
|
| |
| double | c () const |
| | Get read-only access to the \( c \) value in the CBC definition of the barrier certificate.
|
| |
| double | safety () const |
| | Get read-only access to the safety probability of the system of the barrier certificate.
|
| |
| int | T () const |
| | Get read-only access to the time horizon of the barrier certificate.
|
| |
| virtual std::unique_ptr< BarrierCertificate > | clone () const =0 |
| | Clone the barrier certificate.
|
| |
| virtual std::string | to_string () const |
| | Obtain the string representation of this object.
|
| |
Control barrier certificates (CBCs) are often used to certify the safety of a stochastic systems.
A CBC over a domain \( \texttip{\mathcal{X}}{Polish sample vector space} \subseteq \mathbb{R}^d \) with respect to an unsafe set \( \texttip{\mathcal{X}}{Usafe set}_u \) and transition function \( f: \mathcal{X} \times
\mathcal{U} \to \mathcal{X} \), where \( \mathcal{U} \subseteq \mathbb{R}^m \) is the set of control inputs, is a function \( B: \mathcal{X} \to \mathbb{R} \) with the following properties:
\[\begin{align*}
&\forall x \in \mathcal{X} && B(x) \geq 0 \\
&\forall x_0 \in \mathcal{X}_0 && B(x_0) \leq \eta \newline
&\forall x_u \in \mathcal{X}_u && B(x_u) \geq \gamma \newline
&\forall x \in \mathcal{X}, \forall u \in \mathcal{U} && \mathbb{E}[B(x_+)] - B(x) \leq c
\end{align*}
\]
for some \( \) \eta \(, \) \gamma \(, c \in \mathbb{R} \) with \( \) \gamma \( > \) \eta \( \geq 0\) and \( c \geq 0 \). In this context, \( x_+ \) is the next state of the system after applying the control input \( u \) at state \( \texttip{x}{Element of the vector space} \). If such a function exists, then the safety probability of the system can be bounded by
\[P_\text{safe} \geq 1 - \frac{\eta + c T}{\gamma}
\]
where \( T \) is the time horizon, i.e., the number of time steps to consider.
1.13.2