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

robustnesshybrid systemsdecidabilitysafety 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
• Publication:4945221

Cites work

• scientific article; zbMATH DE number 1424031 (Why is no real title available?)
• scientific article; zbMATH DE number 1444348 (Why is no real title available?)
• 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?)
• A survey on continuous time computations
• Algorithmic analysis of nonlinear hybrid systems
• 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
• 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
• 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

(11)

• Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test
• On generalized two dimensional linear hybrid dynamical systems
• Decidability of verification of safety properties of spatial families of linear hybrid automata
• Safety verification of non-linear hybrid systems is quasi-semidecidable
• Assume-guarantee verification of nonlinear hybrid systems with ARIADNE
• Decidability and complexity for the verification of safety properties of reasonable linear hybrid automata
• scientific article; zbMATH DE number 1424031 (Why is no real title available?)
• A delta-sampling verification theorem for discrete-time, possibly discontinuous systems
• Automated Technology for Verification and Analysis
• GUARANTEED TERMINATION IN THE VERIFICATION OF LTL PROPERTIES OF NON-LINEAR ROBUST DISCRETE TIME HYBRID SYSTEMS
• Stabhyli -- a tool for automatic stability verification of non-linear hybrid systems

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)