Compositional Taylor model based validated integration

Abstract

Validated integration is a family of methods that compute enclosures for sets of initial conditions in the Initial Value Problems. The Taylor model based validated integration methods use truncated Taylor series to approximate the solution to the Initial Value Problem and often give better results than other validated integration methods. Validated integration methods, and especially Taylor model based ones, become increasingly more impractical as the number of variables in the system get higher. In this thesis, we develop techniques that mitigate the issues related to the dimension of the system in Taylor model based validated integration methods. This is done by taking advantage of the compositional structure of the problem when possible. More precisely, the main contribution of this thesis is to enable computing an enclosure to a higher dimensional system by using enclosures for smaller lower dimensional subsystem that are contained in the larger system. The techniques called shrink wrapping and preconditioning are used in the Taylor model based validated integration to improve accuracy. We also analyse these techniques from a compositional viewpoint and present their compositional counterparts. We accompany compositional version of the Taylor model based validated integration with implementation of our tool CFlow* and experiments using our tool. The experimental results show performance gains for some systems with non-trivial compositional structure. This work was motivated by interest in formally analysing biological systems and we use biological systems examples in a number of our systems.