SURF 2014: Symbolic Verification of Nonlinear Hybrid Systems using Theorem Provers

2014 SURF project description

• Mentor: Richard M. Murray
• Co-mentor: Ioannis Filippidis

Fig.1: Piecewise affine dynamics representative of systems currently studied with TuLiP.

Fig.2: Abstraction procedure yielding a finite state system approximating the hybrid dynamics.

Fig.3: The proof of a specification about a hybrid program representing a train, as generated by KeYmaera.

The complexity and scale of dynamical systems such as aircraft, autonomous cars and smart buildings together with safety requirements have recently led to the development of new approaches for their synthesis and verification [ 1 ]. One challenge results from the combination of continuous dynamics with computation, resulting in hybrid systems. Current approaches integrate methods from control theory and robotics with verification algorithms from computer science [ 4 ].

Another challenge is scalability of solutions. Symbolic methods prove valuable in reducing the computational complexity of the verification procedure. This project aims at exploring the integration and use of existing symbolic theorem provers with the Temporal Logic Planning Toolbox (TuLiP) [ 2 ] developed by our group. TuLiP is a Python package for automatically synthesizing correct controllers from given specifications. The systems processed by TuLiP are piecewise affine and a discretization step is needed to obtain a finite state representation of their differential equations. This introduces approximations.

An interesting theorem prover for hybrid systems is KeYmaera [ 3 ]. Hybrid programs are used as its modeling language and specifications are expressed in differential dynamic logic. This allows for the exact symbolic verification of non-linear hybrid systems. KeYmaera itself can use several alternatives as backend solvers, including Z3, QEPCAD, and Mathematica.

Possible parts

1. Interfacing the hybrid system representations of TuLiP to the input recognized by KeYmaera, by exporting hybrid programs and calling it with specific options for a proof strategy. This will extend TuLiP's capabilities to non-linear systems.
2. Studying and comparing the trade-offs between hybrid system representations used by different hybrid system solvers.
3. Exploring the compositional proof capabilities of KeYmaera and importing the results of its verification back to TuLiP for further processing.
4. Adding differential dynamic logic to the logics supported by TuLiP.

The experience obtained from working with KeYmaera could help to directly interface other solvers for implementing custom proof strategies.

Required skills: Familiarity with Python and possibly Java (for KeYmaera internals), and interest to learn about hybrid systems, the theory of computation (automata, languages [ 4 ]), and theorem proving.

References

[1] T. Wongpiromsarn, U. Topcu, and R.M. Murray, Synthesis of Control Protocols for Autonomous Systems, Unmanned Systems, 2012 (submitted)

[2] T. Wongpiromsarn, U. Topcu, N. Ozay, H. Xu, and R. Murray, TuLiP: A Software Toolbox for Receding Horizon Temporal Logic Planning, In Proceedings of Hybrid Systems: Computation and Control (HSCC), 2011

[3] A. Platzer, Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics, Springer, 2010

[4] C. Baier and J.-P. Katoen, Principles of Model Checking, MIT Press