Room 206 (2nd floor, badged access)
22 janvier 2019 - 14h00
Verifying Hybrid Systems with Modal Kleene Algebra
par Georg Struth de University of Sheffield
Abstract: Hybrid Systems integrate continuous dynamics and discrete control. Their verification, in domains like the control of chemical plants, finance and traffic systems, the coordination of autonomous vehicles or robots, and the optimisation of mechanical systems or bio systems engineering, is increasingly important. A prominent approach is differential dynamic logic (dL), a modal logic for reasoning about ordinary differential equations and their solutions within hybrid programs. Over the last decade, a domain-specific sequent calculus for dL has been developed together with an intricate explicit substitution calculus. It has been integrated into the KeYmaera X tool, which has proved its worth in numerous case studies.
This talk presents an algebraic reconstruction of dL and the first verification components in an interactive proof assistant inspired by it. It is based on modal Kleene algebra, an extension of Kleene algebra by modal operators in the style of dynamic logic, and integrations of a hybrid store into either the relational or a state transformer semantics of this algebra. This yields a simple semantic variant in which substitutions are replaced by store updates and domains specific inference rules become derivable. At the moment, two approaches to hybrid systems verification are supported: Firstly, solutions to ordinary differential equations can be supplied to the component, and certified along the lines of Picard-Lindelöf's theorem. Verification conditions for the orbits obtained from these solutions, in fact, weakest liberal preconditions, can then be computed and used with the more standard conditions generated by the algebra. Secondly, differential invariants in the style of dL can be supplied and refined within the algebra. Intuitively, these invariants encode the orbit structure of a dynamic system directly as assertions.
Apart from presenting modal Kleene algebra and its extension to hybrid systems, I will comment on the intricacies of formalising the approach within the Isabelle/HOL proof assistant, and outline some future directions for this line of work, time permitting.
This work is joint with Jonathan Julián Huerta y Munive, and partially funded by CONACYT.
