Computing Differential Invariants of Hybrid Systems as Fixedpoints

DOI10.1007/978-3-540-70545-1_17zbMath1155.68445MaRDI 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 invariants; verification logic; verification of hybrid systems; fixedpoint engine

Mathematics Subject Classification ID

93C95: Application models in control theory

68Q60: Specification and verification (program logics, model checking, etc.)

Related Items

Real World Verification, Direct Formal Verification of Liveness Properties in Continuous and Hybrid Dynamical Systems, Barrier certificates revisited, Specifications for decidable hybrid games, Generating invariants for non-linear loops by linear algebraic methods, Computing differential invariants of hybrid systems as fixed points, Computation of polytopic invariants for polynomial dynamical systems using linear programming, Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants, Generating invariants for non-linear hybrid systems, Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems, A compositional modelling and verification framework for stochastic hybrid systems, Synthesizing Switching Controllers for Hybrid Systems by Generating Invariants, Formal Modelling, Analysis and Verification of Hybrid Systems, Computing Differential Invariants of Hybrid Systems as Fixedpoints

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