2024 Fiscal Year Research-status Report
Safety Verification of Black Box Cyber-Physical Systems via Lyapunov Stability Certificates
| Project/Area Number |
24K23861
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
Hsieh Chiao (謝橋) 京都大学, 情報学研究科, 特定助教 (71006426)
|
|---|
| Project Period (FY) |
2024-07-31 – 2026-03-31
|
| Keywords | 形式検証 / サイバーフィジカルシステム / 安定性解析 / ブラックボックスモデル |
|---|
| Outline of Annual Research Achievements |
This year, PI followed the project proposal to achieve the expected result in Phase 1. The major goal in Phase 1 is to establish a baseline black-box analysis for certifying the Lyapunov stability of continuous-time dynamics. Combining the recent idea of sampling and exploiting Lipschitz continuity to approximate the continuous-time dynamics, PI developed a new analysis based on the learner-verifier architecture from Counterexample-Guided Inductive Synthesis, and PI extended the analysis with parallelized verification for different regions of the state space. This new analysis has significant reduced the number of required samples for certifying the stability of 2D and 3D systems compared with the existing analysis. In addition, PI provided a rigorous termination guarantee to ensure the analysis will always finish and answer if the continuous-time dynamics is provably stable, or no proofs can be found in the predefined hypothesis space.
PI has coauthored and submitted a research conference paper summarizing the research outcome in this study, and the paper is accepted by and will be published in the 28th ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2025) in May 2025.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
PI has developed a new black-box analysis as planned, and the analysis has shown great improvement over the existing analysis. The research paper is further accepted by the top international conference.
|
| Strategy for Future Research Activity |
Next year, PI plans to follow the project proposal and achieve the goal for Phase 2. The major goal in Phase 2 is to extend the above-mentioned baseline analysis to support hybrid systems with both continuous-time dynamics and discrete-time transitions. This will enable the analysis on more realistic cyber-physical systems. PI also plans to improve the baseline analysis to handle systems with 4D or more dimensions by better parallelization and optimization techniques.
|
| Causes of Carryover |
In the current fiscal year, the amount to be used in the next fiscal year is incurred because there are delays in the purchase of computers and equipment, and the travel expenses were less than expected because the international conferences were held in Japan. In the following fiscal year, PI plans to use the grant for the purchase of computers and equipment that could not be purchased in the current fiscal year. In addition, PI will use the fund to visit research institutes and attend international conferences oversea.
|
