Abstract
This paper presents Fossil 2.0, a new major release of a software tool for the synthesis of certificates (e.g., Lyapunov and barrier functions) for dynamical systems modelled as ordinary differential and difference equations. Fossil 2.0 is much improved from its original release, including new interfaces, a significantly expanded certificate portfolio, controller synthesis and enhanced extensibility. We present these new features as part of this tool paper. Fossil implements a counterexample-guided inductive synthesis (CEGIS) loop ensuring the soundness of the method. Our tool uses neural networks as templates to generate candidate functions, which are then formally proven by an satisfiability modulo theories solver acting as an assertion verifier. Improvements with respect to the first release include a wider range of certificates, synthesis of control laws, and support for discrete-time models.
| Original language | English |
|---|---|
| Title of host publication | Proceedings of the 27th International Conference on Hybrid Systems: Computation and Control, Part of CPS-IoT Week, HSCC 2024 |
| Editors | Erika Ábrahám, Manuel Mazo |
| Place of Publication | New York, NY |
| Publisher | ACM |
| Number of pages | 10 |
| ISBN (Electronic) | 979-8-4007-0522-9 |
| DOIs | |
| Publication status | Published - 2024 |
| Event | HSCC 2024: 27th ACM International Conference on Hybrid Systems: Computation and Control - Hong Kong Science Park, Hong Kong, China Duration: 14 May 2024 → 16 May 2024 https://hscc.acm.org/2024/ |
Conference
| Conference | HSCC 2024 |
|---|---|
| Country/Territory | China |
| City | Hong Kong |
| Period | 14/05/24 → 16/05/24 |
| Internet address |
Keywords
- CEGIS
- Computer-aided control design
- Lyapunov-like functions
- Neural networks
- SAT-modulo theories