Verification of Hybrid Systems
From MaRDI portal
Publication:3176388
DOI10.1007/978-3-319-10575-8_30zbMath1392.68246OpenAlexW2803699674MaRDI QIDQ3176388
Laurent Doyen, Goran Frehse, André Platzer, George J. Pappas
Publication date: 20 July 2018
Published in: Handbook of Model Checking (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-10575-8_30
Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items
Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL ⋮ Temporal Logic and Fair Discrete Systems ⋮ Combining Model Checking and Deduction ⋮ Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL ⋮ Strategy synthesis for partially-known switched stochastic systems ⋮ Deductive stability proofs for ordinary differential equations ⋮ An axiomatic approach to existence and liveness for differential equations ⋮ A Simulink-based software solution using the infinity computer methodology for higher order differentiation ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates ⋮ Reachability analysis of a general class of neural ordinary differential equations ⋮ Limit cycle analysis of a class of hybrid gene regulatory networks
Uses Software
Cites Work
- Automatic synthesis of switching controllers for linear hybrid systems: safety control
- Controller synthesis for safety and reachability via approximate bisimulation
- Hybrid systems
- Robust parametric reachability for timed automata
- Hybridization methods for the analysis of nonlinear systems
- On the hardness of computing intersection, union and Minkowski sum of polytopes
- Robust safety of timed automata
- Computing differential invariants of hybrid systems as fixed points
- Differential dynamic logic for hybrid systems
- A calculus of communicating systems
- Partial cylindrical algebraic decomposition for quantifier elimination
- Rigorously computed orbits of dynamical systems without the wrapping effect
- What's decidable about hybrid automata?
- Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models
- Hybrid systems: computation and control. 2nd international workshop, HSCC '99. Berg en Dal, the Netherlands, March 29--31, 1999. Proceedings
- A theory of timed automata
- Reachability analysis of dynamical systems having piecewise-constant derivatives
- Hybrid systems: computation and control. 6th international workshop, HSCC 2003, Prague, Czech Republic, April 3--5, 2003. Proceedings
- Hybrid I/O automata.
- A complete uniform substitution calculus for differential dynamic logic
- Hybrid process algebra
- Process algebra for hybrid systems
- HyTech: A model checker for hybrid systems
- Hybrid systems: computation and control. 7th international workshop, HSCC 2004, Philadelphia, PA, USA, March 25--27, 2004. Proceedings.
- Updatable timed automata
- Interactive decision maps. Approximation and visualization of Pareto frontier
- Discrete-time control for rectangular hybrid automata
- O-minimal hybrid systems.
- Syntax and consistent equation semantics of hybrid Chi
- Counterexample-guided predicate abstraction of hybrid systems
- Hybrid systems: computation and control. 10th international conference, HSCC 2007, Pisa, Italy, April 3--5, 2007. Proceedings.
- Abstractions for hybrid systems
- Constructing invariants for hybrid systems
- Fourier-Motzkin elimination and its dual
- Bisimulation relations for dynamical, control, and hybrid systems
- Almost ASAP semantics: from timed models to timed implementations
- Optimal semicomputable approximations to reachable and invariant sets
- A Differential Operator Approach to Equational Differential Invariants
- Proceedings of the 14th international conference on Hybrid systems: computation and control
- Reachability Analysis of Nonlinear Differential-Algebraic Systems
- Automatic invariant generation for hybrid systems using ideal fixed points
- Quantified differential invariants
- A dynamic algorithm for approximate flow computations
- Avoiding geometric intersection operations in reachability analysis of hybrid systems
- Logics of Dynamical Systems
- The Complete Proof Theory of Hybrid Systems
- Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets
- Flowpipe approximation and clustering in space-time
- On Reachability for Hybrid Automata over Bounded Time
- Embedded System Design
- Differential-algebraic Dynamic Logic for Differential-algebraic Programs
- Verification of cooperating traffic agents
- KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems
- Temporal Logic Verification Using Simulation
- Constraint-Based Approach for Analysis of Hybrid Systems
- Verification of Supervisory Control Software Using State Proximity and Merging
- Generating Box Invariants
- KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
- Safety Verification of Non-linear Hybrid Systems Is Quasi-Semidecidable
- Robust Test Generation and Coverage for Hybrid Systems
- The Image Computation Problem in Hybrid Systems Model Checking
- Foundations of a Compositional Interchange Format for Hybrid Systems
- Periodically Controlled Hybrid Systems
- Verification and Control of Hybrid Systems
- Reachability Analysis of Hybrid Systems Using Support Functions
- On the complexity of four polyhedral set containment problems
- Differential automata and their discrete simulators
- A Decision Procedure for the First Order Theory of Real Addition with Order
- COMPLEXITY AND REAL COMPUTATION: A MANIFESTO
- Conflict resolution for air traffic management: a study in multiagent hybrid systems
- Algorithmic analysis of nonlinear hybrid systems
- A unified framework for hybrid control: model and optimal control theory
- Hybrid automata with finite bisimulations
- Logical Foundations of Cyber-Physical Systems
- The Structure of Differential Invariants and Differential Cut Elimination
- A Complete Axiomatization of Quantified Differential Dynamic Logic for Distributed Hybrid Systems
- Logical Analysis of Hybrid Systems
- Generating Invariants for Non-linear Hybrid Systems by Linear Algebraic Methods
- Using Redundant Constraints for Refinement
- Lazy abstraction
- Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs
- Parametric real-time reasoning
- A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games
- Ellipsoidal Techniques for Reachability Analysis of Discrete-Time Linear Systems
- Approximation Metrics for Discrete and Continuous Systems
- A Framework for Worst-Case and Stochastic Safety Verification Using Barrier Certificates
- Periodicity and chaos from switched flow systems: contrasting examples of discretely controlled continuous systems
- Hybrid Systems: Computation and Control
- Hybrid Systems: Computation and Control
- Hybrid Systems: Computation and Control
- Handbook of Hybrid Systems Control
- Hybrid dynamical systems
- Abstraction and Counterexample-Guided Construction of ω-Automata for Model Checking of Step-Discrete Linear Hybrid Models
- Symbolic Model Checking of Hybrid Systems Using Template Polyhedra
- HYBRID SYSTEM VERIFICATION IS NOT A SINECURE — THE ELECTRONIC THROTTLE CONTROL CASE STUDY
- Algorithm for discovering the set of all the solutions of a linear programming problem
- Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems
- Hybrid Systems: Computation and Control
- Hybrid Systems: Computation and Control
- Hybrid Systems: Computation and Control
- Formal Modeling and Analysis of Timed Systems
- Languages and Tools for Hybrid Systems Design
- Hybrid Systems: Computation and Control
- Symbolic reachability computation for families of linear vector fields
- State equivalences for rectangular hybrid automata
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
