Computing Differential Invariants of Hybrid Systems as Fixedpoints

DOI10.1007/978-3-540-70545-1_17zbMath1155.68445OpenAlexW3021664313MaRDI QIDQ3512492

André Platzer, Edmund M. Clarke

Publication date: 15 July 2008

Published in: Computer Aided Verification (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-70545-1_17

zbMATH Keywords

differential invariantsverification logicverification of hybrid systemsfixedpoint engine

Mathematics Subject Classification ID

Application models in control theory (93C95) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (18)

Synthesizing invariant barrier certificates via difference-of-convex programming ⋮ Characterizing positively invariant sets: inductive and topological methods ⋮ Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems ⋮ A compositional modelling and verification framework for stochastic hybrid systems ⋮ Formal Modelling, Analysis and Verification of Hybrid Systems ⋮ Computation of polytopic invariants for polynomial dynamical systems using linear programming ⋮ Computing Differential Invariants of Hybrid Systems as Fixedpoints ⋮ Generating invariants for non-linear loops by linear algebraic methods ⋮ Specifications for decidable hybrid games ⋮ Barrier certificates revisited ⋮ Real World Verification ⋮ Direct Formal Verification of Liveness Properties in Continuous and Hybrid Dynamical Systems ⋮ Automated and formal synthesis of neural barrier certificates for dynamical models ⋮ Computing differential invariants of hybrid systems as fixed points ⋮ Synthesizing Switching Controllers for Hybrid Systems by Generating Invariants ⋮ Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants ⋮ Encoding inductive invariants as barrier certificates: synthesis via difference-of-convex programming ⋮ Generating invariants for non-linear hybrid systems

Uses Software

• QEPCAD
• KeYmaera
• PHAVer
• HyTech

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Differential dynamic logic for hybrid systems
• Partial cylindrical algebraic decomposition for quantifier elimination
• Program invariants as fixedpoints
• Hybrid systems: computation and control. 7th international workshop, HSCC 2004, Philadelphia, PA, USA, March 25--27, 2004. Proceedings.
• Hybrid systems: computation and control. 10th international conference, HSCC 2007, Pisa, Italy, April 3--5, 2007. Proceedings.
• Computing Differential Invariants of Hybrid Systems as Fixedpoints
• Systematic Simulation Using Sensitivity Analysis
• The Image Computation Problem in Hybrid Systems Model Checking
• Conflict resolution for air traffic management: a study in multiagent hybrid systems
• A Framework for Worst-Case and Stochastic Safety Verification Using Barrier Certificates
• Hybrid Systems: Computation and Control
• Differential Dynamic Logic for Verifying Parametric Hybrid Systems
• Automated Technology for Verification and Analysis
• Hybrid Systems: Computation and Control
• Computer Aided Verification

This page was built for publication: Computing Differential Invariants of Hybrid Systems as Fixedpoints