Compositional Relational Abstraction for Nonlinear Hybrid Systems

We propose techniques to construct abstractions for nonlinear dynamics in terms of relations expressed in linear arithmetic. Such relations are useful for translating the closed loop verification problem of control software with continuous-time, nonlinear plant models into discrete and linear models that can be handled by efficient software verification approaches for discrete-time systems. We construct relations using Taylor model based flowpipe construction and the systematic composition of relational abstractions for smaller components. We focus on developing efficient schemes for the special case of composing abstractions for linear and nonlinear components. We implement our ideas using a relational abstraction system, using the resulting abstraction inside the verification tool NuXMV, which implements numerous SAT/SMT solver-based verification techniques for discrete systems. Finally, we evaluate the application of relational abstractions for verifying properties of time triggered controllers, comparing with the Flow(star) tool. We conclude that relational abstractions are a promising approach towards nonlinear hybrid system verification, capable of proving properties that are beyond the reach of tools such as Flow(star). At the same time, we highlight the need for improvements to existing linear arithmetic SAT/SMT solvers to better support reasoning with large relational abstractions.