Algebraic Reasoning for Hybrid Systems -Two Case Studies -

erschienen 2008 in R. Berghammer, B. Möller, G. Struth (eds.): Relations and Kleene algebra in computer science.
Lecture Notes in Computer Science 4988. Springer 2008, pp. 191-205

Abstract:
At an abstract level hybrid systems are related to variants of Kleene algebra. Since it has recently been showed that Kleene algebras and their variants, like omega algebras, provide a reasonable base for automated reasoning, the aim of the present paper is to show that automated algebraic reasoning for hybrid system is feasible. We mainly focus on applications. In particular, we present case studies and proof experiments to show how concrete properties of hybrid systems, like safety and liveness, can be algebraically characterised and how off-the-shelf automated theorem provers can be used to verify them.