The Image Computation Problem in Hybrid Systems Model Checking

DOI10.1007/978-3-540-71493-4_37MaRDI QIDQ3612995zbMATH OpenOpenAlexFDO

Authors André Platzer, Edmund Clarke

Publication date 11 March 2009

Published in Hybrid Systems: Computation and Control (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-71493-4_37

zbMATH Keywords

hybrid systemsmodel checkingimage computation

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Attainable sets, reachability (93B03) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30) Application models in control theory (93C95)

Recommendations

• Computer Aided Verification
• Efficient image computation in infinite state model checking.
• scientific article; zbMATH DE number 1670789
• Hybrid Systems: Computation and Control
• scientific article; zbMATH DE number 1303060
• Hybrid diagrams: a deductive-algorithmic approach to hybrid system verification
• Improving HyLTL model checking of hybrid systems
• A compositional approach to the verification of hybrid systems
• Computational techniques for hybrid system verification

Cited in

(16)

• Differential dynamic logic for hybrid systems
• Efficient image computation in infinite state model checking.
• Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces
• A formal framework for Hybrid Event B
• Superposition modulo non-linear arithmetic
• Computing differential invariants of hybrid systems as fixed points
• Verifiably safe exploration for end-to-end reinforcement learning
• ModelPlex: verified runtime validation of verified cyber-physical system models
• Exact asymptotic stability analysis and region-of-attraction estimation for nonlinear systems
• Verification of Hybrid Systems
• Exact safety verification of hybrid systems using sums-of-squares representation
• Set-valued state estimation of nonlinear discrete-time systems with nonlinear invariants based on constrained zonotopes
• Guaranteed methods based on constrained zonotopes for set-valued state estimation of nonlinear discrete-time systems
• Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space
• Computing Differential Invariants of Hybrid Systems as Fixedpoints
• Quantifier-free encoding of invariants for hybrid systems

This page was built for publication: The Image Computation Problem in Hybrid Systems Model Checking

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3612995)