Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems
From MaRDI portal
Publication:5696927
DOI10.1142/S012905410300190XzbMath1101.68678WikidataQ124937340 ScholiaQ124937340MaRDI QIDQ5696927
Joël Ouaknine, Ansgar Fehnker, Olaf Stursberg, Zhi Han, Michael Theobald, Edmund M. Clarke, Bruce H. Krogh
Publication date: 19 October 2005
Published in: International Journal of Foundations of Computer Science (Search for Journal in Brave)
Related Items (25)
Advanced algorithms for abstract dialectical frameworks based on complexity analysis of subclasses and SAT solving ⋮ Porous invariants ⋮ Counterexample-guided predicate abstraction of hybrid systems ⋮ Deadness and how to disprove liveness in hybrid dynamical systems ⋮ Template-Based Unbounded Time Verification of Affine Hybrid Automata ⋮ Incremental Computation of Succinct Abstractions for Hybrid Systems ⋮ Verification of Hybrid Systems ⋮ Hybridization methods for the analysis of nonlinear systems ⋮ Abstraction based verification of stability of polyhedral switched systems ⋮ Hybrid automata-based CEGAR for rectangular hybrid systems ⋮ Compositional abstraction refinement for control synthesis ⋮ Stability analysis of planar probabilistic piecewise constant derivative systems ⋮ Refinements of behavioural abstractions for the supervisory control of hybrid systems ⋮ The minimum principle of hybrid optimal control theory ⋮ Taylor approximation for hybrid systems ⋮ Counterexample-Guided Refinement of Template Polyhedra ⋮ Assume–guarantee verification of nonlinear hybrid systems with <scp>Ariadne</scp> ⋮ On the relationships between models in protocol verification ⋮ Hybrid control of networked embedded systems ⋮ Language-Based Abstraction Refinement for Hybrid System Verification ⋮ Falsification of LTL Safety Properties in Hybrid Systems ⋮ Finding Errors of Hybrid Systems by Optimising an Abstraction-Based Quality Estimate ⋮ Differential dynamic logic for hybrid systems ⋮ Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants ⋮ GUARANTEED TERMINATION IN THE VERIFICATION OF LTL PROPERTIES OF NON-LINEAR ROBUST DISCRETE TIME HYBRID SYSTEMS
Cites Work
This page was built for publication: Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems