Template-based unbounded time verification of affine hybrid automata

DOI10.1007/978-3-642-25318-8_6MaRDI QIDQ2901366zbMATH OpenOpenAlexFDO

Authors 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

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)

Recommendations

• A Policy Iteration Technique for Time Elapse over Template Polyhedra
• Symbolic Model Checking of Hybrid Systems Using Template Polyhedra
• Discretizing affine hybrid automata with uncertainty
• Space-time interpolants
• Counterexample-Guided Refinement of Template Polyhedra

Cites work

• scientific article; zbMATH DE number 2085344 (Why is no real title available?)
• A Policy Iteration Technique for Time Elapse over Template Polyhedra
• A lattice-theoretical fixpoint theorem and its applications
• Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems
• Computer Aided Verification
• Computing relaxed abstract semantics w.r.t. quadratic zones precisely
• 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
• Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis
• Deciding the winner in parity games is in \(\mathrm{UP}\cap\mathrm{co-UP}\)
• Discretizing affine hybrid automata with uncertainty
• Grammar Analysis and Parsing by Abstract Interpretation
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Hybridization methods for the analysis of nonlinear systems
• Improving strategies via SMT solving
• Precise Fixpoint Computation Through Strategy Iteration
• Precise Relational Invariants Through Strategy Iteration
• Static Analysis by Policy Iteration on Relational Domains
• Verification, Model Checking, and Abstract Interpretation

Cited in

(13)

• Symbolic Model Checking of Hybrid Systems Using Template Polyhedra
• Automatic dynamic parallelotope bundles for reachability analysis of nonlinear systems
• Hybrid Systems: Computation and Control
• Numerical invariants through convex relaxation and max-strategy iteration
• Discretizing affine hybrid automata with uncertainty
• Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration
• Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration
• Hypervolume Approximation in Timed Automata Model Checking
• A Policy Iteration Technique for Time Elapse over Template Polyhedra
• 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)