Automating Numerical Parameters Along the Evolution of a Nonlinear System

When analysing cyber-physical systems for runtime verification purposes, reachability analysis can be used to identify whether the set of reached points stays within given safe bounds. If the system dynamics exhibits nonlinearity, approximate numerical techniques (with rigorous numerics) are often necessary when dealing with system evolution. Since the error involved in numerical approximation should be kept low to perform verification successfully, the associated processing and memory costs become relevant especially when runtime verification is considered. Given a reachability analysis tool, the issue of controlling its numerical accuracy is not trivial from the user's perspective, due to the complex interaction between the configuration parameters of the tool. As a result, user intervention in the tuning of a specific problem is always required. This paper explores the problem of automatically choosing numerical parameters that drive the computation of the finite-time reachable set, when the configuration parameters of the tool are specified within bounds or lists of values. In particular, it is designed to be performed along evolution, in order to adapt to local properties of the dynamics and to reduce the setup overhead, essential for runtime verification.