|
lucid
0.0.1
Lifting-based Uncertain Control Invariant Dynamics
|
|
|
lucid
0.0.1
Lifting-based Uncertain Control Invariant Dynamics
|
Barrier certificate using a Fourier basis as a template for the function. More...
#include <FourierBarrierCertificate.h>
Public Member Functions | |
| bool | synthesize (int lattice_resolution, const Estimator &estimator, const TruncatedFourierFeatureMap &feature_map, const RectSet &X_bounds, const Set &X_init, const Set &X_unsafe, const FourierBarrierCertificateParameters ¶meters={}) |
| This is an overloaded member function, provided for convenience. It differs from the above function only in what argument(s) it accepts. | |
| bool | synthesize (const Optimiser &optimiser, int lattice_resolution, const Estimator &estimator, const TruncatedFourierFeatureMap &feature_map, const RectSet &X_bounds, const Set &X_init, const Set &X_unsafe, const FourierBarrierCertificateParameters ¶meters={}) |
| Synthesize the barrier certificate. | |
| const Vector & | coefficients () const |
| Get read-only access to the coefficients of the basis of the Fourier barrier certificate. | |
| std::unique_ptr< BarrierCertificate > | clone () const override |
| Clone the barrier certificate. | |
| std::string | to_string () const override |
| Obtain the string representation of this object. | |
| BarrierCertificate (int T, double gamma, double eta=0, double c=0) | |
| Construct a new BarrierCertificate object. | |
 Public Member Functions inherited from lucid::BarrierCertificate | |
| 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. | |
Private Member Functions | |
| double | apply_impl (ConstVectorRef x) const override |
| Concrete implementation of operator()(). | |
| void | optimiser_callback (bool success, double obj_val, const Vector &coefficients, double eta, double c, double norm, double b_norm) |
| Utility function called by the optimiser when the synthesis is done. | |
Private Attributes | |
| Vector | coefficients_ |
| Coefficients of the Fourier basis. | |
Additional Inherited Members | |
| Protected Attributes inherited from lucid::BarrierCertificate | |
| int | T_ |
| Time horizon. | |
| double | gamma_ |
| \( \gamma \) value in the CBC definition | |
| double | eta_ |
| \( \eta \) value in the CBC definition | |
| double | c_ |
| \( c \) value in the CBC definition | |
| double | norm_ |
| Norm describing the complexity of the barrier. It is 0 if the barrier has not been synthesized. | |
| double | safety_ |
| Safety probability of the system. It is 0 if the barrier has not been synthesized. | |
Barrier certificate using a Fourier basis as a template for the function.
The function is defined as follows:
\[B(x) = \phi_M(x)^T b = \alpha_0 + \sum_{j=1}^{M} \alpha_i \cos{\omega_i^T P(x)} + \beta_i \sin{\omega_i^T P(x)} \]
with
\[b = \begin{bmatrix} \frac{\alpha_0}{\sigma_f^2} & \frac{\alpha_1}{2 \sigma_f^2 \omega_1^2} & \frac{\beta_1}{2 \sigma_f^2 \omega_1^2} & \cdots & \frac{\alpha_M}{2 \sigma_f^2 \omega_M^2} & \frac{\beta_M}{2 \sigma_f^2 \omega_M^2} \end{bmatrix}^T \]
|
nodiscardoverrideprivatevirtual |
Concrete implementation of operator()().
| x | input vector |
Implements lucid::BarrierCertificate.
|
explicit |
Construct a new BarrierCertificate object.
T must be greater than 0. gamma must be greater than or equal to 0. eta must be greater than or equal to 0. c must be greater than or equal to 0. | T | time horizon |
| gamma | \( \gamma \) value in the CBC definition |
| eta | \( \eta \) value in the CBC definition |
| c | \( c \) value in the CBC definition |
|
nodiscardoverridevirtual |
Clone the barrier certificate.
Create a new instance of the barrier certificate with the same parameters. If the barrier was synthesized, the new instance will have the same synthesis results.
Implements lucid::BarrierCertificate.
|
inlinenodiscard |
Get read-only access to the coefficients of the basis of the Fourier barrier certificate.
|
private |
Utility function called by the optimiser when the synthesis is done.
Used to store the results of the synthesis into the barrier certificate object. If the synthesis was unsuccessful, the barrier is left unchanged.
| success | true if the synthesis was successful |
| obj_val | objective value |
| coefficients | coefficients of the basis |
| eta | \( \eta \) value |
| c | \( c \) value |
| norm | actual norm of the barrier function |
| b_norm | target norm for the coefficients of the basis |
| bool lucid::FourierBarrierCertificate::synthesize | ( | const Optimiser & | optimiser, |
| int | lattice_resolution, | ||
| const Estimator & | estimator, | ||
| const TruncatedFourierFeatureMap & | feature_map, | ||
| const RectSet & | X_bounds, | ||
| const Set & | X_init, | ||
| const Set & | X_unsafe, | ||
| const FourierBarrierCertificateParameters & | parameters = {} ) |
Synthesize the barrier certificate.
This is done in multiple steps.
Finding the bounds
First, we find some upper and lower bounds on the value the barrier certificate can assume over \( \texttip{\mathcal{X}}{Initial set}_0 \) and \( \texttip{\mathcal{X}}{Usafe set}_u \). For simplicity, we only explain the process for finding the upper bound over \( \texttip{\mathcal{X}}{Initial set}_0 \), but the same applies to the lower bound over \( \texttip{\mathcal{X}}{Initial set}_0 \) and bounds over \( \texttip{\mathcal{X}}{Usafe set}_u \). We can obtain the lower bound on \( \texttip{\mathcal{X}}{Initial set}_0 \) by using the following inequality:
\[B(x) \le \hat{B}^{\mathcal{X}_0}_{\tilde{N}}C_{\tilde{N}} + R^{\mathcal{\tilde{X}}\setminus\mathcal{X}_0}_{\tilde{N}}\underbrace{\frac{1}{\tilde{N}} \sum_{\bar{x} \in \Theta_{\tilde{N}}\setminus\mathcal{X}_0} D^n_{f_{\max}-\tilde{Q}-f_{\max}}(x - \bar{x})} _{A^{\mathcal{\tilde{X}\setminus\mathcal{X}_0}}_\tilde{N}} \quad \forall x \in \mathcal{X}_0 , \]
where \( R^{\mathcal{\tilde{X}}\setminus\mathcal{X}_0}_{\tilde{N}} = \max_{x \in \Theta_\tilde{N} \setminus \mathcal{X}_0}\{\phi_M(x)^Tb\} - \hat{B}_\tilde{N}^{\mathcal{X}_0} \) is the residual outside \( \texttip{\mathcal{X}}{Initial set}_0 \), and \( C_{\tilde{N}} = \left( 1 - \frac{2 f_{\max}}{\tilde{Q}} \right)^{-\frac{n}{2}} \). Note that we can find the upper bound \( A^{\mathcal{\tilde{X}\setminus\mathcal{X}_0}}_\tilde{N} \) by solving an optimisation problem before starting the synthesis, using, e.g., particle swarm optimisation (PSO).
| optimiser | LP optimiser to use for the synthesis |
| lattice_resolution | number of lattice points on periodic domain per dimension |
| estimator | estimator model to compute the value of the feature map on @xp |
| feature_map | feature map to apply to the lattice points |
| X_bounds | bounds of the set \( \texttip{\mathcal{X}}{Polish sample vector space} \) |
| X_init | initial set \( \texttip{\mathcal{X}}{Initial set}_0 \) |
| X_unsafe | unsafe set \( \texttip{\mathcal{X}}{Usafe set}_u \) |
| parameters | parameters for barrier synthesis |
|
nodiscardoverridevirtual |
Obtain the string representation of this object.
Reimplemented from lucid::BarrierCertificate.
1.13.2