Currently, perhaps the most limiting bottleneck encountered when applying HYTECH to large systems is its insistence on exact computation, and the resulting resource inefficiencies. To remedy this deficiency, we propose to implement algorithms using approximate computation for the analysis of hybrid systems. Such algorithms will replace arbitrary-precision arithmetic with standard computer arithmetic using fixed-length number representations. Naive numerical rounding, however, might invalidate verification results. Hence some care needs to be exercised when using approximate methods for verification purposes.
We plan to develop approximation methods that guarantee conservative results by erring, if at all, in the direction of safety. Suppose, for example, that we wish to check if all possible system behaviors stay within a target zone. Then overapproximation of the set of system behaviors and underapproximation of the target zone will ensure that approximate analysis yields conservative results: if approximate analysis concludes safety, then the actual system is safe. If, on the other hand, approximate analysis detects an error trajectory, then it must be checked if the error is possible in the actual system, and if not, then the approximation must be refined before reanalysis.
For refining approximations, it will be useful to have a theory of error analysis for hybrid systems. We have started to develop such a theory [66]. For example, while numerical errors and approximation errors may accumulate during the run of a system in the time domain, this may not be case in the phase domain; that is, the system trajectories may stay within a constant error from the target zone.