Differential Radical Invariants: Safety Verification and Design of Correct Hybrid Systems

Abstract:

The verification of hybrid systems requires ways of handling both the discrete and continuous dynamics, e.g., by proofs, abstraction, or approximation. Fundamentally, however, the study of the safety of hybrid systems can be shown to reduce constructively to the problem of generating invariants for their differ- ential equations. We recently focused on this core problem. We study the case of algebraic invariant equation, i.e. invariants described by a polynomial equation of the form p = 0 for a polynomial p. In [2] we present a novel necessary and sufficient condition for a polynomial p to have the reachable set of the solution as a subset of the set of its roots. We then build on top of this characterization to check the invariance of algebraic set candidate as well as generating invariant equations. We show that the generation of invariant algebraic set can be expressed as a symbolic linear algebra problem. In [3], we extend our characterization to the conjunction of polynomial equalities. Subsequently in [4], we theoretically compared the deductive power of already existing proof rules and discuss an op- timized decision procedure to decide the invariance of algebraic sets. The automated invariant generation of non-linear dynamical systems were successfully used in [1] to effectively design a safe automated traffic management of airplanes where the motion of each airplane is described by a set of continu- ous differential equations, while each pilot is allowed to make discrete decisions to control the aircraft. We abstract the trajectories using automatically generated functional invariants (first integrals). We then use these invariants to generate a safety monitor which will serve to synthesize safe commands for the system. If a possible collision is detected we explicitly give a set of safe, flyable, choices that prevent the collision from happening

References:

1. Ghorbal, K., Jeannin, J.B., Zawadzki, E.W., Platzer, A., Gordon, G.J., Capell, P.: Hybrid the- orem proving of aerospace systems: Applications and challenges. Journal of Aerospace Infor- mation Systems (2014)
2. Ghorbal, K., Platzer, A.: Characterizing algebraic invariants by differential radical invariants.
In: Springer (ed.) TACAS. pp. 279–294 (2014)
3. Ghorbal, K., Sogokon, A., Platzer, A.: Invariance of conjunctions of polynomial equalities for algebraic differential equations. In: Mu¨ller-Olm, M., Seidl, H. (eds.) SAS. LNCS, vol. 8723, pp. 151–167. Springer (2014)
4. Ghorbal, K., Sogokon, A., Platzer, A.: A hierarchy of proof rules for checking differential
invariance of algebraic sets. In: VMCAI. LNCS, Springer (2015), to appear