Constructing invariants for hybrid systems

DOI10.1007/s10703-007-0046-1zbMath1133.68365OpenAlexW2087749124MaRDI QIDQ2475635

Zohar Manna, Sriram Sankaranarayanan, Henny B. Sipma

Publication date: 11 March 2008

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-007-0046-1

zbMATH Keywords

Gröbner basesHybrid systemsAnalysisInvariantsAlgebraic geometryVerificationPolynomials

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Formal languages and automata (68Q45) Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases) (13P10)

Related Items (20)

Verification of Hybrid Systems ⋮ Pegasus: sound continuous invariant generation ⋮ Reachable set estimation and safety verification of nonlinear systems via iterative sums of squares programming ⋮ Exact safety verification of hybrid systems using sums-of-squares representation ⋮ Synthesizing ReLU neural networks with two hidden layers as barrier certificates for hybrid systems ⋮ Verifying Neural Network Controlled Systems Using Neural Networks ⋮ Change-of-bases abstractions for non-linear hybrid systems ⋮ SAT modulo linear arithmetic for solving polynomial constraints ⋮ Invariants for Parameterised Boolean Equation Systems ⋮ Efficient solution of a class of quantified constraints with quantifier prefix exists-forall ⋮ A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets ⋮ A search-based procedure for nonlinear real arithmetic ⋮ Invariants for parameterised Boolean equation systems ⋮ Unnamed Item ⋮ Validating numerical semidefinite programming solvers for polynomial invariants ⋮ Safety verification of interconnected hybrid systems using barrier certificates ⋮ Speeding up the Constraint-Based Method in Difference Logic ⋮ Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants ⋮ Explaining AI decisions using efficient methods for learning sparse Boolean formulae ⋮ Generating invariants for non-linear hybrid systems

Uses Software

• QEPCAD
• Kronos
• HyTech
• Uppaal
• d/dt

Cites Work

• Partial cylindrical algebraic decomposition for quantifier elimination
• Affine relationships among variables of a program
• Notes on Gröbner bases
• Semidefinite programming relaxations for semialgebraic problems
• Kronos: A verification tool for real-time systems
• Non-linear loop invariant generation using Gröbner bases
• Automatic Generation of Polynomial Loop Invariants
• Term Rewriting and All That
• Verification: Theory and Practice
• Hybrid Systems: Computation and Control
• Static Analysis
• Static Analysis
• Static Analysis
• Computer Aided Verification
• Symbolic reachability computation for families of linear vector fields
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Constructing invariants for hybrid systems