Joerg Preussig, Stephan Kowalewski, Howard Wong-Toi, and Thomas A. Henzinger
Rectangular automata are well suited for the approximate modeling of mixed continuous-discrete systems. The exact analysis of these automata is feasible for small examples but can encounter severe numerical problems for even medium-sized systems. This paper presents an analysis algorithm that uses conservative overapproximation to avoid numerical problems. The algorithm is demonstrated on a simple benchmark system consisting of two connected tanks.
Proceedings of the Fifth International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT), Lecture Notes in Computer Science 1486, Springer, 1998, pp. 228-240.