Source-linked AI summary
Computing Semi-algebraic Invariants for Polynomial Dynamical Systems
Jiang Liu, Naijun Zhan, Hengjun Zhao
TL;DR
Discovering invariants strong enough for safety verification is challenging, while direct reachable-set methods may require solving or approximating differential equations. The paper gives a sound and complete criterion for checking semi-algebraic invariants and a relatively complete template-based generation method; it reports generating more invariants than related work.
Problem
Discovering invariants strong enough to imply a safety property is challenging, and direct reachable-set methods require exact or approximate solutions of differential equations.
Source: §1.1 · p. 1Method
The paper presents a sound and complete criterion for checking semi-algebraic invariants and a relatively complete method for generating them using templates.
Source: §8 · p. 12Results
The paper reports that its approach generates more invariants than related work, as demonstrated by examples and case studies.
Source: §8 · p. 12Takeaways & Limitations
The approach completes the gap left open in.
Source: §8 · p. 12First-order quantifier elimination has doubly exponential cost, making efficiency a main target for future work.
Source: §8 · p. 12
Abstract
from arXiv · showhide
In this paper, we consider an extended concept of invariant for polynomial dynamical system (PDS) with domain and initial condition, and establish a sound and complete criterion for checking semi-algebraic invariants (SAI) for such PDSs. The main idea is encoding relevant dynamical properties as conditions on the high order Lie derivatives of polynomials occurring in the SAI. A direct consequence of this criterion is a relatively complete method of SAI generation based on template assumption and semi-algebraic constraint solving. Relative completeness means if there is an SAI in the form of a predefined template, then our method can indeed find one using this template.
1. INTRODUCTION
The paper addresses invariant discovery for hybrid-system modes, where continuous dynamics make inductive invariants difficult to find and direct reachability methods have limited scope. It develops a sound and complete SAI-checking criterion and relatively complete template-based generation method for polynomial systems.
1. INTRODUCTION
- Hybrid systems combine continuous evolutions and discrete transitions, and safety asks whether unsafe states are unreachable from initial states along system trajectories.Source: §1 · p. 1
1.1 Motivation
- Direct reachability methods have limited scope, while discovering sufficiently strong invariants is the main challenge for inductive safety verification of hybrid systems.The paper focuses on continuous invariants at a single mode; global inductiveness across discrete transitions is outside its scope.Source: §1.1 · pp. 1–2
1.2 Related Work
- Earlier algebraic-invariant methods use ideal theory, while inequality-based methods include barrier certificates and differential induction; some approaches have soundness problems at boundaries.The paper notes that differential induction is sound but imposes a strong condition.Source: §1.2 · p. 2
1.3 Our Contribution
- The method checks semi-algebraic invariants soundly and completely, and generates one whenever an invariant exists in the predefined template.The paper also presents the method as resolving the computational infeasibility of earlier higher-order Lie-derivative rules that required infinitely many candidate tests.Source: §1.3 · p. 2
1.4 Paper Organization
- The paper proceeds from preliminaries and SAI definitions to fundamental results, generation methods, case studies, and conclusions.Source: §1.4 · p. 2
2. PRELIMINARIES
The preliminaries establish the algebraic and dynamical vocabulary used to define polynomial systems and analyze their trajectories. Higher-order Lie derivatives provide information about trajectory tendencies when the first derivative is inconclusive.
2. PRELIMINARIES
- The preliminaries set notation for rational-coefficient polynomials and define atomic formulas using polynomial comparisons with zero.Source: §2.1 · p. 2, §2.2 · p. 3
2.1 Polynomial Ideal Theory
- Polynomial ideals have finite generating sets and satisfy the ascending chain condition, while templates use parameters whose instantiations substitute fixed coefficient values.Source: §2.1 · pp. 2–3
2.2 Semi-algebraic Set
- Semi-algebraic sets are described by quantifier-free polynomial formulas and are closed under basic set operations.Source: §2.2 · p. 3
2.3.1 Trajectories of Continuous Dynamical System
- A continuous dynamical system is modeled by first-order ordinary differential equations, and local Lipschitz continuity ensures a unique local solution from each initial state.Source: §2.3.1 · p. 3
2.3.2 Polynomial Vector Field and Lie Derivatives
- For polynomial vector fields, Lie derivatives are formed iteratively from the gradient and vector field, and their values describe how a polynomial changes along trajectories.If the first Lie derivative is zero, a nonzero higher-order derivative can determine the trajectory's tendency; the pointwise rank identifies the first such order, or infinity if none exists.Source: §2.3.2 · pp. 3–4
- The first nonzero Lie derivative at a boundary point determines the local sign change of the polynomial along the trajectory and supports defining a transverse set.The transverse set marks points outside the nonnegative region or boundary points whose trajectories immediately exit it.Source: §2.3.2 · pp. 4–5
3. SEMI-ALGEBRAIC INVARIANT
The paper formalizes continuous invariants for systems with domains and initial states, then specializes to polynomial dynamical systems and semi-algebraic invariants. This framework supports the paper's sound and complete method for discovering such invariants.
3. SEMI-ALGEBRAIC INVARIANT
- The paper's target is automatic SAI discovery for polynomial systems with domain and initial conditions, with the resulting method intended to support verification of polynomial hybrid systems.Source: §3 · p. 5
3.1 Continuous Invariants of CDSwDI
- A continuous invariant contains the initial states and preserves its property along continuous evolutions that start there, for as long as they remain in the domain.Source: §3.1 · p. 5
- A continuous invariant need not be contained in the domain; even any set containing the domain qualifies, a feature useful when verifying hybrid systems across modes.Source: §3.1 · p. 5
3.2 PDS and SAI
- A PDS has a semi-algebraic domain and initial states and a polynomial vector field; its semi-algebraic continuous invariants are called SAIs.Source: §3.2 · p. 5
- The paper presents a sound and complete method to automatically discover SAIs for a PDS.Source: §3.2 · p. 5
4. FUNDAMENTAL RESULTS
For polynomial p and vector field f, the rank bounds finite Lie-derivative order, making the associated transition set computable and semi-algebraic. The bound also extends uniformly to parametric polynomials.
4. FUNDAMENTAL RESULTS
- The set Transf↑p is semi-algebraic and computable for polynomial p and polynomial vector field f.Its computability follows from a computable upper bound on the rank.Source: §4 · pp. 5–6
- For polynomial p and f, every finite γp,f(x) is bounded by an integer N uniformly over x ∈ R^n.The paper calls such an N the rank of p and f.Source: §4 · p. 5
- The rank bound follows from stabilization of the decreasing sets D_l, using finite generation of the ideal of Lie derivatives.Once D_l stabilizes, later derivatives vanish on that set, yielding a cutoff for finite γp,f(x).Source: §4 · p. 5
- A computable upper bound on γp,f can be found effectively, although the paper does not give an expression for γp,f itself.The minimal index satisfying the fixed-point condition gives an upper bound; Example 8 has N_h,f = 2.Source: §4 · pp. 5–6
- For parametric polynomial p(u, x), one integer N bounds every finite γ_pu0,f(x) across all x ∈ R^n and parameter choices u0 ∈ R^t.The parametric rank result supports the polynomial templates used in SAI generation.Source: §4 · p. 6
5. GENERATING SAI IN SIMPLE CASE
For a polynomial inequality candidate, the section gives a necessary-and-sufficient SAI criterion and uses it to generate invariants through template constraints and quantifier elimination. A worked example produces an invariant for a specified system, domain, and initial states.
5. GENERATING SAI IN SIMPLE CASE
- Theorem 17 characterizes p(x) ≥ 0 as an SAI exactly when the criterion formula and the initial-state implication hold for all x ∈ R^n.The criterion is derived from the boundary behavior of the candidate invariant within the domain.Source: §5 · p. 6
- The generation procedure chooses a parametric polynomial template and applies quantifier elimination to derive constraints on its coefficients.If the resulting formula is false, no polynomial continuous invariant of degree at most d exists for that setting.Source: §5 · p. 7
- A solution to the coefficient constraints yields an invariant when instantiated, using a rational sample if available or an algebraic sample otherwise.A simplified template can reduce search complexity; choosing specific nonzero-coefficient terms can also impose special conditions.Source: §5 · p. 7
- For the example system, quantifier elimination gives a ≤ 0, and choosing a = −1 yields −xy + y² ≥ 0 as an invariant.The example uses domain h(x, y) = −x − y² ≥ 0 and two specified initial states.Source: §5 · p. 7
6. GENERAL CASE
The general-case method handles complicated domain boundaries by encoding trajectory-based invariance conditions as polynomial formulas for SAI checking and generation, with generation complete relative to a predefined template. An example illustrates a generated semi-algebraic set that is neither open nor closed.
6. GENERAL CASE
- The general-case procedure follows the earlier generation steps but handles complicated boundaries through topological conditions that are equivalently encoded as first-order polynomial formulas.The SAI conditions rely on results expressing trajectory behavior through polynomial Lie-derivative formulas.Source: §6 · p. 7, §6.2 · pp. 9–10
6.1 Necessary and Sufficient Condition for CI
- Theorem 19 characterizes continuous invariance through necessary-and-sufficient conditions using forward and backward trajectory behavior at set interiors and exteriors.The section introduces immediate-entry and immediate-exit sets, including their backward-time counterparts, for this topological analysis.Source: §6.1 · p. 8
6.2 Necessary and Sufficient Condition for SAI
- Theorem 29 gives a sound and complete criterion for checking semi-algebraic invariants and a sound generation method complete relative to its predefined template.The method considers arbitrary semi-algebraic invariant sets, which may be neither open nor closed.Source: §6.2 · p. 10
- For the example template x−a ≥0 ∨ y−b >0, quantifier elimination yields a+b ≤0 ∧ b ≤0, and a=−1, b=−0.5 produces an SAI.The resulting invariant is {(x,y) ∈ R^2 | x ≥−1 ∨ y > −0.5}.Source: §6.2 · pp. 10–11
- In the example, the generated SAI is a union of two simple semi-algebraic sets and is neither closed nor open.Source: §6.2 · p. 11
7. CASE STUDY
The case studies apply continuous-invariant generation to CTCS-3 train safety and two-aircraft collision-avoidance dynamics. They illustrate invariant checking and generation using the paper’s method.
7.1 Formal Verification of CTCS-3
- The CTCS-3 safety check reduces to testing whether v < v.Seg is a continuous invariant of the train’s polynomial dynamical system.The system domain is v < v.Seg, with initial velocity below the segment limit.Source: §7.1 · p. 11
- A prior directional-derivative sign principle may fail for this invariant because its required condition is false when a ≥ 0.The example illustrates the claimed completeness advantage of the paper’s criterion over that principle.Source: §7.1 · p. 11
7.2 Collision Avoidance Maneuvers
- For the two-aircraft dynamics, the method enumerates polynomial templates and uses quantifier elimination to obtain constraints for assigning invariant coefficients.The example reports template constraints and resulting polynomial invariants.Source: §7.2 · pp. 11–12
- Arbitrary semi-algebraic templates can generate invariants beyond polynomial equations, at the cost of heavier computation.Source: §7.2 · p. 12
8. CONCLUSIONS
The paper presents a sound and complete criterion for checking semi-algebraic invariants and a relatively complete template-based generation method. It identifies efficiency and extensions beyond polynomial vector fields as future work.
8. CONCLUSIONS
- The paper establishes a sound and complete criterion for checking semi-algebraic invariants of polynomial dynamical systems.Source: §8 · p. 12
- It also gives a relatively complete method for automatic invariant generation using templates and reports that it can generate more invariants than related work.The method is based on computable algebraic-geometry theory and is demonstrated with examples and case studies.Source: §8 · p. 12
- Future work includes extending the approach beyond polynomial vector fields and improving efficiency, since first-order quantifier elimination has doubly exponential cost.For linear templates, the authors identify linear programming as a potentially helpful way to reduce complexity.Source: §8 · p. 12