GUARANTEED TERMINATION IN THE VERIFICATION OF LTL PROPERTIES OF NON-LINEAR ROBUST DISCRETE TIME HYBRID SYSTEMS

DOI10.1142/S0129054107004577zbMath1109.68064MaRDI QIDQ3426788

Werner Damm, Stefan Ratschan, Guilherme A. Pinto

Publication date: 13 March 2007

Published in: International Journal of Foundations of Computer Science (Search for Journal in Brave)

zbMATH Keywords

robustness; model-checking; abstraction refinement; constraint-solving; non-linear hybrid systems

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

Related Items

Safe \& robust reachability analysis of hybrid systems, PTIME parametric verification of safety properties for reasonable linear hybrid automata, Quasi-decidability of a fragment of the first-order theory of real numbers, \textsc{LTL} falsification in infinite-state systems, Safety verification of non-linear hybrid systems is quasi-decidable, Incremental Computation of Succinct Abstractions for Hybrid Systems, Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space, Falsification of LTL Safety Properties in Hybrid Systems

Cites Work

• Unnamed Item
• Unnamed Item
• On optimal control of non-autonomous switched systems with a fixed mode sequence
• Quantified constraints under perturbation
• Verification of cooperating traffic agents
• Algorithmic analysis of nonlinear hybrid systems
• Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems
• Reliable minimax parameter estimation