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

robustnessmodel-checkingabstraction refinementconstraint-solvingnon-linear hybrid systems

Mathematics Subject Classification ID

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

Related Items

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

Cites Work

• 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
• Unnamed Item
• Unnamed Item