Piecewise-affine approximations for a powertrain control verification benchmark


We present a benchmark example of an automotive powertrain control system converted to a hybrid system with piecewise-affine (PWA) continuous dynamics. The purpose is to provide an example of an industrial nonlinear system that is amenable to existing software tools for performing verification of safety properties for hybrid systems. Existing algorithmic approaches to hybrid system verification require that system representations are restricted to specific class of models. Therefore, it is important to develop and evaluate techniques to generate approximate models that adhere to the required class of systems without introducing an unacceptable amount of approximation errors. The example we present is intended to demonstrate a symbolic method to automatically approximate a nonlinear model with a PWA approximation while respecting a given bound on the approximation error. While existing tools are applicable to the resulting model, the scale of the PWA model is intended to challenge the capabilities of these tools. We conduct an experimental comparison between the original and PWA models and present our observations and discuss challenges for the research community.

ARCH14-15. 1st and 2nd International Workshop on Applied Verification for Continuous and Hybrid Systems