Template-Based Unbounded Time Verification of Affine Hybrid Automata
DOI10.1007/978-3-642-25318-8_6zbMATH Open1348.68100OpenAlexW2107265973MaRDI QIDQ2901366FDOQ2901366
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
Formal languages and automata (68Q45) Analysis of algorithms and problem complexity (68Q25) 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) Semantics in the theory of computing (68Q55)
Cites Work
- Title not available (Why is that?)
- Hybrid Systems: Computation and Control
- A lattice-theoretical fixpoint theorem and its applications
- Hybrid Systems: Computation and Control
- Grammar Analysis and Parsing by Abstract Interpretation
- Deciding the winner in parity games is in \(\mathrm{UP}\cap\mathrm{co-UP}\)
- Computer Aided Verification
- Static Analysis by Policy Iteration on Relational Domains
- Precise Fixpoint Computation Through Strategy Iteration
- Coupling Policy Iteration with Semi-definite Relaxation to Compute Accurate Numerical Invariants in Static Analysis
- Precise Relational Invariants Through Strategy Iteration
- Computing Relaxed Abstract Semantics w.r.t. Quadratic Zones Precisely
- Verification, Model Checking, and Abstract Interpretation
- Hybridization methods for the analysis of nonlinear systems
- Counterexample-guided predicate abstraction of hybrid systems
- Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems
- Discretizing Affine Hybrid Automata with Uncertainty
- A Policy Iteration Technique for Time Elapse over Template Polyhedra
- Computing the smallest fixed point of order-preserving nonexpansive mappings arising in positive stochastic games and static analysis of programs
- Improving Strategies via SMT Solving
Cited In (9)
- Automatic dynamic parallelotope bundles for reachability analysis of nonlinear systems
- Numerical invariants through convex relaxation and max-strategy iteration
- Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration
- Hypervolume Approximation in Timed Automata Model Checking
- 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
- Validating numerical semidefinite programming solvers for polynomial invariants
- Symbolic analysis of linear hybrid automata -- 25 years later
- Using Intersection of Unions to Minimize Multi-directional Linearization Error in Reachability Analysis
This page was built for publication: Template-Based Unbounded Time Verification of Affine Hybrid Automata
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2901366)
