Counterexample-Guided Refinement of Template Polyhedra
From MaRDI portal
Publication:3303915
DOI10.1007/978-3-662-54577-5_34zbMath1452.68099OpenAlexW2602950602WikidataQ62037202 ScholiaQ62037202MaRDI QIDQ3303915
Mirco Giacobbe, Goran Frehse, Sergiy Bogomolov, Thomas A. Henzinger
Publication date: 5 August 2020
Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)
Full work available at URL: https://eprint.ncl.ac.uk/271826
hybrid automataabstract interpretercounter-example guided abstraction refinement (CEGAR)spurious counter-examplestemplate polyhedra
Related Items (7)
Geometric Model Checking of Continuous Space ⋮ Symbolic analysis of linear hybrid automata -- 25 years later ⋮ Using Intersection of Unions to Minimize Multi-directional Linearization Error in Reachability Analysis ⋮ Fully-Automated Verification of Linear Systems Using Reachability Analysis with Support Functions ⋮ Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration ⋮ Template polyhedra and bilinear optimization ⋮ Decomposing reach set computations with low-dimensional sets and high-dimensional matrices (extended version)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Quantifier-free encoding of invariants for hybrid systems
- An exact duality theory for semidefinite programming and its complexity implications
- Second-order cone programming
- Flowpipe approximation and clustering in space-time
- Eliminating spurious transitions in reachability with support functions
- Parallelotope Bundles for Polynomial Reachability
- Grammar Analysis and Parsing by Abstract Interpretation
- Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction
- Image Computation for Polynomial Dynamical Systems Using the Bernstein Expansion
- Reachability Analysis of Hybrid Systems Using Support Functions
- Path-Oriented Reachability Verification of a Class of Nonlinear Hybrid Automata Using Convex Programming
- Reachability Analysis of Polynomial Systems Using Linear Programming Relaxations
- Using Redundant Constraints for Refinement
- Lazy abstraction
- Symbolic Model Checking of Hybrid Systems Using Template Polyhedra
- Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems
- Hybrid Systems: Computation and Control
- Verification, Model Checking, and Abstract Interpretation
- Lazy Abstraction with Interpolants
- Formal Modeling and Analysis of Timed Systems
This page was built for publication: Counterexample-Guided Refinement of Template Polyhedra