## Automatic Rectangular Refinement of Affine Hybrid Systems

*Laurent Doyen,
Thomas A. Henzinger,
and Jean-Francois Raskin*

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.

*Proceedings of the Third International Conference on
Formal Modeling and Analysis of Timed Systems*
(FORMATS),
Lecture Notes in Computer Science 3829,
Springer, 2005, pp. 144-161.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2005 Springer.