Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models

Alec Edwards, Andrea Peruffo, Alessandro Abate

TL;DR

Fossil 2.0 tackles the challenge of formally verifying and controlling dynamical systems by automatically synthesizing certificates and, in parallel, neural controllers. It extends the prior Fossil release with a broad portfolio of properties (e.g., ROA, SWA, RWA, RSWA, RAR) for continuous- and discrete-time models, all within a unified CEGIS framework that uses neural templates and SMT verification (CVC5). The tool offers a new CLI, a Python API, and an extensible certificate framework that accommodates bespoke domains, delivering robust, sound certificates with favorable performance relative to the 1.0 release. A case study on an inverted pendulum demonstrates concurrent certificate and controller synthesis, underscoring the approach’s practical potential for verification-driven controller design in complex dynamical systems.

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 SMT 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.

Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models

TL;DR

Fossil 2.0 tackles the challenge of formally verifying and controlling dynamical systems by automatically synthesizing certificates and, in parallel, neural controllers. It extends the prior Fossil release with a broad portfolio of properties (e.g., ROA, SWA, RWA, RSWA, RAR) for continuous- and discrete-time models, all within a unified CEGIS framework that uses neural templates and SMT verification (CVC5). The tool offers a new CLI, a Python API, and an extensible certificate framework that accommodates bespoke domains, delivering robust, sound certificates with favorable performance relative to the 1.0 release. A case study on an inverted pendulum demonstrates concurrent certificate and controller synthesis, underscoring the approach’s practical potential for verification-driven controller design in complex dynamical systems.

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 SMT 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.
Paper Structure (27 sections, 12 equations, 4 figures, 4 tables)

This paper contains 27 sections, 12 equations, 4 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Overview of Functionality
  3. Tool Scope and Breadth
  4. Scope
  5. Properties
  6. Lyapunov Stability
  7. Region of Attraction (ROA)
  8. Barrier Functions for Safety
  9. Stable While Avoid
  10. Reach While Avoid
  11. Reach-and-Stay While Avoid
  12. Reach, Avoid and Remain
  13. A Note on Control Models
  14. Inductive Certificate Synthesis with Counter-Examples
  15. Tool Use -- Operating Instructions
  16. ...and 12 more sections

Figures (4)

  • Figure 1: General architecture of Fossil 2.0.
  • Figure 2: Pictorial depiction of relevant properties verifiable by Fossil 2.0. Here, $\mathcal{X}_I$ is the initial set, $\mathcal{X}_U$ the unsafe set ($\mathcal{X}_S$ is its safe complement), $\mathcal{X}_G$ the goal/target set, $\mathcal{X}_F$ the final set. (The entire state space is $\mathcal{X}$.) A dashed background denotes that the corresponding set's existence is implied by the corresponding certificate, but that it is not explicitly defined in the property.
  • Figure 3: Schematic representation of the Certificate class providing required functionality to the components of CEGIS.
  • Figure 4: Phase plane of the closed loop model for the presented case study, as well as the zero contours of the two functions that comprise the reach-avoid-remain certificate.