Incremental Computation of Succinct Abstractions for Hybrid Systems

DOI10.1007/978-3-642-24310-3_19zbMath1348.68133OpenAlexW2154637232MaRDI QIDQ3172856

Stefan Ratschan, Tomáš Dzetkulič

Publication date: 7 October 2011

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-24310-3_19

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Attainable sets, reachability (93B03)

Uses Software

• RSOLVER
• HSolver

Cites Work

• Unnamed Item
• Unnamed Item
• Sometime = always + recursion \(\equiv\) always. On the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs
• The essence of constraint propagation
• 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
• Logical Interpretation: Static Program Analysis Using Theorem Proving
• Finding Errors of Hybrid Systems by Optimising an Abstraction-Based Quality Estimate
• Efficient solving of quantified inequality constraints over the real numbers
• Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems

This page was built for publication: Incremental Computation of Succinct Abstractions for Hybrid Systems