Symbolic Model Checking of Hybrid Systems Using Template Polyhedra

DOI10.1007/978-3-540-78800-3_14zbMath1134.68419OpenAlexW1497013959MaRDI QIDQ5458327

Franjo Ivančić, Thao Dang, Sriram Sankaranarayanan

Publication date: 11 April 2008

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-78800-3_14

Mathematics Subject Classification ID

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

Related Items (17)

Automatic dynamic parallelotope bundles for reachability analysis of nonlinear systems ⋮ Verification of Hybrid Systems ⋮ Geometric Model Checking of Continuous Space ⋮ Hybrid Tools for Hybrid Systems – Proving Stability and Safety at Once ⋮ Computation of polytopic invariants for polynomial dynamical systems using linear programming ⋮ Symbolic analysis of linear hybrid automata -- 25 years later ⋮ Using Intersection of Unions to Minimize Multi-directional Linearization Error in Reachability Analysis ⋮ A Policy Iteration Technique for Time Elapse over Template Polyhedra ⋮ \(\epsilon\)-semantics computations on biological systems ⋮ Counterexample-Guided Refinement of Template Polyhedra ⋮ Reachability computation for polynomial dynamical systems ⋮ Exact join detection for convex polyhedra and other numerical abstractions ⋮ Efficient geometric operations on convex polyhedra, with an application to reachability analysis of hybrid systems ⋮ Template polyhedra and bilinear optimization ⋮ Synthesizing Switching Controllers for Hybrid Systems by Generating Invariants ⋮ Recent developments in theory and tool support for hybrid systems verification with \textsc{HyPro} ⋮ Generating invariants for non-linear hybrid systems

Uses Software

• PHAVer
• HyTech
• RSOLVER
• Benchmarks
• HSolver
• d/dt

Cites Work

• Newton: Constraint programming over nonlinear constraints
• Semidefinite programming relaxations for semialgebraic problems
• Counterexample-guided predicate abstraction of hybrid systems
• A Policy Iteration Technique for Time Elapse over Template Polyhedra
• A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Static Analysis
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Computer Aided Verification
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Symbolic Model Checking of Hybrid Systems Using Template Polyhedra