Safety verification of non-linear hybrid systems is quasi-decidable

DOI10.1007/S10703-013-0196-2MaRDI QIDQ2248097zbMATH OpenOpenAlexWikidataFDO

Authors Stefan Ratschan

Publication date 30 June 2014

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10703-013-0196-2

zbMATH Keywords

decidabilityhybrid systemsrobustnesssafety verification

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Safety verification of non-linear hybrid systems is quasi-semidecidable
• GUARANTEED TERMINATION IN THE VERIFICATION OF LTL PROPERTIES OF NON-LINEAR ROBUST DISCRETE TIME HYBRID SYSTEMS
• Automated Technology for Verification and Analysis
• Decidability and complexity for the verification of safety properties of reasonable linear hybrid automata
• Analysis of hybrid systems: An ounce of realism can save an infinity of states

Cites work

• A survey on continuous time computations
• Algorithmic analysis of nonlinear hybrid systems
• Analysis of hybrid systems: An ounce of realism can save an infinity of states
• Continuity and computability of reachable sets
• Dynamical properties of timed automata
• GUARANTEED TERMINATION IN THE VERIFICATION OF LTL PROPERTIES OF NON-LINEAR ROBUST DISCRETE TIME HYBRID SYSTEMS
• scientific article; zbMATH DE number 3281219 (Why is no real title available?)
• scientific article; zbMATH DE number 2242595 (Why is no real title available?)
• scientific article; zbMATH DE number 3068536 (Why is no real title available?)
• Hybrid dynamical systems. Modeling, stability, and robustness
• Interval Methods for Systems of Equations
• Nonlinear systems.
• Quantified constraints under perturbation
• Quantifier elimination and cylindrical algebraic decomposition. Proceedings of a symposium, Linz, Austria, October 6--8, 1993
• Robust undecidability of timed and hybrid systems
• Safety verification of non-linear hybrid systems is quasi-semidecidable
• Semantics and computability of the evolution of hybrid systems
• Set-valued analysis
• Solutions to hybrid inclusions via set and graphical convergence with stability theory applications
• Some undecidable problems involving elementary functions of a real variable
• What's decidable about hybrid automata?

Cited in

(14)

• Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants
• Decidability of verification of safety properties of spatial families of linear hybrid automata
• Decidability and complexity for the verification of safety properties of reasonable linear hybrid automata
• Stabhyli -- a tool for automatic stability verification of non-linear hybrid systems
• A delta-sampling verification theorem for discrete-time, possibly discontinuous systems
• GUARANTEED TERMINATION IN THE VERIFICATION OF LTL PROPERTIES OF NON-LINEAR ROBUST DISCRETE TIME HYBRID SYSTEMS
• Safety verification of non-linear hybrid systems is quasi-semidecidable
• Analysis of hybrid systems: An ounce of realism can save an infinity of states
• Assume-guarantee verification of nonlinear hybrid systems with ARIADNE
• Automated Technology for Verification and Analysis
• Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test
• On generalized two dimensional linear hybrid dynamical systems
• Deciding robust instances of an escape problem for dynamical systems in Euclidean space
• Complete robust hybrid systems reachability

This page was built for publication: Safety verification of non-linear hybrid systems is quasi-decidable

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2248097)