--- res: bibo_abstract: - We show how to automatically construct and refine rectangular abstractions of systems of linear differential equations. From a hybrid automaton whose dynamics are given by a system of linear differential equations, our method computes automatically a sequence of rectangular hybrid automata that are increasingly precise overapproximations of the original hybrid automaton. We prove an optimality criterion for successive refinements. We also show that this method can take into account a safety property to be verified, refining only relevant parts of the state space. The practicability of the method is illustrated on a benchmark case study. @eng bibo_authorlist: - foaf_Person: foaf_givenName: Laurent foaf_name: Doyen, Laurent foaf_surname: Doyen - foaf_Person: foaf_givenName: Thomas A foaf_name: Thomas Henzinger foaf_surname: Henzinger foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87 orcid: 0000−0002−2985−7724 - foaf_Person: foaf_givenName: Jean foaf_name: Raskin, Jean-François foaf_surname: Raskin bibo_doi: 'DOI: 10.1007/11603009_13' bibo_volume: 3829 dct_date: 2005^xs_gYear dct_publisher: Springer@ dct_title: Automatic rectangular refinement of affine hybrid systems@ ...