UC5 Mapping-2-18 EvalCriteriaV&V-1

Evaluation of volume of synthesized stable region and of robustness to parameter changes via multiple methods.
We contribute by certifying the stability of hybrid systems by mean of symbolic techniques. The model considered is a hybrid system with two modes, each one consisting of an affine dynamical system. The evaluation focuses on two aspects: the synthesis of a robust region (with fixed reference values), and robustness to reference values changes. We approach these two targets using the tool Sabbath, which computes and certifies quadratic Lyapunov functions.   To assess the scalability of the algorithm, we consider different sizes of the problem, obtained by Balanced Truncation Model Reduction on the full system; we also consider Lyapunov functions obtained using different algorithms, and we validate them using different SMT solvers or symbolic methods.  Out of 192 problems: 186 Lyapunov functions were validated, 2 proved incorrect, and 4 syntheses failed due to timeout. The volume of the synthesized regions and the robustness to reference values changes depends on the method used to synthesize the Lyapunov function and on the specific dynamical system considered. We evaluate "time": the time in seconds needed to compute the robust region; "vol": the volume of such region; and "ϵ": the radius of the ball that is proved to be a robust region for reference values changes. These results are related to Eval_VV_3 – Number of test cases, Eval_VV_1 – Time of test execution, and Eval_SCP_11 – Simulation level system robustness. The quantitative improvement can vary, based on how many test cases belong to the synthesized region of certified stability. Therefore, the total saving depends on the density of the test cases. Implementing multiple methods instead of just one can boost the results by up to 30%. This improvement is measured with respect to the linearized volume (21st root of the volume) since we are comparing volumes of 21-dimensional regions.
UC5
Evaluation Criteria for V&V Processes
Time of execution

The quantitative improvement can vary, based on how many test cases belong to the synthesized region of certified stability. Therefore, the total saving depends on the density of the test cases. Implementing multiple methods instead of just one can boost the results by up to 30%. This improvement is measured with respect to the linearized volume (21st root of the volume) since we are comparing volumes of 21-dimensional regions.

We contribute by certifying the stability of hybrid systems by mean of symbolic techniques. The model considered is a hybrid system with two modes, each one consisting of an affine dynamical system. The evaluation focuses on two aspects: the synthesis of a robust region (with fixed reference values), and robustness to reference values changes. We approach these two targets using the tool Sabbath, which computes and certifies quadratic Lyapunov functions.  

To assess the scalability of the algorithm, we consider different sizes of the problem, obtained by Balanced Truncation Model Reduction on the full system; we also consider Lyapunov functions obtained using different algorithms, and we validate them using different SMT solvers or symbolic methods. 
Out of 192 problems: 186 Lyapunov functions were validated, 2 proved incorrect, and 4 syntheses failed due to timeout. The volume of the synthesized regions and the robustness to reference values changes depends on the method used to synthesize the Lyapunov function and on the specific dynamical system considered. We evaluate "time": the time in seconds needed to compute the robust region; "vol": the volume of such region; and "ϵ": the radius of the ball that is proved to be a robust region for reference values changes.

Contents

There are currently no items in this folder.