Counterexample-Guided Refinement of Template Polyhedra

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

zbMATH Keywords

hybrid automataabstract interpretercounter-example guided abstraction refinement (CEGAR)spurious counter-examplestemplate polyhedra

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

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

• PHAVer
• HyTech
• GLPK
• Mosek
• SpaceEx
• XSpeed
• Flow*

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