Template-Based Unbounded Time Verification of Affine Hybrid Automata

DOI10.1007/978-3-642-25318-8_6zbMath1348.68100OpenAlexW2107265973MaRDI QIDQ2901366

Thao Dang, Thomas Martin Gawlitza

Publication date: 20 July 2012

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-25318-8_6

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Formal languages and automata (68Q45) Semantics in the theory of computing (68Q55) 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)

Related Items (8)

Automatic dynamic parallelotope bundles for reachability analysis of nonlinear systems ⋮ Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration ⋮ A piecewise ellipsoidal reachable set estimation method for continuous bimodal piecewise affine systems ⋮ Symbolic analysis of linear hybrid automata -- 25 years later ⋮ Using Intersection of Unions to Minimize Multi-directional Linearization Error in Reachability Analysis ⋮ Numerical invariants through convex relaxation and max-strategy iteration ⋮ Validating numerical semidefinite programming solvers for polynomial invariants ⋮ Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration

Cites Work

• Unnamed Item
• Deciding the winner in parity games is in \(\mathrm{UP}\cap\mathrm{co-UP}\)
• Hybridization methods for the analysis of nonlinear systems
• Computing the smallest fixed point of order-preserving nonexpansive mappings arising in positive stochastic games and static analysis of programs
• Counterexample-guided predicate abstraction of hybrid systems
• A lattice-theoretical fixpoint theorem and its applications
• Improving Strategies via SMT Solving
• Discretizing Affine Hybrid Automata with Uncertainty
• A Policy Iteration Technique for Time Elapse over Template Polyhedra
• Coupling Policy Iteration with Semi-definite Relaxation to Compute Accurate Numerical Invariants in Static Analysis
• Grammar Analysis and Parsing by Abstract Interpretation
• Precise Relational Invariants Through Strategy Iteration
• Computing Relaxed Abstract Semantics w.r.t. Quadratic Zones Precisely
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems
• Verification, Model Checking, and Abstract Interpretation
• Computer Aided Verification
• Static Analysis by Policy Iteration on Relational Domains
• Precise Fixpoint Computation Through Strategy Iteration

This page was built for publication: Template-Based Unbounded Time Verification of Affine Hybrid Automata