Assume-guarantee verification of nonlinear hybrid systems with ARIADNE
DOI10.1002/RNC.2914zbMATH Open1284.93121OpenAlexW1772923315MaRDI QIDQ5408048FDOQ5408048
Authors: Luca Benvenuti, Davide Bresolin, Alberto Ferrari, Luca Geretti, Tiziano Villa, Pieter Collins 
Publication date: 8 April 2014
Published in: International Journal of Robust and Nonlinear Control (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1002/rnc.2914
Recommendations
- An introduction to the verification of hybrid systems using \textsc{Ariadne}
- Ariadne: dominance checking of nonlinear hybrid automata using reachability analysis
- Safety verification of non-linear hybrid systems is quasi-semidecidable
- Safety verification of non-linear hybrid systems is quasi-decidable
- GUARANTEED TERMINATION IN THE VERIFICATION OF LTL PROPERTIES OF NON-LINEAR ROBUST DISCRETE TIME HYBRID SYSTEMS
Nonlinear systems in control theory (93C10) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30) Realizations from input-output data (93B15)
Cites Work
- HyTech: A model checker for hybrid systems
- Kronos: A verification tool for real-time systems
- Uppaal in a nutshell
- KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
- Graph-Based Algorithms for Boolean Function Manipulation
- What's decidable about hybrid automata?
- Title not available (Why is that?)
- An introduction to Kolmogorov complexity and its applications
- The algorithmic analysis of hybrid systems
- Solutions to hybrid inclusions via set and graphical convergence with stability theory applications
- An Approach to Modelling and Verification of Component Based Systems
- Continuity and computability of reachable sets
- Semantics and computability of the evolution of hybrid systems
- Hybrid I/O automata.
- Abstractions for hybrid systems
- Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems
Cited In (13)
- Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system
- The ksmt calculus is a \(\delta \)-complete decision procedure for non-linear constraints
- Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration
- A dynamic quantized state system execution framework for hybrid automata
- A computable and compositional semantics for hybrid systems
- An introduction to the verification of hybrid systems using \textsc{Ariadne}
- Proving the existence of fair paths in infinite-state systems
- The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints
- Constraint-driven nonlinear reachability analysis with automated tuning of tool properties
- Ariadne: dominance checking of nonlinear hybrid automata using reachability analysis
- Adaptive reachability algorithms for nonlinear systems using abstraction error analysis
- Adaptive parameter tuning for reachability analysis of nonlinear systems
- Formal Verification Applied to Robotic Surgery
Uses Software
This page was built for publication: Assume-guarantee verification of nonlinear hybrid systems with ARIADNE
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5408048)
